module Solver_intf:sig
..end
This modules defines the safe external interface for solvers.
Solvers that implements this interface can be obtained using the Make
functor in Solver
or Mcsolver
.
type ('term, 'form)
sat_state = {
|
eval : |
(* |
Returns the valuation of a formula in the current state
of the sat solver.
Raises UndecidedLit if the literal is not decided | *) |
|
eval_level : |
(* |
Return the current assignement of the literals, as well as its
decision level. If the level is 0, then it is necessary for
the atom to have this value; otherwise it is due to choices
that can potentially be backtracked.
Raises UndecidedLit if the literal is not decided | *) |
|
iter_trail : |
(* |
Iter thorugh the formulas and terms in order of decision/propagation
(starting from the first propagation, to the last propagation).
| *) |
|
model : |
(* |
Returns the model found if the formula is satisfiable.
| *) |
type ('clause, 'proof)
unsat_state = {
|
unsat_conflict : |
(* |
Returns the unsat clause found at the toplevel
| *) |
|
get_proof : |
(* |
returns a persistent proof of the empty clause from the Unsat result.
| *) |
module type S =sig
..end
Solver.Make
and Mcsolver.Make
functors.