Centralizing equality reasoning in MCSAT

François Bobot (1) , Stéphane Graham-Lengrand (2, 3) , Bruno Marre (1) , Guillaume Bury (4)

1 LSL - Laboratoire Sûreté des Logiciels
2 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
3 PARSIFAL - Proof search and reasoning with logic specifications
4 LSV - Laboratoire Spécification et Vérification [Cachan]

MCSAT is an approach to SMT-solving that uses assignments of values to first-order variables in order to try and build a model of the input formula. When different theories are combined, as formalized in the CDSAT system, equalities between variables and terms play an important role, each theory module being required to understand equalities and which values are equal to which. This paper broaches the topic of how to reason about equalities in a centralized way, so that the theory reasoners can avoid replicating equality reasoning steps, and even benefit from a centralized implementation of equivalence classes of terms, which is based on a equality graph (Egraph). This paper sketches the design of a prototype based on this architecture.

Domaines: Logique en informatique [cs.LO]

François Bobot, Stéphane Graham-Lengrand, Bruno Marre, Guillaume Bury. Centralizing equality reasoning in MCSAT. 16th International Workshop on Satisfiability Modulo Theories (SMT 2018), Jul 2018, Oxford, United Kingdom. ⟨hal-01935591⟩