Satml_frontend.Make
exception Sat of t
exception Unsat of Explanation.t
exception I_dont_know of t
val empty : unit -> t
the 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 -> t
assume 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 -> t
assume 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 -> t
pred_def env f
assume a new predicate definition f
in env
.
val unsat : t -> Expr.gformula -> Explanation.t
unsat 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 -> unit
get_model t
produces the current model.