Functor Solver.M


module M: 
functor (X : S) -> sig .. end
Parameters:
X : S

type state 
type var = int 
type lit 
val lit_of_var : var -> bool -> lit
val initialize_problem : ?print_var:(Format.formatter -> int -> unit) -> int -> state
initialize the solver
val copy : state -> state
provide a deep copy of the current state of the solver
val propagate : state -> unit
val protect : state -> unit
val reset : state -> unit
reset reset the state of the solver and, in particular, it resets the variable assignment array

type value =
| True
| False
| Unknown
the value of a variable at any give time
val assignment : state -> value array
val add_un_rule : state -> lit -> X.reason list -> unit
add_un_rule gets that state of the solver, a literal and reasons to return in case this clause was involved in a clash.
val add_bin_rule : state -> lit -> lit -> X.reason list -> unit
add_bin_rule gets that state of the solver, two literals a,b and a list reasons to return in case this clause was involved in a clash. Updates the internal state of the solver with ( a \lor b )
val add_rule : state -> lit array -> X.reason list -> unit
add_bin_rule gets that state of the solver, a list of literals l and a list reasons to return in case this clause was involved in a clash. Updates the internal state of the solver with ( \Bigvee l )
val associate_vars : state -> lit -> var list -> unit
associate_vars associate a variable to a list of variables. The solver * will use this information to guide the search heuristic
val solve : state -> var -> bool
solve st v finds a variable assignment that makes v true
val solve_lst : state -> var list -> bool
solve st l finds a variable assignment that makes true all variables in l
val collect_reasons : state -> var -> X.reason list
val collect_reasons_lst : state -> var list -> X.reason list