Combining Non-stably Infinite, Non-first Order Theories

AbstractA crucial step in the assertional verification of concurrent programs is deciding whether some sets of literals are satisfiable or not. In this context, the Nelson-Oppen combination scheme is often used. This scheme combines decision procedures for two disjoint theories into a decision procedure for the union of these theories. However, the standard version of the Nelson-Oppen technique tackles only one-sorted, stably infinite first-order theories. The scheme has previously been adapted to a many-sorted framework [C. Tinelli and C. G. Zarba. Combining decision procedures for theories in sorted logics. Technical Report 04-01, Department of Computer Science, The University of Iowa, Feb. 2004], and to handle non-stably infinite theories [C. Tinelli and C. G. Zarba. Combining non-stably infinite theories, in: I. Dahn and L. Vigneron, editors, Proceedings of the 4th International Workshop on First Order Theorem Proving, FTP'03 (Valencia, Spain), Electronic Notes in Theoretical Computer Science 86.1 (2003), Elsevier Science Publishers]. Those two enhancements were presented independently. We propose a unifying version in the continuity of both previous ones, which further relaxes the stably infinite requirement. Notably, some non-stably infinite theories can now be combined with the theory of arrays. Also, the combination scheme is presented here using a semantic notion of theory, allowing to handle non-first order theories