Module `Msat_sat`

Sat solver

This modules instanciates a pure sat solver using integers to represent atomic propositions.

A functor that can generate as many solvers as needed.

include Msat.S with type Formula.t = Int_lit.t and type theory = unit and type lemma = unit

include Msat.Solver_intf.EXPR

module Term : sig ... end

module Value : sig ... end

module Formula : Msat.Solver_intf.FORMULA

type atom: 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.

module Atom : sig ... end

module Clause : sig ... end

module Proof : Msat.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.

val create : ?⁠store_proof:bool -> ?⁠size:[ `Tiny | `Small | `Big ] -> theory -> t

Create new solver

parameter store_proof: if true, stores proof (default true). Otherwise the functions that return proofs will fail with No_proof

parameter size: the initial size of internal data structures. The bigger, the faster, but also the more RAM it uses.

type res = | Sat of (term, formula, Value.t) Msat.Solver_intf.sat_state Returned when the solver reaches SAT, with a model | Unsat of (atom, clause, Proof.t) Msat.Solver_intf.unsat_state Returned when the solver reaches UNSAT, with a proof: Result type for the solver

exception UndecidedLit: Exception raised by the evaluating functions when a literal has not yet been assigned a value.

val assume : t -> formula list list -> lemma -> unit: Add the list of clauses to the current set of assumptions. Modifies the sat solver state in place.

val add_clause : t -> atom list -> lemma -> unit: Lower level addition of clauses

val add_clause_a : t -> atom array -> lemma -> unit: Lower level addition of clauses

val solve : ?⁠assumptions:atom list -> t -> res

Try and solves the current set of clauses.

parameter assumptions: additional atomic assumptions to be temporarily added. The assumptions are just used for this call to solve, they are not saved in the solver's state.

val make_term : t -> term -> unit: 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.

val make_atom : t -> formula -> atom: 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.

val true_at_level0 : t -> atom -> bool: true_at_level0 a returns true if a was proved at level0, i.e. it must hold in all models

val eval_atom : t -> atom -> Msat.Solver_intf.lbool: Evaluate atom in current state

`\|` `Sat of (term, formula, Value.t) Msat.Solver_intf.sat_state`	Returned when the solver reaches SAT, with a model
`\|` `Unsat of (atom, clause, Proof.t) Msat.Solver_intf.unsat_state`	Returned when the solver reaches UNSAT, with a proof