module Th : Solver_intf.PLUGIN_SAT
These are the internal modules used, you should probably not use them if you're not familiar with the internals of mSAT.
with type Term.t = Solver_intf.void
with module Formula = Th.Formula
module Value : sig ... end
module Formula = Th.Formula
type term = Term.t
type formula = Formula.t
The type of atoms given by the module argument for formulas. An atom is a user-defined atomic formula whose truth value is picked by Msat.
type lemma = Th.proof
A theory lemma or an input axiom
module Atom : sig ... end
module Clause : sig ... end
module Proof : Solver_intf.PROOF with type clause = clause and type atom = atom and type formula = formula and type lemma = lemma and type t = proof
A module to manipulate proofs.
type t = solver
Main solver type, containing all state for solving.
type res =
| Sat of (term, formula, Value.t) Solver_intf.sat_state(*
Returned when the solver reaches SAT, with a model*)
| Unsat of (atom, clause, Proof.t) Solver_intf.unsat_state(*
Returned when the solver reaches UNSAT, with a proof*)
Result type for the solver
Exception raised by the evaluating functions when a literal has not yet been assigned a value.
Add the list of clauses to the current set of assumptions. Modifies the sat solver state in place.
Try and solves the current set of clauses.
Add a new term (i.e. decision variable) to the solver. This term will be decided on at some point during solving, wether it appears in clauses or not.
Add a new atom (i.e propositional formula) to the solver. This formula will be decided on at some point during solving, wether it appears in clauses or not.
true_at_level0 a returns
a was proved at level0, i.e. it must hold in all models
val eval_atom : t -> atom -> Solver_intf.lbool
Evaluate atom in current state
val export : t -> clause Solver_intf.export