package mc2

  1. Overview
  2. Docs
type t = [ `SAT ] state
val eval : t -> atom -> bool

Returns the valuation of a formula in the current state of the sat solver.

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.

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