Module Solver.MS

Instance of MiniSat solver.

val solver_type : Solver_intf.solver_t
val string_of_solver_t : string
include Solver_intf.E
type t
type var
val pp_var : Ppx_deriving_runtime.Format.formatter -> var -> Ppx_deriving_runtime.unit
val show_var : var -> Ppx_deriving_runtime.string
type lit
val pp_lit : Ppx_deriving_runtime.Format.formatter -> lit -> Ppx_deriving_runtime.unit
val show_lit : lit -> Ppx_deriving_runtime.string
val create : unit -> t
val set_verbosity : t -> int -> unit
val add_clause : t -> lit list -> unit
val add_clause_empty : t -> unit
val add_clause_unit : t -> lit -> unit
val add_clause_binary : t -> lit -> lit -> unit
val add_clause_ternary : t -> lit -> lit -> lit -> unit
val add_clause_quaternary : t -> lit -> lit -> lit -> lit -> 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 okay : t -> bool
val simplify : t -> unit
val solve : t -> Solver_intf.solution
val solve_all : t -> var list -> var list list
val value_of : t -> var -> Solver_intf.value
val get_stats : t -> Solver_intf.stats
val cpu_time : unit -> float

Cumulative user CPU time (seconds) for the process, as measured by the solver's C layer. Monotonic; not reset per solve.

val positive_lit : var -> lit

Cumulative user CPU time (seconds) for the process, as measured by the solver's C layer. Monotonic; not reset per solve.

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_implication : t -> lit -> lit list 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