What is SMT-RAT? ←
SMT-RAT is a C++ toolbox offering theory solver modules for the development of SMT solvers for nonlinear real arithmetic (NRA).
The current list of changes to SMT-RAT can be viewed here.
- A Java-based GUI for an easy configuration of new NRA theory solvers. New!
Get the last version on https://sourceforge.net/projects/smtrat/files/source/.
How to install SMT-RAT? ←
SMT-RAT has been tested under Xubuntu since 11.04, Gentoo, and ArchLinux.
Install the required packages: CMake, CLN, GiNaC, and GiNaCRA.
We recommend to build the project in a separate build directory. The following installation instructions are based on this recommendation.
In order to build the GUI, install Ant and Java and type:
In order to build the API documentation, install Doxygen and type:
We provide a modified OpenSMT variant, which can be used to run our benchmark sets. Its source is available here, a 64 bits Linux binary (x86_64) here (New version!).
Note that building OpenSMT from source requires the following software:
(for Ubuntu users
sudo apt-get install autoconf libtool g++ bison flex).
In order to build OpenSMT with SMT-RAT, build and install the SMT-RAT library so that you linker can find it.
Then, we recommend to follow these instructions:
tar xf opensmt-1.0.1_smtrat.tar.gz
After installation run
with EXAMPLE.smt2 being any example of the following benchmark sets:
How to use SMT-RAT? ←
A detailed description of SMT-RAT can be found in the SMT-RAT manual.