## 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

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