functor (X : S) ->
sig
type state
type var = int
type lit
val lit_of_var : Solver.M.var -> bool -> Solver.M.lit
val initialize_problem :
?print_var:(Format.formatter -> int -> unit) -> int -> Solver.M.state
val copy : Solver.M.state -> Solver.M.state
val propagate : Solver.M.state -> unit
val protect : Solver.M.state -> unit
val reset : Solver.M.state -> unit
type value = True | False | Unknown
val assignment : Solver.M.state -> Solver.M.value array
val add_un_rule : Solver.M.state -> Solver.M.lit -> X.reason list -> unit
val add_bin_rule :
Solver.M.state -> Solver.M.lit -> Solver.M.lit -> X.reason list -> unit
val add_rule :
Solver.M.state -> Solver.M.lit array -> X.reason list -> unit
val associate_vars :
Solver.M.state -> Solver.M.lit -> Solver.M.var list -> unit
val solve : Solver.M.state -> Solver.M.var -> bool
val solve_lst : Solver.M.state -> Solver.M.var list -> bool
val collect_reasons : Solver.M.state -> Solver.M.var -> X.reason list
val collect_reasons_lst :
Solver.M.state -> Solver.M.var list -> X.reason list
end