×

SMT-RAT

swMATH ID: 13091
Software Authors: Corzilius, F., Kremer, G., Junges, S., Schupp, S., Ábrahám, E.
Description: 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.
Homepage: https://github.com/smtrat/smtrat/wiki
Dependencies: CArL
Related Software: SMT-LIB; CVC4; z3; QEPCAD; MathSAT5; REDLOG; raSAT; veriT; Yices; MiniSat; Mathematica; CoCoALib; AProVE; iSAT; SYNRAC; REDUCE; RegularChains; CalCS; StarExec; CArL
Referenced in: 18 Publications

Referencing Publications by Year