Sharing is Caring: Combination of Theories

by Dejan Jovanović, Clark Barrett
Abstract:
One of the main shortcomings of the traditional methods for combining theories is the complexity of guessing the arrangement of the 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:
Sharing is Caring: Combination of Theories (Dejan Jovanović, Clark Barrett), In Proceedings of the 8th International Symposium on Frontiers of Combining Systems (FroCoS ’11) (Cesare Tinelli, Viorica Sofronie-Stokkermans, eds.), Springer, volume 6989, 2011. (Saarbrücken, Germany)
Bibtex Entry:
@inproceedings{JB11-FroCoS,
  url       = "http://www.cs.stanford.edu/~barrett/pubs/JB11-FroCoS.pdf",
  author    = "Dejan Jovanović and Clark Barrett",
  title     = "Sharing is Caring: Combination of Theories",
  booktitle = "Proceedings of the 8th International Symposium on Frontiers of Combining Systems (FroCoS '11)",
  series    = "Lecture Notes in Computer Science",
  volume    = 6989,
  publisher = "Springer",
  editor    = "Cesare Tinelli and Viorica Sofronie-Stokkermans",
  pages     = "195--210",
  month     = oct,
  year      = 2011,
  note      = {Saarbr"{u}cken, Germany},
  category  = "Conference Publications",
  abstract  = "One of the main shortcomings of the traditional methods for combining theories is the complexity of guessing the arrangement of the 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