Home

SMT-RAT is an open source C++ toolbox for strategic and parallel SMT solving consisting of a collection of SMT compliant implementations of methods for solving quantifier-free (non)linear real and integer arithmetic (QF_LRA, QF_LIA, QF_NRA, QF_NIA) formulas, we refer to as modules. These modules can be combined to (1) an SMT solver or (2) a theory solver in order to extend the supported logics of an existing SMT solver by the supported logics of SMT-RAT. Further modules for closed quantifier-free formulas over the theory of fixed-size bitvectors (QF_BV) and quantifier-free formulas built over a signature of uninterpreted sort and function symbols (QF_UF) as well as combinations of these logics with already supported logics (QF_UFLRA, QF_UFLIA, QF_UFNRA, QF_UFNIA) are in progress.

We want to encourage developer of SMT compliant implementations of further procedures (for the supported or other logics) to use SMT-RAT as an SMT solving environment. We have tailored everything exactly towards this goal, for instance:

• the creation, integration and usage of a new module can be achieved automatically
• the developer only fills the core methods of a module and can make use of, e.g., the existing modules and a rich set of methods on polynomials and formulas
• we provide many useful features for the improvement of the implemented procedure:
• logging of assumptions of the satisfiability of occurring formulas to check their correctness later with other SMT solvers
• quality-check of generated infeasible subsets (how small is it?)
• statistics collection
• built-in delta debugging

SMT-RAT provides a graphical user interface (GUI) for the creation of a strategy specifying how to combine modules to a theory or SMT solver. The strategy specifies dynamically which modules have to solve a given formula, involving the formula's properties and the solving history.

Documentation

• You can either follow this wiki,

• read our manual or

• use the doxygen-generated documentation.

Installation

Look either into the README, the manual or here.

$i_1\neq i_2$