OpenSMT is a small, efficient and open-source SMT-Solver, currently released under the GNU General Public Licence 3.
The main motivations of OpenSMT are:
OpenSMT includes a parser for SMT-LIB language, a state-of-the-art SAT-Solver, and a clean interface for plugging in new theory-solvers; a template (empty) theory-solver is provided, to facilitate the development of solvers for other logics.
OpenSMT currently supports the following logics: QF_UF, QF_IDL, QF_RDL, QF_LRA, QF_BV, QF_UFIDL, QF_UFLRA.
OpenSMT is written in C++. It is based on MiniSAT 2.0 [2]. We tried to avoid modifications of its code as much as possible. Any added or modified line in the code is explicitly indicated.
A feature of OpenSMT is to provide an automatic mechanisms to compute reasons for theory-deductions by means of the consistency check algorithm. This makes it easier the implementation of a new solver, as the solver is required just to detect deduction without having to provide an immediate explanation for them, and without storing any additional information. This mechanism enables the possibility of performing theory-propagation for inherently complex theories such as bit-vectors.
OpenSMT implements a preliminary preprocessor for SMT arithmetic formulae based on [5]. We are working to make it more stable.
The congruence closure algorithm implemented is the same as the one used in Simplify [1], however we rely on the algorithm of [3] for retrieving explanations: this can be done by storing the necessary information for retrieving the conflict inside the data-structures for term-representation described in [1].
The difference logic solver is based on [6] and it works on integers. QF_RDL benchmarks are translated into the equisatisfiable QF_IDL version at preprocessing time. The solver for QF_LRA is based on [7]. Every arithmetic solver supports infinite precision arithmetic, ultimately based on GMP [8]. The solver for QF_BV is ultimately based on bit-blasting. It also embeds the decision procedure described in [9].
OpenSMT is still in a preliminary stage, as the version number suggests. We expect decent performance for QF_UF, QF_RDL, and QF_IDL. As far as QF_LRA and QF_BV are concerned we didn’t have time to perform extensive tuning for the competition.
The following features are currently on our TODO list: further theory combination, quantifiers, solver for arrays theory, solver for linear integer arithmetic theory.