On equations with incompatible sets of pvars #53
Description
We want to support equations like f(?x, ?z) = g(?y, ?z), i.e. where the sets of pvars are not necessarily the same on both sides of the equation.
These equations can't work as a simple egg rewrite rule, as matching against the lhs, doesn't produce a sufficient subst that is applicable to the rhs.
There are two parts to solving this:
1) The "compacting" part
Effectively, we want to match against Eq(lhs, lhs) /\ Eq(rhs, rhs) and add all corresponding equations lhs=rhs to our e-graph -- as Marcus pointed out.
Note that this is "compacting" as it cannot grow the e-graph, it just merges classes that already exist.
Matching against Eq(lhs, lhs) /\ Eq(rhs, rhs) directly might not always be super efficient, as it looks at the cartesian product of possibilities over what the pvars from the lhs might match against TIMES what the pvars from the rhs might match against.
Thus, we instead might want to ematch against both f(?x, ?z) (aka lhs) and g(?y, ?z) (aka rhs) individually, and then group the resulting matches by what they map ?z (or in general the intersection of pvars between lhs and rhs) to.
A match in this case is a (Subst, Side) pair, where enum Side { Lhs, Rhs }.
Then, all matches from the same group can be unioned.
Note that it is okay to union lhs with lhs, or rhs with rhs this way!
After all f(?x1, ?z) = f(?x2, ?z) is a consequence of f(?x, ?z) = g(?y, ?z), just like redundant slots from slotted e-graphs.
2) The "explosion" part
As the previous approach only merges terms that already exist.
When we want to do "explosion", we'd effectiely do
f(?x, ?z) -> g(a, ?z) for a bunch of e-classes a.
Although, this can quickly explode the e-graph. And it can easy generate non-wellformed terms for poor choices of a.
I could imagine that picking only a single a is sometimes useful.