Up

module EdosSolver

: sig

Edos sat solver

#
module type S = sig

generic failure reason

#
type reason
end
#
module type T = sig

Sat solver functor type

#
module X : S

generic failure reason

#
type state

state of the solver

#
type var = 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 : ?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 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 TARGET NONE: \Bigvee l

#
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
#
val solve_pbo : (int array * 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
#
val pboidx : state -> int -> int -> int
end
#
module M : functor (X : S) -> T with module X = X

functor

end