How to check if a given EClass is a child of another EClass

[Kixiron]

Pretty much what the title says, I'm writing a condition that looks like if contains_clause("?clause", "?unit") where I want to check if ?clause contains ?unit anywhere (transitively), how would I go about doing that?

[pavpanchekha]

So, this is kind of a dangerous thing to do, because an eclass contains many equivalent terms. What if one of the equivalent terms does contain the unit and the other doesn't? You'll need to be able to answer this question.

Once you've done that, though, the first thing that comes to mind is an eclass analysis. It should store a boolean as the analysis value, return true for the unit eclass and for any enode that has it as an argument, and either do an and or an or on join.

If you want to do queries for various containments (as in, if ?unit isn't fixed in advance) then you'll probably need to do a full scan over the e-graph, which could get expensive.

[pavpanchekha]

After thinking about this a bit, I don't see a great "egraphy" way to do this. Perhaps others have an idea.

[Bastacyclop]

As an approximate solution, you could try extracting terms and performing the term-based simplification before merging it into the e-graph. I've used this for lambda calculus substitution and it worked surprisingly well in my use-case (https://arxiv.org/abs/2111.13040).

You could also rely on associativity + commutativity rules to simply apply (a ∨ ¬b)∧ b --> a∧ b? The downside is that the e-graph size is likely to blow up and the exponential backoff scheduler might be counterproductive. Maybe the work on Caviar can alleviate this (https://dl.acm.org/doi/abs/10.1145/3497776.3517781).

[mwillsey]

Indeed, this is a tricky problem. In essence, you are asking "is it possible to write x in terms of some other term y?", which might very well be possible in surprising ways if you have a full e-graph.

I think you could get away with an e-class analysis that tracks whether an e-class mentions some other term(s) of interest. Using a merge like set union should give you the right over-approximation. Note that this is answering "is it possible to write x in terms of y", not "is it guaranteed", which are two different things!

[Kixiron]

Well the big issue isn't really finding the sub-term, it's substituting it without totally breaking the graph

[mwillsey]

For substituting it, the only scalable approach I'm aware of is @Bastacyclop's extract-subst-add approach.