mwillsey
commented
2 months ago Yes, associativity (especially together with commutativity) are known to blow up the e-graph. There are various strategies to control this, but they basically amount to artificial limitations on the equality saturation process.
The problem is that equality saturation not only reasons about the (sub)terms that you give it, but it creates many new terms along the way (terms that are not equivalent to anything in the input) and reasons about them too! Associativity is a good example: once you rewrite a + (b + c) to (a + b) + c, you've made a new term a + b that is not equivalent to anything in the input!
This problem is particularly bad with associativity, because you're discovering a million new ways to rewrite 0. So one approach people take is to prune 0's e-class:
#[test]
fn foo() {
#[derive(Default)]
struct MyAnalysis;
type EGraph = egg::EGraph<SymbolLang, MyAnalysis>;
impl Analysis<SymbolLang> for MyAnalysis {
type Data = ();
fn make(egraph: &mut EGraph, enode: &SymbolLang) -> Self::Data {
()
}
fn merge(&mut self, a: &mut Self::Data, b: Self::Data) -> DidMerge {
DidMerge(false, false)
}
fn modify(egraph: &mut EGraph, id: Id) {
let nodes = &mut egraph[id].nodes;
if nodes.iter().any(|n| n.is_leaf()) {
nodes.retain(|n| n.is_leaf());
}
}
}
let mut rules: Vec<Rewrite<SymbolLang, MyAnalysis>> = vec![];
rules.push(rewrite!("commute-add"; "(+ ?x ?y)" => "(+ ?y ?x)"));
rules.extend(rewrite!("assoc-add"; "(+ (+ ?x ?y) ?z)" <=> "(+ ?x (+ ?y ?z))"));
rules.push(rewrite!("cancel-add-neg"; "(+ ?x (- ?x))" => "0"));
rules.push(rewrite!("add-0"; "(+ ?x 0)" => "?x"));
let expr = "(+ a (+ b (- a)))";
let runner = Runner::default()
.with_explanations_enabled()
.with_expr(&expr.parse().unwrap())
.with_node_limit(64)
.run(&rules);
runner.print_report();
let mut egraph = runner.egraph;
println!("Generated classes:");
for class in egraph.classes() {
println!(" {}", egraph.id_to_expr(class.id));
}
println!("Explanation for final generated class:");
let newest_id = egraph.classes().map(|c| c.id).max().unwrap();
let newest_expr = egraph.id_to_expr(newest_id);
println!(
"{}",
egraph.explain_existance(&newest_expr).get_flat_string()
);
}All I have done here is add a trivial e-class analysis that does nothing, except for use the modify hook to prune any e-class that has leaf e-nodes in it. This works on the assumption that once you prove something equivalent to a constant/variable, you don't need to rewrite it any further.
KarelPeeters
yihozhang
Hey! Thanks for doing the equivalence graph research and building this crate as an implementation.
I'm investigating how easy it is to use
eggas part of the integer range type system for an experimental language I'm working on. Right now I'm trying to see fast achieving saturation is for simple arithmetic expressions, only involving addition and negation. This is the full test code I'm running:This already explodes, without a node or time limit the graph keeps growing forever (as far as I can tell). The set of rules I included here is minimal: removing any single rule fixes the "exploding graph" problem, at the cost of severely reducing expressiveness. This is the shortened output of running this program with all 4 rules:
To me it looks like it keeps generating new classes that are equivalent to classes it already knows about, faster than it can prove that they are indeed equivalent. For example, the final class that is printed,
(+ (+ (+ a b) a) (+ (- a) (+ (- a) (- a))))), is really just(+ b (- a))again, but they have not yet been proven to be the same.I'm surprised by steps like
(Rewrite<= add-0 (+ b 0))being included in the existence reason. I defined the one-directional rewriterewrite!("add-0"; "(+ ?x 0)" => "?x"), why is it being used in the opposite direction too? Is it expected behavior that simple sets of rules already blow up the graph forever?