Parameter Make.S

Internal modules

These are the internal modules used, you should probably not use them if you're not familiar with the internals of mSAT.

include Msat.Solver_intf.EXPR
type proof

An abstract type for proofs

module Term : sig ... end
module Value : sig ... end

formulas

type term = Term.t

user terms

type formula = Formula.t

user formulas

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.

type clause
type theory
type lemma

A theory lemma or an input axiom

type solver
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.

type t = solver

Main solver type, containing all state for solving.

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

Create new solver

  • parameter theory

    the theory

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

val theory : t -> theory

Access the theory state

Types

type res =
  1. | Sat of (term, formula, Value.t) Msat.Solver_intf.sat_state
    (*

    Returned when the solver reaches SAT, with a model

    *)
  2. | 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.

Base operations

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