Politeness and Combination Methods for Theories with Bridging Functions
Résumé
The Nelson-Oppen combination method is ubiquitous in Satisfiability
Modulo Theories solvers. However, one of its major drawbacks is to
be restricted to disjoint unions of theories. We investigate the
problem of extending this combination method to particular
non-disjoint unions of theories defined by connecting disjoint
theories via bridging functions. A possible application is to solve
verification problems expressed in a combination of data structures
connected to arithmetic with bridging functions such as the length
of lists and the size of trees. We present a sound and complete
combination method à la Nelson-Oppen for the theory of absolutely
free data structures, including lists and trees. This combination
procedure is then refined for standard interpretations. The
resulting theory has a nice politeness property, enabling
combinations with arbitrary decidable theories of elements. In
addition, we have identified a class of polite data structure
theories for which the combination method remains sound and
complete. This class includes all the subtheories of absolutely
free data structures (e.g, the empty theory, injectivity,
projection). Again, the politeness property holds for any theory in
this class, which can thus be combined with bridging functions and
arbitrary decidable theories of elements. This illustrates the
significance of politeness in the context of non-disjoint combinations
of theories.
Origine : Fichiers produits par l'(les) auteur(s)
Loading...