module type T =sig
..end
Sat solver functor type
module X:Common.EdosSolver.S
generic failure reason
type
state
state of the solver
typevar =
int
variables are integers numbered from 0 to (size - 1)
type
value =
| |
True |
| |
False |
| |
Unknown |
The value of a literal
type
lit
A literal. Literals can be positive or negative
val lit_of_var : var -> bool -> lit
lit_of_var
given a variable create a positive or a negative literal.
By default the assigment of all variables (that is its value) is
Unknown.
val initialize_problem : ?print_var:(Stdlib.Format.formatter -> int -> unit) ->
?buffer:bool -> int -> state
initialize the solver initialize_problem n
print_var
: a function to print a variablebuffer
: decide weather or not to store a human readable
representaion of the sat problem.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 to a state that would be obtained
by re initializing the solver with an identical constraints set
val assignment : state -> value array
assignment st
return the array of values associated to every variable.
val assignment_true : state -> var list
assignment_true st
return the list of variables that are true
val add_rule : state ->
lit array -> X.reason list -> unit
add_rule st l
add a disjuction to the solver of type
val associate_vars : state ->
lit -> var list -> unit
associate_vars st lit vl
associate a variable to a list of variables. The solver
will use this information to guide the search heuristic
val solve_all : (state -> unit) ->
state -> var -> bool
solve st v
finds a variable assignment that makes v
True
val solve : state -> var -> bool
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
in case of failure return the list of associated reasons
val collect_reasons_lst : state -> var list -> X.reason list
in case of failure return the list of associated reasons
val dump : state -> (int * bool) list list
if the solver was initialized with buffer = true
,
dump the state of the solver. Return an empty list otherwise
val debug : bool -> unit
enable debug messages
val stats : state -> unit