FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Centralizing Equality Reasoning in MCSAT

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: