SMT-RAT  2.1.0
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving

This is the documentation of SMT-RAT, an Open Source C++ Toolbox for Strategic and Parallel SMT Solving. On this page, you can find introductory information on how to obtain and compile SMT-RAT and a traditional doxygen API documentation.

If you are new to SMT-RAT and want to have a look around, we recommend reading the manual.

If you want to use SMT-RAT and want to know how to get and install it, have a look at Getting Started. It covers the most important steps including obtaining the actual source code, obtaining dependencies, building the library and running our test suite.

If you already use SMT-RAT and want to dig deeper or submit new code, you can additionally browse in Developers' Guide. It contains information about supplementary features like our logging framework and some basic guidelines for our code like how we use doxygen.

Note that this documentation is, and will probably still be for quite some time, work in progress. If you feel that some topic that is important to you is missing or some explanation is unclear, please let us know!