Module Msat.Make_mcsatSource

Parameters

Signature

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 Solver_intf.EXPR with module Term = Th.Term with module Formula = Th.Formula
Sourcetype proof

An abstract type for proofs

Sourcemodule Term = Th.Term
Sourcemodule Value : sig ... end
Sourcemodule Formula = Th.Formula
Sourcetype term = Term.t

user terms

Sourcetype formula = Formula.t

user formulas

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

Sourcetype clause
Sourcetype theory = Th.t
Sourcetype lemma = Th.proof

A theory lemma or an input axiom

Sourcetype solver
Sourcemodule Atom : sig ... end
Sourcemodule Clause : sig ... end
Sourcemodule 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.

Sourcetype t = solver

Main solver type, containing all state for solving.

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

Sourceval theory : t -> theory

Access the theory state

Types

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

    Returned when the solver reaches SAT, with a model

    *)
  2. | Unsat of (atom, clause, Proof.t) Solver_intf.unsat_state
    (*

    Returned when the solver reaches UNSAT, with a proof

    *)

Result type for the solver

Sourceexception UndecidedLit

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

Base operations

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

Sourceval add_clause : t -> atom list -> lemma -> unit

Lower level addition of clauses

Sourceval add_clause_a : t -> atom array -> lemma -> unit

Lower level addition of clauses

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

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

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

Sourceval 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

Sourceval eval_atom : t -> atom -> Solver_intf.lbool

Evaluate atom in current state