package mc2

  1. Overview
  2. Docs

Module Solver.Sat_stateSource

Sourcetype t = [ `SAT ] state
Sourceval eval : t -> atom -> bool

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

Sourceval eval_opt : t -> atom -> bool option

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

Sourceval 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.

Sourceval 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).

Sourceval model : t -> Mc2_core__.Solver_types.assignment_view list

Returns the model found if the formula is satisfiable.

Sourceval check_model : t -> bool

Check model, or fail