SMT-RAT  19.10
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. The documentation comes in three flavours:

  • API documentation as HTML: the regular web-based doxygen documentation is generated by make doc-apidoc-html into build/doc/apidoc-html/ and online at
  • API documentation as PDF: (almost) the full doxygen documentation as a pdf file is generated by make doc-apidoc-pdf into build/doc/doc_smtrat-*.pdf and online here.
  • Manual as PDF: only the manual, suitable for reading as an introduction into SMT-RAT, is generated by make doc-manual into build/doc/manual_smtrat-*.pdf and online here.

Note that all the information of the manual is contained in the API documentation (both HTML and PDF) as well. It is much more compact, though, and may thus be more approachable as an introduction. However, references to classes do not work in the manual (as the class documentation is not contained).

If you are new to SMT-RAT and want to have a look around, we recommend reading the manual. The full API documentation can be found either online, or in the pdf documentation.

If you want to use SMT-RAT and want to know how to get and install it, have a look at Installation. 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 information. 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!