Join GitHub today
GitHub is home to over 28 million developers working together to host and review code, manage projects, and build software together.Sign up
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.
- You can either follow this wiki,
- System Architecture
- Constructing Formulas
- Embedding of an SMT-RAT Solver Composition
- Implementing Further Modules
- Composing a Solver
- Further Features
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
- 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)
- 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.
For an interactive user interface with more options.
Build the project, in particular, build the solver
Other targets to build
Show a list of possible targets.
Force the build system to re-build everything.
Install library to the specified (adjust via ccmake) system directory.
Make the java-based GUI.
Make/run the java-based GUI.
Construct a package of the project.
Build the project API documentation.
Run the solver
The excecutable solver smtrat can be found in the build directory. It accepts
.smt2 files as described by SMT-LIB.
For more information, run
To run the solver on an inputfile