2006 | OriginalPaper | Buchkapitel
To Ackermann-ize or Not to Ackermann-ize? On Efficiently Handling Uninterpreted Function Symbols in
verfasst von : Roberto Bruttomesso, Alessandro Cimatti, Anders Franzén, Alberto Griggio, Alessandro Santuari, Roberto Sebastiani
Erschienen in: Logic for Programming, Artificial Intelligence, and Reasoning
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Satisfiability Modulo Theories
$(\mathit{SMT}(\mathcal{T}))$
is the problem of deciding the satisfiability of a formula with respect to a given background theory
${\mathcal{T}}$
. When
${\mathcal{T}}$
is the combination of two simpler theories
${{\mathcal{T}}_1}$
and
${{\mathcal{T}}_2} ({\mathit{SMT}({{\mathcal{T}}_1\cup{\mathcal{T}}_2})})$
, a standard and general approach is to handle the integration of
${{\mathcal{T}}_1}$
and
${{\mathcal{T}}_2}$
by performing some form of search on the equalities between the shared variables.
A frequent and very relevant sub-case of
${\mathit{SMT}({{\mathcal{T}}_1\cup{\mathcal{T}}_2})}$
is when
${{\mathcal{T}}_1}$
is the theory of Equality and Uninterpreted Functions
$({\mathcal{EUF}})$
. For this case, an alternative approach is to eliminate first all uninterpreted function symbols by means of Ackermann’s expansion, and then to solve the resulting
${\mathit{SMT}}({{\mathcal{T}}_2})$
problem.
In this paper we build on the empirical observation that there is no absolute winner between these two alternative approaches, and that the performance gaps between them are often dramatic, in either direction.
We propose a simple technique for estimating a priori the costs and benefits, in terms of the size of the search space of an
${\mathit{SMT}}$
tool, of applying Ackermann’s expansion to all or part of the function symbols.
A thorough experimental analysis, including the benchmarks of the SMT’05 competition, shows that the proposed technique is extremely effective in improving the overall performance of the
${\mathit{SMT}}$
tool.