Module Solver.Sat_state
type t
= [ `SAT ] state
val eval : t -> atom -> bool
Returns the valuation of a formula in the current state of the sat solver.
- raises UndecidedLit
if the literal is not decided
val eval_opt : t -> atom -> bool option
Returns the valuation of a formula in the current state of the sat solver.
val eval_level : t -> atom -> bool * int
Return the current assignment 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
val iter_trail : t -> Mc2_core__.Solver_types.term Iter.t
Iterate through the formulas and terms in order of decision/propagation (starting from the first propagation, to the last propagation).
val model : t -> Mc2_core__.Solver_types.assignment_view list
Returns the model found if the formula is satisfiable.
val check_model : t -> bool
Check model, or fail