<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

Online veröffentlicht: 29. Aug. 2018

Seitenbereich: 5 - 25

Eingereicht: 15. Mai 2018

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

Schlüsselwörter
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

Online veröffentlicht: 29. Aug. 2018

Seitenbereich: 5 - 25

Eingereicht: 15. Mai 2018

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

Schlüsselwörtersatisfiability 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.

Schlüsselwörter
satisfiability modulo theories, polynomial arithmetic, strategic combination