package msat

You can search for identifiers within the package.

in-package search v0.2.0

Library containing a SAT solver that can be parametrized by a theory

Install

Dune Dependency

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

Authors

Maintainers

Sources

v0.8.2.tar.gz

md5=c02d63bf45357aa1d1b85846da373f48

sha512=e6f0d7f6e4fe69938ec2cc3233b0cb72dd577bfb4cc4824afe8247f5db0b6ffea2d38d73a65e7ede500d21ff8db27ed12f2c4f3245df4451d02864260ae2ddaf

doc/msat.sat/Msat_sat/index.html

Module `Msat_sat`Source

Sat solver

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

Sourcemodule 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

Sourcetype proof

An abstract type for proofs

Sourcemodule Term : sig ... end

Sourcemodule Value : sig ... end

Sourcemodule Formula : Msat.Solver_intf.FORMULA with type t = Int_lit.t

formulas

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

Sourcetype lemma = unit

A theory lemma or an input axiom

Sourcetype solver

Sourcemodule Atom : sig ... end

Sourcemodule Clause : sig ... end

Source

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.

Sourcetype t = solver

Main solver type, containing all state for solving.

Source

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.

Sourceval theory : t -> theory

Access the theory state

Types

Sourcetype res =

| Sat of (term, formula, Value.t) Msat.Solver_intf.sat_state
(*
Returned when the solver reaches SAT, with a model
*)
| 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

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

Evaluate atom in current state

Sourceval export : t -> clause Msat.Solver_intf.export