Abstract
We present SMT-RAT, a C++ toolbox offering theory solver modules for the development of SMT solvers for nonlinear real arithmetic (NRA). NRA is an important but hard-to-solve theory and only fragments of it can be handled by some of the currently available SMT solvers. Our toolbox contains modules implementing the virtual substitution method, the cylindrical algebraic decomposition method, a Gröbner bases simplifier and a general simplifier. These modules can be combined according to a user-defined strategy in order to exploit their advantages. © 2012 Springer-Verlag.
Cite
CITATION STYLE
Corzilius, F., Loup, U., Junges, S., & Ábrahám, E. (2012). SMT-RAT: An SMT-compliant nonlinear real arithmetic toolbox (Tool presentation). In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7317 LNCS, pp. 442–448). https://doi.org/10.1007/978-3-642-31612-8_35
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
