Overview
OpenSMT is a small, efficient and open-source SMT-Solver, currently released under the BSD-licensed.
The main motivations of OpenSMT are:
- to promote the use of SMT-Solvers in combination with other verification tools
- to provide a level of detail of decision procedures that goes beyond the scientific publication
- to promote the development of efficient SMT-Solvers by providing a simple infrastructure for helping non-experts to develop theory-solvers without having to start from scratch
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_LIA, QF_LRA, QF_IDL, QF_RDL, QF_AX, QF_UFLIA, QF_UFLRA.
Implementation Details
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 mechanism 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].
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].
