package dose3
Install
Dune Dependency
Authors
Maintainers
Sources
md5=bc99cbcea8fca29dca3ebbee54be45e1
sha512=98dc4bd28e9f4aa8384be71b31783ae1afac577ea587118b8457b554ffe302c98e83d0098971e6b81803ee5c4f2befe3a98ef196d6b0da8feb4121e982ad5c2f
doc/dose3.algo/Dose_algo/Depsolver_int/S/index.html
Module Depsolver_int.S
Source
state of the solver
variables are integers numbered from 0 to (size - 1)
The value of a literal
A literal. Literals can be positive or negative
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:(Format.formatter -> int -> unit) ->
?buffer:bool ->
int ->
state
initialize the solver initialize_problem n
reset
reset the state of the solver to a state that would be obtained by re initializing the solver with an identical constraints set
assignment st
return the array of values associated to every variable.
assignment_true st
return the list of variables that are true
add_rule st l
add a disjuction to the solver of type \Bigvee l
associate_vars st lit vl
associate a variable to a list of variables. The solver will use this information to guide the search heuristic
solve st l
finds a variable assignment that makes True
all variables in l
in case of failure return the list of associated reasons
in case of failure return the list of associated reasons
if the solver was initialized with buffer = true
, dump the state of the solver. Return an empty list otherwise
enable debug messages