Module type `EdosSolver.T`

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 : ?⁠print_var:(Stdlib.Format.formatter -> int -> unit) -> ?⁠buffer:bool -> int -> state

initialize the solver initialize_problem n

parameter print_var: a function to print a variable

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

parameter 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 \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 : 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: 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