Release of mSAT version 0.7. Changes include:

Bugfixes

• Some propagations were forgotten, which caused problems because it could make some conflicts disappear.
• Similarly, new subterms could be forgotten to be added for semantic decision during temporary propagations
• Duplicate elimination in clauses was buggy
• Subterms are now added before simplification, in order to not forget terms
• Late conflicts (with level lower than the current level) are now allowed
• User level pushed while the solver is in the UNSAT state now raise an exception, as the solver is not in a coherent state that allows backtracking and storing

Features

• New backend for Coq Proofs
• Better interface for the Dot backend (breaking)
• Propagations are now done at the lowest possible level (instead of the current level), following the possibility for late conflicts

Internal Changes

• Better travis scripts (using opam 2.0)
• Some warnings are now fixed
• Some additional internal assertions particularly concerning theory inputs (conflicts clauses, etc...)

This release comes with full documentation and some new features:

• An already instantiated sat solver available in the Sat module
• A full_slice function for running possibly expensive satisfiability tests (in SMTs) when a propositional model has been found
• Forgetful propagations: propagations whose reason (i.e clause) is not watched

New release with some breaking changes:

• a cleaner API, moving some types outside the client-required interface
• remove push/pop (source of many bugs), replaced by solve : assumptions:lit list -> unit -> result for local assumptions
• some performance improvements
• many bugfixes
• more tests

New release, containing mainly bug fixes, but also with:

• Proofs for atoms at level 0
• Compatibility with ocaml >= 4.00
• Released some restrictions on dummy sat theories

Along with a few bugfixes, this release brings the following some new features:

• push/pop operations
• access to decision level when evaluating literals

There have been some refactoring of code and some changes in internal modules, some of which visible in exported interfaces, so expect some breaking changes. More precisely:

• the Log argument has been removed from functors
• instead, log capabilities are now ensured by the Msat.Log module, which is current implements inlined dummy functions, effectively negating any costs (as well as the logs)
• All the functors now take a dummy last argument to ensure the solver modules are unique

First release of the modular SAT solver mSAT.

This library provides functor to easily build a SAT, SMT and/or McSAT solver given an implementation of terms. Current features of the solver are:

• decent performances
• proof output
• push/pop operations
• CNF transformation tools

This project derives from Alt-Ergo Zero, but does not provide any built-in theories, it is designed to let the users use their own implementation of terms and theories.