search

egraphs-good / egglog

egraphs + datalog!
https://egraphs-good.github.io/egglog/
MIT License
459 stars 54 forks source link

Destructive rewriting in egglog ? #411

Open remi-delmas-3000 opened 3 months ago

remi-delmas-3000 commented 3 months ago

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.

saulshanabrook commented 3 months ago

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.