exception Sat of texception Unsat of Explanation.texception I_dont_know of tval empty : unit -> tthe empty sat-solver context
push env n add n new assertion levels. A guard g is added for every expression e assumed at the current assertion level. Ie. assuming e after the push will become g -> e, a g will be forced to be true (but not propagated at level 0)
pop env n remove an assertion level. Internally, the guard g introduced in the push correponsding to this pop will be propagated to false (at level 0)
val assume : t -> Expr.gformula -> Explanation.t -> tassume env f assume a new formula f in env. Raises Unsat if f is unsatisfiable in env
val assume_th_elt : t -> Expr.th_elt -> Explanation.t -> tassume env f exp assume a new formula f with the explanation exp in the theories environment of env.
val pred_def : t -> Expr.t -> string -> Explanation.t -> Loc.t -> tpred_def env f assume a new predicate definition f in env.
val unsat : t -> Expr.gformula -> Explanation.tunsat env f size checks the unsatisfiability of f in env. Raises I_dont_know when the proof tree's height reaches size. Raises Sat if f is satisfiable in env
print_model header fmt env print propositional model and theory model on the corresponding fmt.
val get_model : t -> unitget_model t produces the current model.