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.
References in zbMATH (referenced in 4 articles , 1 standard article )
Showing results 1 to 4 of 4.
- Corzilius, Florian; Kremer, Gereon; Junges, Sebastian; Schupp, Stefan; Ábrahám, Erika: SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving (2015)
- Larraz, Daniel; Oliveras, Albert; Rodríguez-Carbonell, Enric; Rubio, Albert: Minimal-model-guided approaches to solving polynomial constraints and extensions (2014)
- Junges, Sebastian; Loup, Ulrich; Corzilius, Florian; Ábrahám, Erika: On Gröbner bases in the context of satisfiability-modulo-theories solving over the real numbers (2013)
- Corzilius, Florian; Loup, Ulrich; Junges, Sebastian; Ábrahám, Erika: SMT-RAT: an SMT-compliant nonlinear real arithmetic toolbox (tool presentation) (2012)