Satisfiability Modulo Theories (SMT) can be seen as an extended form of propositional satisfiability, where propositions are either simple boolean propositions or quantifier-free atomic constraints, in a specific theory. In this paper we present MathSAT version 3, a DPLL-based decision procedure for the SMT problem for various theories, including those of Equality and Uninterpreted Functions, of Separation Logic, and of Linear Arithmetic on Reals and on the integers
The Mathsat3 System
Bozzano, Marco;Bruttomesso, Roberto;Cimatti, Alessandro;Sebastiani, Roberto
2005-01-01
Abstract
Satisfiability Modulo Theories (SMT) can be seen as an extended form of propositional satisfiability, where propositions are either simple boolean propositions or quantifier-free atomic constraints, in a specific theory. In this paper we present MathSAT version 3, a DPLL-based decision procedure for the SMT problem for various theories, including those of Equality and Uninterpreted Functions, of Separation Logic, and of Linear Arithmetic on Reals and on the integersFile in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
