Destructive rewriting in egglog ?
Opened this issue · 1 comments
Hi, is there a notion of destructive rewrite rules in egglog ? i.e. rules that delete their antecedent from the e-class after they've been applied ?
Is deleting from an e-class cheap enough that this could be implemented as a new type of rule ?
Imagine applying negative normal form conversion through rewrite rules, where you'll want to push negations down using (not (and x y)) ~~> (or (not x) (not y)) and never look back, deleting (not (and x y) forever.
Yes you can use delete or subsume. subsume is like delete, but it will leave the term in the database, but will never match on it again and you can't extract it. So it's useful if you want to make sure a term can never re-appear, whereas with delete you can re-add it later.