Decision Procedures for Term Algebras with Integer Constraints
Ting Zhang,
Henny B. Sipma,
Zohar Manna
Abstract
Term algebras can model recursive data structures which
are widely used in programming languages.
To verify programs we must be able to reason about these structures.
However, as programming languages often involve multiple data domains,
in program verification decision procedures for a single theory are usually not applicable.
A natural example of such ``mixed'' constraints are combinations of data structures with integer constraints on the size of data structures.
In this paper we extend the theory of term algebras with the length function which maps a term to its size, resulting in a combined theory of term algebras and Presburger arithmetic.
This arithmetic extension provides a natural but tight coupling
between the two theories, and hence the general purpose combination methods
like Nelson-Oppen combination are not applicable.
We present decision procedures for quantifier-free theories in structures
with an infinite atom and with a finite constant domain, respectively.
We also present a quantifier elimination procedure for the extended first-order theory
that can remove a block of existential quantifiers in one step.
