Modular derivation of decision procedures for extensions of the algebraic theory of arrays

We investigate methods to automatically derive decision procedures for array theories using expressive features such as unbounded quantification or cardinality constraints from decision procedures for their indices and element theories. We observe that traditional methods such as the Nelson-Oppen combination procedure are severely limited in terms of the theories that can be used to specify elements or indices. We show that the polite theory combination method is already able to combine arbitrary element theories with theories of sets with cardinality constraints, which was left open in [1]. We also show that the polite theory combination approach is applicable for theories that mix set- and first-order specifications, provided that their signatures are disjoint. Finally, we show that for fragments with non-disjoint signatures, a reduction approach can be used to modularly combine arbitrary index and element theories. Our results provide a starting point for the analysis of the modular combination problem of expressive string or sequence theories.