package msat

  1. Overview
  2. Docs
package msat
Legend:
Library
Module
Module type
Parameter
Class
Class type

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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct