Authors: François Bobot, Stephane Graham-Lengrand, Bruno Marre and Guillaume Bury
Paper Information
Title: | Centralizing Equality Reasoning in MCSAT |
Authors: | François Bobot, Stephane Graham-Lengrand, Bruno Marre and Guillaume Bury |
Proceedings: | SMT Informal Proceedings |
Editors: | Rayna Dimitrova and Vijay D'Silva |
Keywords: | MC-SAT, Egraph, SMT-solving, automated reasonning |
Abstract: | ABSTRACT. 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. |
Pages: | 12 |
Talk: | Jul 13 11:00 (Session 86K) |
Paper: |