msat

Library containing a SAT solver that can be parametrized by a theory
Library msat
Module Msat . Make_cdcl_t

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 type Term.t = Solver_intf.void with module Formula = Th.Formula
type proof

An abstract type for proofs

module Term : sig ... end
module Value : sig ... end
module Formula = Th.Formula
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 = Th.t
type lemma = Th.proof

A theory lemma or an input axiom

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

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 =
| 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 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 -> Solver_intf.lbool

Evaluate atom in current state

val export : t -> clause Solver_intf.export