Decision Procedures for Recursive Data Structures with Integer Constraints
Ting Zhang,
Henny B. Sipma,
Zohar Manna
Abstract
This paper is concerned with the integration of recursive data
structures with Presburger arithmetic. The integrated theory includes
a length function on data structures, thus providing a tight coupling
between the two theories, and hence the general Nelson-Oppen
combination method for decision procedures is not applicable to this
theory, even for the quantifier-free case. We present four decision
procedures for the integrated theory depending on whether the language
has infinitely many constants and whether the theory has quantifiers.
Our decision procedures for quantifier-free theories are based on
Oppen's algorithm for acyclic recursive data structures with infinite
atom domain.
