package msat

  1. Overview
  2. Docs
Library containing a SAT solver that can be parametrized by a theory

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (16)

Authors

  1. S
    Simon Cruanes
  2. G
    Guillaume Bury

Maintainers

  1. G
    guillaume.bury@gmail.com
  2. S
    simon.cruanes.2007@m4x.org

Sources

v0.9.1.tar.gz
md5=ba623630b0b8e0edc016079dd214c80b
sha512=51c133cefe8550125e7b1db18549e893bac15663fdd7a9fac87235c07de755f39eab9fc3cfdf6571612fd79b3d5b22f49f459581b480c7349bacddf2618c8a99

doc/msat.sat/Msat_sat/index.html

Module Msat_sat

Sat solver

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

module Int_lit : sig ... end

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

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 with type Formula.t = Int_lit.t
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 = unit
type lemma = unit

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 : ?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 -> Msat.Solver_intf.lbool

Evaluate atom in current state