<abstract xmlns="http://www.w3.org/1999/xhtml"><p>In this paper we present the latest developments in SMT-RAT, a tool for the automated check of quantifier-free real and integer arithmetic formulas for satisfiability. As a distinguishing feature, SMT-RAT provides a set of solving modules and supports their strategic combination. We describe our CArL library for arithmetic computations, the available modules implemented on top of CArL, and how modules can be combined to satisfiability-modulo-theories (SMT) solvers. Besides the traditional SMT approach, some new modules support also the recently proposed and highly promising model-constructing satisfiability calculus approach.</p></abstract>

In this paper we present the latest developments in SMT-RAT, a tool for the automated check of quantifier-free real and integer arithmetic formulas for satisfiability. As a distinguishing feature, SMT-RAT provides a set of solving modules and supports their strategic combination. We describe our CArL library for arithmetic computations, the available modules implemented on top of CArL, and how modules can be combined to satisfiability-modulo-theories (SMT) solvers. Besides the traditional SMT approach, some new modules support also the recently proposed and highly promising model-constructing satisfiability calculus approach.

Modular strategic SMT solving with SMT-RAT

Acta Universitatis Sapientiae, Informatica

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 License.

{"article-title":"Modular strategic SMT solving with SMT-RAT"}

In this paper we present the latest developments in SMT-RAT, a tool for the automated check of quantifier-free real and integer arithmetic formulas for...

Modular strategic SMT solving with SMT-RAT

Publié en ligne: 29 août 2018

Pages: 5 - 25

Reçu: 15 mai 2018

DOI: https://doi.org/10.2478/ausi-2018-0001

Mots clés
satisfiability modulo theories, polynomial arithmetic, strategic combination

© 2018 Gereon Kremer et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 License.

Modular strategic SMT solving with SMT-RAT

Publié en ligne: 29 août 2018

Pages: 5 - 25

Reçu: 15 mai 2018

DOI: https://doi.org/10.2478/ausi-2018-0001

Mots cléssatisfiability modulo theories, polynomial arithmetic, strategic combination

© 2018 Gereon Kremer et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 License.

Mots clés
satisfiability modulo theories, polynomial arithmetic, strategic combination