SMT-RAT Logo

SMT-RAT  

The Satisfiability–Modulo–Theories  
Real Arithmetic Toolbox  

What is SMT-RAT?

Features

Download

How to install SMT-RAT?

Benchmarks

How to use SMT-RAT?

Contact

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).

Features  

  • A Java-based GUI for an easy configuration of new NRA theory solvers. New!
The current list of changes to SMT-RAT can be viewed here.

Download  

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.

  • Prepare the build directory:

    tar xf smtrat-*.tar.gz
    cd smtrat-*
    mkdir build
    cd build

  • If you use a newer version of GiNaCRA, it is required to apply this patch from the root directory of SMT-RAT (New!):

    patch -p1 < ../smtrat-0.2.0_ginacra-0.6.1.patch

  • Configure the source with cmake (alternatively with ccmake for a user interface variant):

    cmake ..

  • Build:

    make

  • Install (with superuser privileges):

    make install

In order to build the GUI, install Ant and Java and type:

make gui

In order to build the API documentation, install Doxygen and type:

make doc

Benchmarks  

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
cd opensmt-1.0.1_smtrat
autoreconf -i
mkdir build
cd build
../configure
make

After installation run

./opensmtSMTRAT EXAMPLE.smt2

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.

Contact  

Valid HTML 4.01 Transitional Valid CSS! Source code is styled by Jindent.

Last Update: