This code is free, under the Apache 2.0 license.
mSAT is an ocaml library providing SAT/SMT/McSat solvers. More precisely, what mSAT provides are functors to easily create such solvers. Indeed, the core of a sat solver does not need much information about either the exact representation of terms or the inner workings of a theory.
Most modules in mSAT actually define functors. These functors usually take one or two arguments, usually an implementation of Terms and formulas used, and an implementation of the theory used during solving.
The following modules allow to easily create a SAT or SMT solver (remark: a SAT solver is simply an SMT solver with an empty theory).
| Solver | Create SAT/SMT Solvers |
| Solver_intf | Interface for Solvers |
| Formula_intf | SMT formulas |
| Theory_intf | SMT Theory |
The following modules allow the creation of a McSat solver (Model Constructing solver):
| Mcsolver | Create McSat solver |
| Solver_intf | Interface for Solvers |
| Expr_intf | Mcsat expressions |
| Plugin_intf | McSat Theory |
An instanciation of a pure sat solver is also provided:
| Sat | Sat solver |
Lastly, mSAT also provides an implementation of Tseitin's CNF conversion:
| Tseitin | Tseitin CNF conversion |
| Tseitin_intf | Interfaces for Tseitin's CNF conversion |
mSAT solvers are able to provide detailed proofs when an unsat state is reached. To do
so, it require the provided theory to give proofs of the tautologies it gives the solver.
These proofs will be called lemmas. The type of lemmas is defined by the theory and can
very well be unit.
In this context a proof is a resolution tree, whose conclusion (i.e. root) is the
empty clause, effectively allowing to deduce false from the hypotheses.
A resolution tree is a binary tree whose nodes are clauses. Inner nodes' clauses are
obtained by performing resolution between the two clauses of the children nodes, while
leafs of the tree are either hypotheses, or tautologies (i.e. conflicts returned by
the theory).
| Res | Resolution proofs |
| Res_intf | Interface for proofs |
Backends for exporting proofs to different formats:
| Dot | Dot backend for proofs |
| Coq | Coq Backend |
| Dedukti | Deduki backend for proofs |
| Backend_intf | Backend interface |
WARNING: for advanced users only ! These modules expose a lot of unsafe functions that must be used with care to not break the required invariants. Additionally, these interfaces are not part of the main API and so are subject to a lot more breaking changes than the safe modules above.
| Dimacs | |
| Internal | mSAT core |
| External | mSAT safe interface |
| Solver_types | Internal types (implementation) |
| Solver_types_intf | Internal types (interface) |