OpenSMT 0.2 System Description

Overview

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:

  • 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_IDL, QF_RDL, QF_LRA, QF_BV, QF_UFIDL, 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 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].

Expected Performance

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.

Future Steps

The following features are currently on our TODO list: further theory combination, quantifiers, solver for arrays theory, solver for linear integer arithmetic theory.

 

References

[1] David Detlefs, Greg Nelson, and James B. Saxe. Simplify: a theorem prover for program checking. Journal of ACM, 52(3):365–473, 2005.
[2] MiniSAT. http://minisat.se.
[3] Robert Nieuwenhuis and Albert Oliveras. Proof-Producing Congruence Closure. In RTA’05, pages 453–468, 2005.
[4] OpenSMT. http://code.google.com/p/opensmt.
[5] R. Bruttomesso. An Extension of the Davis-Putnam Procedure and its Application to Preprocessing in SMT. In SMT, 2009.
[6] S. Cotton and O. Maler. Fast and Flexible Difference Constraint Propagation for DPLL(T). In SAT’06, pages 170–183, 2006.
[7] B. Dutertre and L. M. de Moura. A Fast Linear-Arithmetic Solver for DPLL(T). In CAV’06, pages 81–94, 2006.
[8] The GNU Multiple Precision Library. http://gmplib.org.
[9] R. Bruttomesso and N. Sharygina. A Scalable Decision Procedure for Fixed-Width Bit-Vectors. In ICCAD, 2009. to appear.