Nested patterns

[skius]

Hi!

While trying to find rewrites to aid SMT solving, I had the thought of "nested patterns" (or maybe "scoped rewrites"). As an example:

rw!("eq-subst", "(& (= ?x ?y) ?z)" => scoped!("?z")("?x" => "?y"))

This would apply the rewrite ?x => ?y, but only to the expression that was matched by ?z.

Is it possible to implement this functionality with the existing Searcher/Applier traits? The problem I'm facing is that I can only seem to search a whole egraph, instead of just the induced subgraph by ?z.

EDIT:
This rewrite rule would allow for rewrites like the following:

(& (= a (+ b 1)) (< c (^ 2 a))) 
  => 
(& (= a (+ b 1)) (< c (^ 2 (+ b 1)))) 

// in math notation:
a = b + 1 & c < 2^a 
  =>
a = b + 1 & c < 2^(b+1)

[mwillsey]

This is an interesting concept, could you supply an example (perhaps by editing the post)? I'm not sure I fully understand the use case from "This would apply the rewrite ?x => ?y, but only to the expression that was matched by ?z."

[skius]

Edited!

[mwillsey]

Ah ok I see what you're saying. This is basically substitution, so the lambda example might be your best bet. Unfortunately, the explicit substitution representation is clunky and slow. How to do this better (or really any "contextual" operation in the e-graph) is a topic of current research. Let me know if you have any ideas!

[skius]

Thanks for clearing that up.

I poked around for a bit, however my untrained eyes weren't able to find anything. I did try for a bit to get something to work with Pattern::search_eclass, however I got stuck at "transfering" the substitution info about ?x from the original match, and then only applying it to one eclass in Pattern::apply_one.