Satml.Make
type th = Th.t
val solve : t -> unit
val set_new_proxies :
t ->
(Satml_types.Atom.atom * Satml_types.Atom.atom list * bool)
AltErgoLib.Util.MI.t ->
unit
val new_vars :
t ->
nbv:int ->
Satml_types.Atom.var list ->
Satml_types.Atom.atom list list ->
Satml_types.Atom.atom list list ->
Satml_types.Atom.atom list list * Satml_types.Atom.atom list list
val assume :
t ->
Satml_types.Atom.atom list list ->
Satml_types.Atom.atom list list ->
Expr.t ->
cnumber:int ->
Satml_types.Atom.atom option AltErgoLib.Satml_types.Flat_Formula.Map.t ->
dec_lvl:int ->
unit
val boolean_model : t -> Satml_types.Atom.atom list
val instantiation_context :
t ->
Satml_types.Flat_Formula.hcons_env ->
AltErgoLib.Satml_types.Atom.Set.t
val empty : unit -> t
val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> unit
val decision_level : t -> int
val cancel_until : t -> int -> unit
val update_lazy_cnf :
t ->
do_bcp:bool ->
Satml_types.Atom.atom option AltErgoLib.Satml_types.Flat_Formula.Map.t ->
dec_lvl:int ->
unit
val exists_in_lazy_cnf : t -> Satml_types.Flat_Formula.t -> bool
val known_lazy_formulas : t -> int AltErgoLib.Satml_types.Flat_Formula.Map.t
val reason_of_deduction :
Satml_types.Atom.atom ->
AltErgoLib.Satml_types.Atom.Set.t
val assume_simple : t -> Satml_types.Atom.atom list list -> unit
val decide : t -> Satml_types.Atom.atom -> unit
val conflict_analyze_and_fix : t -> conflict_origin -> unit
val push : t -> Satml_types.Atom.atom -> unit
val pop : t -> unit