Efficient way to get large expression into the e-graph

[saulshanabrook]

In the Python bindings we currently make a lot of top level let calls to try to add large expressions to the e-graph efficiently, as DAGs instead of trees. It might be nice to have an "official" way to do this for other end users. Some disadvantages of the current approach are that the let bindings show up in the extraction/visualization and also its slower than adding them in a rule since it rebuilds after each other.

If we changed expressions in Egglog AST to be DAGs (like termdags) then we could more efficiently do this directly, instead of making let bindings.

[saulshanabrook]

Another motivation for this would be if you want to easily extract, then create a new e-graph and re-add those terms, if you are using Rust you have to manually create let bindings for each of the terms, see this zulip conversation.

Instead if the AST contained termdags instead of expressions then it would be much easier to do this.

[saulshanabrook]

Probably need a concrete design proposal here. Talked about it a bit in the lab the thought was that the current rule/let binding workaround is good but awkward especially from rust/python when you are generating expressions. Like some kind of insert termdag helper or something.

[saulshanabrook]

I think it would be nice to have this in the egglog syntax, not just in the Rust API, both so that people can use who are just using egglog from CLI and also that rust/python code generating egglog can be saved and replayed as just egglog source.

One option I just thought about would be to try to implement this in experimental as a custom command. That way we wouldn't have to change the existing expr syntax, as a let* command that supports referencing other parts of the expression tree when parsing. So for example something like:

(let my_big_expr (Mul (Add x y) (Add x y))

;; equiv to

(let* my_big_expr (Mul (let _tmp_1 (Add x y)) _tmp_1_ ))

So it would let you make temporary labels inside the expression and then use those as variables.
Those wouldn't be added as other let bindings in the e-graph, but would only be used to add the expression efficiently.

I don't feel strongly about how you create new variables inside the expression and reference them. In the above example I used let and then the variable. But it could be something else like:

(let* my_big_expr (Mul (let-tmp 0 (Add x y)) (ref-tmp 0))

In the end I believe whatever the syntax is it has to be parsed as Exprs, based on how custom commands are set up. But then we can traverse those Exprs however we want.

[asglover]

Nice, I like that the egglog specification is similar to the datatype vs datatype* design, so it's intuitive how the feature will work.

I don't know enough about the language to know if let or the combo of let-tmp and ref-tmp is more appropriate. If it's not too much of an overload onlet` it might be nice to reuse it? Maybe the answer will appear during implementation.

And then on the rust api side, we could make this string and parse into a list of commands.

It would be nice if there was a convenience API that directly accepts a DAG-like object. But it doesn't seem like there's currently any convenience functions for things like let. So that's probably a different thing. Thanks for putting this together!

[asglover]

Maybe something to think about when choosing between the syntax proposals is how easy it would be to modify existing programs. It would be convenient if it were possible to wrap an existing sequence of let statements in a (let* .. ) but if it has to be more complex, that's not a problem

[oflatt]

Some discussion on zulip about how slow using global let bindings is currently
#egg/egglog > ✔ Adding expressions to egraph

[oflatt-claude]

Some measurements on global lets vs. the same construction inside a rule, relevant here and to the closed #836.

After #848 ("rebuild only when union find changes"), a chain of N global lets is now linear in N on the default backend — the quadratic "super slow" behavior is gone. It is still roughly 2x slower than building the same terms in a rule:

N (a (Wrap (Wrap … (Base 0))) chain, default backend)	global lets	same work in a rule
2000	0.10s	0.06s
4000	0.19s	0.10s
8000	0.37s	0.19s

The remaining ~2x is per-command overhead: each top-level action is typechecked, compiled into a one-shot rule, run, and merged separately, whereas a rule amortizes all of that into a single compiled execution. So the "it's slower than a rule, and the lets show up in extraction/visualization" point above still stands — fully closing it would want a batched/DAG insertion path rather than one command per node.

(Under the experimental relations-based term/proof encoding the per-let gap is larger, because there each global also gets its own view table. #957 removes one quadratic cost that shows up in that setting — merge_all resetting every table on each operation.)