These are the internal modules used, you should probably not use them if you're not familiar with the internals of mSAT.
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 theory = Th.t
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 =
Returned when the solver reaches SAT, with a model*)
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.
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