SMT-RAT
24.02
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:
make doc-apidoc-html
into build/doc/apidoc-html/
and online at https://ths-rwth.github.io/smtrat
.make doc-apidoc-pdf
into build/doc/doc_smtrat-*.pdf
and online here.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 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!