Module `Solver.MS`

Instance of MiniSat solver.

val solver_type : solver_t
val string_of_solver_t : string

include E

type t
type var
type lit

val create : unit -> t
val set_verbosity : t -> int -> unit
val add_clause : t -> lit list -> unit
val add_at_most : t -> lit list -> int -> unit
val add_at_least : t -> lit list -> int -> unit
val add_exactly : t -> lit list -> int -> unit
val new_var : t -> var
val simplify : t -> unit
val solve : t -> solution
val value_of : t -> var -> value
val get_stats : t -> stats
val positive_lit : var -> lit
val negative_lit : var -> lit
val negate : lit -> lit

val new_var_vector : t -> int -> var array
val new_var_matrix : t -> int -> int -> var array array
val add_clauses : t -> lit list list -> unit
val add_implication : t -> lit -> lit list list -> unit
val add_iff : t -> lit -> lit list list -> unit
val add_conj_pairs : t -> (lit * lit) list -> unit
val add_fun : t -> var array array -> unit
val add_injection : t -> var array array -> unit
val add_bijection : t -> var array array -> unit
val ban : t -> var list -> unit
val get_iso : t -> var array array -> Iso.t
val get_fun : t -> var array array -> Fun.t