Up
# module EdosSolver

: sig

Edos sat solver

#

module type T = sig

Sat solver functor type

#

type state

state of the solver

#

type var = int

variables are integers numbered from 0 to (size - 1)

#

type lit

A literal. Literals can be positive or negative

#

val initialize_problem : ?pbo:int array -> ?print_var:(Format.formatter -> int -> unit) -> ?buffer:bool -> int -> state

initialize the solver `initialize_problem n`

print_var a function to print a variable

buffer decide weather or not to store a human readable
representaion of the sat problem.

n the size of the sat problem. that is the max number of
variables to consider

#

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 add_rule : state -> lit array -> X.reason list -> unit

`add_rule st l`

add a disjuction to the solver of type TARGET NONE: \Bigvee l

#

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

end

end