sig
module X : S
type state
type var = int
type value = True | False | Unknown
type lit
val lit_of_var : Common.EdosSolver.T.var -> bool -> Common.EdosSolver.T.lit
val initialize_problem :
?print_var:(Format.formatter -> int -> unit) ->
?buffer:bool -> int -> Common.EdosSolver.T.state
val copy : Common.EdosSolver.T.state -> Common.EdosSolver.T.state
val propagate : Common.EdosSolver.T.state -> unit
val protect : Common.EdosSolver.T.state -> unit
val reset : Common.EdosSolver.T.state -> unit
val assignment :
Common.EdosSolver.T.state -> Common.EdosSolver.T.value array
val assignment_true :
Common.EdosSolver.T.state -> Common.EdosSolver.T.var list
val add_rule :
Common.EdosSolver.T.state ->
Common.EdosSolver.T.lit array -> X.reason list -> unit
val associate_vars :
Common.EdosSolver.T.state ->
Common.EdosSolver.T.lit -> Common.EdosSolver.T.var list -> unit
val solve_all :
(Common.EdosSolver.T.state -> unit) ->
Common.EdosSolver.T.state -> Common.EdosSolver.T.var -> bool
val solve : Common.EdosSolver.T.state -> Common.EdosSolver.T.var -> bool
val solve_lst :
Common.EdosSolver.T.state -> Common.EdosSolver.T.var list -> bool
val collect_reasons :
Common.EdosSolver.T.state -> Common.EdosSolver.T.var -> X.reason list
val collect_reasons_lst :
Common.EdosSolver.T.state ->
Common.EdosSolver.T.var list -> X.reason list
val dump : Common.EdosSolver.T.state -> (int * bool) list list
val debug : bool -> unit
val stats : Common.EdosSolver.T.state -> unit
end