Being Careful about Theory Combination

by Dejan Jovanović, Clark Barrett
Abstract:
One of the main shortcomings of traditional methods for combining theories is the complexity of guessing the arrangement of variables shared by the individual theories. This paper presents a reformulation of the Nelson-Oppen method that takes into account explicit equality propagation and can ignore pairs of shared variables that the theories do not care about. We show the correctness of the new approach and present care functions for the theory of uninterpreted functions and the theory of arrays. The effectiveness of the new method is illustrated by experimental results demonstrating a dramatic performance improvement on benchmarks combining arrays and bit-vectors.
Reference:
Being Careful about Theory Combination (Dejan Jovanović, Clark Barrett), In Formal Methods in System Design, Springer US, volume 42, 2013.
Bibtex Entry:
@article {JB13,
   url       = "http://www.cs.stanford.edu/~barrett/pubs/JB13.pdf",
   author    = "Dejan Jovanović and Clark Barrett",
   affiliation = {New York University, New York, USA},
   title     = "Being Careful about Theory Combination",
   journal   = "Formal Methods in System Design",
   publisher = {Springer US},
   issn      = {0925-9856},
   volume    = 42,
   number    = 1,
   doi       = "10.1007/s10703-012-0159-z",
   keywords  = {Theory combination; Nelson-Oppen; Satisfiability modulo theories},
   pages     = "67--90",
   month     = feb,
   year      = 2013,
   category  = "Journal Articles",
   abstract  = "One of the main shortcomings of traditional methods for combining theories is
the complexity of guessing the arrangement of variables shared by the individual theories.
This paper presents a reformulation of the Nelson-Oppen method that takes into account
explicit equality propagation and can ignore pairs of shared variables that the theories do
not care about. We show the correctness of the new approach and present care functions
for the theory of uninterpreted functions and the theory of arrays. The effectiveness of the
new method is illustrated by experimental results demonstrating a dramatic performance
improvement on benchmarks combining arrays and bit-vectors."
}

Fork me on GitHub