msat 0.9.1 · OCaml Package

Parameters

module Th : Solver_intf.PLUGIN_SAT

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 = unit

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 : 
  ?on_conflict:(atom array -> unit) ->
  ?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