Home

SMT-RAT is an open source C++ toolbox for strategic and parallel SMT solving consisting of a collection of SMT compliant implementations of methods for solving quantifier-free (non)linear real and integer arithmetic (QF_LRA, QF_LIA, QF_NRA, QF_NIA) formulas, we refer to as modules. These modules can be combined to (1) an SMT solver or (2) a theory solver in order to extend the supported logics of an existing SMT solver by the supported logics of SMT-RAT. Further modules for closed quantifier-free formulas over the theory of fixed-size bitvectors (QF_BV) and quantifier-free formulas built over a signature of uninterpreted sort and function symbols (QF_UF) as well as combinations of these logics with already supported logics (QF_UFLRA, QF_UFLIA, QF_UFNRA, QF_UFNIA) are in progress.

We want to encourage developer of SMT compliant implementations of further procedures (for the supported or other logics) to use SMT-RAT as an SMT solving environment. We have tailored everything exactly towards this goal, for instance:

• the creation, integration and usage of a new module can be achieved automatically
• the developer only fills the core methods of a module and can make use of, e.g., the existing modules and a rich set of methods on polynomials and formulas
• we provide many useful features for the improvement of the implemented procedure:
• logging of assumptions of the satisfiability of occurring formulas to check their correctness later with other SMT solvers
• quality-check of generated infeasible subsets (how small is it?)
• statistics collection
• generic infrastructure for settings
• built-in delta debugging

SMT-RAT provides a graphical user interface (GUI) for the creation of a strategy specifying how to combine modules to a theory or SMT solver. The strategy specifies dynamically which modules have to solve a given formula, involving the formula's properties and the solving history.

Documentation

• You can either follow this wiki,

1. System Architecture
2. Constructing Formulas
3. Embedding of an SMT-RAT Solver Composition
4. Implementing Further Modules
5. Composing a Solver
6. Further Features

• read our manual or

• use the doxygen-generated documentation.

Installation

For Linux and Mac OS 64 Bit machines, executable binaries of SMT-RAT with four different strategies can be found here. Examples of SMT-LIB files can be found at the SMT-LIB webpages or here.

For the installation of SMT-RAT look either into the README, the manual, here or follow these instructions:

Download a stable release of SMT-RAT here or clone the newest (possibly non-stable) version of SMT-RAT:

git clone https://github.com/smtrat/smtrat.git

Prerequisites

• A C++ compiler with C++11x capabilities. We assume GCC 4.8 or higher.
• The build system CMake: http://www.cmake.org/ (only for building the library)
• The library CArL: https://github.com/smtrat/carl (formula and polynomial data structures and basic operation)

Optional dependencies

• The library GiNaC: http://www.ginac.de/ (if usage of polynomial factorization is enabled, which is recommended for solving QF_NRA and QF_NIA formulas with SMT-RAT)
• The documentation build system Doxygen: http://www.stack.nl/~dimitri/doxygen/
• The build system Ant: http://ant.apache.org/ (only for building the gui)
• A Java development environment >= 1.6: http://www.oracle.com/technetwork/java/index.html (only for building the gui)

How to build the project including library and the solver

Create a separate build directory.

 mkdir build
 cd build

Configure using cmake.

 cmake ..

For an interactive user interface with more options.

 ccmake ..

Build the project, in particular, build the solver smtrat.

 make

Other targets to build

Show a list of possible targets.

 make help

Force the build system to re-build everything.

 make clean

Install library to the specified (adjust via ccmake) system directory.

 make install

Make the java-based GUI.

 make build-gui

Make/run the java-based GUI.

 make run-gui

Construct a package of the project.

 make package

Build the project API documentation.

 make doc

Run the solver

The excecutable solver smtrat can be found in the build directory. It accepts .smt2 files as described by smtlib.

For more information, run

 ./smtrat --help

To run the solver on an inputfile input.smt2 run

 ./smtrat input.smt2