SMT-RAT
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.
Keywords for this software
References in zbMATH (referenced in 19 articles , 1 standard article )
Showing results 1 to 19 of 19.
Sorted by year (- Ábrahám, Erika; Davenport, James H.; England, Matthew; Kremer, Gereon: Deciding the consistency of non-linear real arithmetic constraints with a conflict driven search using cylindrical algebraic coverings (2021)
- Kruff, Niclas; Lüders, Christoph; Radulescu, Ovidiu; Sturm, Thomas; Walcher, Sebastian: Algorithmic reduction of biological networks with multiple time scales (2021)
- Kremer, Gereon; Ábrahám, Erika: Fully incremental cylindrical algebraic decomposition (2020)
- Borralleras, Cristina; Larraz, Daniel; Rodríguez-Carbonell, Enric; Oliveras, Albert; Rubio, Albert: Incomplete SMT techniques for solving non-linear formulas over the integers (2019)
- Hong, Hoon; Sturm, Thomas: Positive solutions of systems of signed parametric polynomial inequalities (2018)
- Kremer, Gereon; Ábrahám, Erika: Modular strategic SMT solving with \textbfSMT-RAT (2018)
- Vale-Enriquez, Fernando; Brown, Christopher W.: Polynomial constraints and unsat cores in \textscTarski (2018)
- Jovanović, Dejan: Solving nonlinear integer arithmetic with MCSAT (2017)
- Ábrahám, Erika; Abbott, John; Becker, Bernd; Bigatti, Anna M.; Brain, Martin; Buchberger, Bruno; Cimatti, Alessandro; Davenport, James H.; England, Matthew; Fontaine, Pascal; Forrest, Stephen; Griggio, Alberto; Kroening, Daniel; Seiler, Werner M.; Sturm, Thomas: \textsfSC(^2): satisfiability checking meets symbolic computation. (Project paper) (2016)
- Eraşcu, Mădălina: Efficient simplification techniques for special real quantifier elimination with applications to the synthesis of optimal numerical algorithms (2016)
- Kremer, Gereon; Corzilius, Florian; Ábrahám, Erika: A generalised branch-and-bound approach and its application in SAT modulo nonlinear integer arithmetic (2016)
- Maréchal, Alexandre; Fouilhé, Alexis; King, Tim; Monniaux, David; Périn, Michael: Polyhedral approximation of multivariate polynomials using Handelman’s theorem (2016)
- Tung, Vu Xuan; Khanh, To Van; Ogawa, Mizuhito: raSAT: an SMT solver for polynomial constraints (2016)
- Abraham, Erika: Building bridges between symbolic computation and satisfiability checking (2015)
- Corzilius, Florian; Kremer, Gereon; Junges, Sebastian; Schupp, Stefan; Ábrahám, Erika: \textttSMT-RAT: an open source \textttC++ toolbox for strategic and parallel SMT solving (2015)
- Jaroschek, Maximilian; Dobal, Pablo Federico; Fontaine, Pascal: Adapting real quantifier elimination methods for conflict set computation (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) ioport