System SMT RAT

SMT-RAT

People

Current: Erika Ábrahám, Jasper Nalbach, Valentin Promies

Previous: Gereon Kremer, Florian Corzilius, Rebecca Haehn, Sebastian Junges, Stefan Schupp

Short Description

SMT-RAT is an Open Source C++ Toolbox for Strategic and Parallel SMT (Satisfiability Modulo Theories) Solving, with focus on non-linear real arithmetic.

Capabilities

• Proving
• Model finding

Input Language

The input format is SMT-LIB 2.6. The language accepted by SMT-RAT corresponds to the quantifier-free fragment of non-linear real arithmetic.

Output

SMT-RAT follows the SMT-LIB reporting standard

Proof Format

SMT-RAT does only provide models for satisfiable formulas, according to the SMT-LIB standard.

Official Page

https://ths-rwth.github.io/smtrat/

Other relevant information

SMT-RAT participates to the annual SMT competition SMT-COMP.

SMT-RAT is open source (MIT license) and written in C++. Currently, only Linux is supported.

Status

Maintained

References

Florian Corzilius, Gereon Kremer, Sebastian Junges, Stefan Schupp and Erika Ábrahám. SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving. Proc. of SAT 2015, volume 9340 of Lecture Notes in Computer Science. DOI: 10.1007/978-3-319-24318-4_26.