Fractional Collections with Cardinality Bounds, and Mixed Integer Linear Arithmetic with Stars

We present decision procedures for logical constraints that support reasoning about collections of elements such as sets, multisets, and fuzzy sets. Element membership in such collections is given by a characteristic function from a finite universe (of unknown size) to a subset of rational numbers specified by user-defined constraints in mixed linear integer-rational arithmetic. Our logic supports standard operators such as union, intersection, difference, or any operation defined pointwise using mixed linear integer-rational arithmetic. Moreover, it supports the notion of cardinality of the collection. Deciding formulas in such logic has application in verification of data structures. Our decision procedure reduces satisfiability of formulas with collections to satisfiability of formulas in an extension of mixed linear integer-rational arithmetic with an “unbounded sum” operator. Such extension is also interesting in its own right because it can encode reachability problems for a simple class of transition systems. We present a decision procedure for the resulting extension, using a satisfiability-preserving transformation that eliminates the unbounded sum operator. Our decidability result subsumes previous special cases for sets and multisets.