SMT-RAT

		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: gcc/g++ version >= 4.3.2 flex bison autoreconf libtool (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: bouncing ball etcs rectangular positioning zankl How to use SMT-RAT? ← A detailed description of SMT-RAT can be found in the SMT-RAT manual.
	Contact ← Florian Corzilius Ulrich Loup
		Last Update: