Predicate E-Graphs with Symbolic Conditional Rewriting
summary
Defines predicate e-graphs that attach Boolean fact-sets to colors and maintain a dynamic pre-order that approximates implication; supports adding edges and colors, merging colors when fact-sets become equivalent, and uses union-find canonicalization to collapse equivalent color cycles. Demonstrates conditional rewriting on an example where A≤0 and A≥0 produce A=0, and introduces symbolic matching to create least-upper-bound colors for multi-condition rewrites. No implementation yet; goal is enabling more conditional Erlang optimizations.
AI-written summary · about
chapters (12)
- 0:00Introduction
- 0:20Motivation for predicate e-graphs
- 1:24E-graphs and colored e-graphs
- 2:48Generalizing to predicate e-graphs
- 4:33Formal definition
- 6:00Operations on e-graphs
- 7:46Example with lattice
- 9:13Conditional rewriting
- 10:38Equivalent facts and optimizations
- 11:00Symbolic matching
- 11:43Summary and future
- 12:48Q&A
related talks
38mE-graphs and Automated Reasoning: Looking back to look forward
23mVersioned E-Graphs
22mAutomated Proof Generation for Associative and Distributive Rewriting with E-Graphs
20mSlotted E-Graphs: First-Class Support for (Bound) Variables in E-Graphs
35mOmelets Need Onions: E-graphs Modulo Theories via Bottom Up E-Matching
30mA Novel EGs-Based Framework for Systematic Propositional-Formula Simplification
19mDestructive E-Graph Rewrites
28mBridging Syntax and Semantics of Lean Expressions in E-Graphs