sig
  type solution = int list
  module type S =
    sig
      type t
      val create : ?primary:int -> bool array array -> Emc.S.t
      val create_sparse :
        ?primary:int -> columns:int -> int list array -> Emc.S.t
      val find_solution : Emc.S.t -> Emc.solution
      val iter_solution : (Emc.solution -> unit) -> Emc.S.t -> unit
      val count_solutions : Emc.S.t -> int
      module type ARITH =
        sig
          type t
          val zero : Emc.S.ARITH.t
          val one : Emc.S.ARITH.t
          val add : Emc.S.ARITH.t -> Emc.S.ARITH.t -> Emc.S.ARITH.t
        end
      module Count :
        functor (A : ARITH) -> sig val count_solutions : Emc.S.t -> A.t end
    end
  module D : S
  module Z :
    sig
      type t = Zdd.t
      val create : ?primary:int -> bool array array -> t
      val create_sparse : ?primary:int -> columns:int -> int list array -> t
      val find_solution : t -> solution
      val iter_solution : (solution -> unit) -> t -> unit
      val count_solutions : t -> int
      module type ARITH =
        sig type t val zero : t val one : t val add : t -> t -> t end
      module Count :
        functor (A : ARITH) -> sig val count_solutions : t -> A.t end
    end
  val print_boolean_matrix : Format.formatter -> bool array array -> unit
  val print_boolean_array : Format.formatter -> bool array -> unit
  val print_matrix_size : Format.formatter -> 'a array array -> unit
  module Sat :
    sig
      type t
      val create : primary:int -> bool array array -> Emc.Sat.t
      val create_sparse : primary:int -> int list array -> Emc.Sat.t
      val print : Format.formatter -> Emc.Sat.t -> unit
      val print_in_file : string -> Emc.Sat.t -> unit
    end
end