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