Deciding Extensions of the Theories of Vectors and Bags

摘要

Vectors and bags are basic collection data structures, which are usedfrequently in programs and specifications. Reasoning about these data structuresis supported by established algorithms for deciding ground satisfiability in thetheories of arrays (for vectors) and multisets (for bags), respectively. Yet, thesedecision procedures are only able to reason about vectors and bags in isolation,not about their combination. This paper presents a decision procedure for the combination of the theoriesof vectors and bags, even when extended with a function bagof bridging betweenvectors and bags. The function bagof converts vectors into the bags of their el-ements, thus admitting vector/bag comparisons. Moreover, for certain syntacti-cally restricted classes of ground formulae decidability is retained if the theoryof vectors is extended further with a map function which applies uninterpretedfunctions to all elements of a vector.