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.
In Proc. 2nd International Joint Conference on Automated Reasoning (IJCAR'04), LNCS 3097, pp 152-167, Springer Verlag, 2004.
Postscript, PDF (Extended version). © 2004, Springer Verlag.