[Feature Request] Checkpoints/expression removal/incremental rewriting

[Kixiron]

It'd be really nice to support incremental rewrites of some sort, then egg could function as a library underlying a more complex incremental solver
I'm thinking something along these lines

let mut graph = ...;

let expr_id = graph.add(some_expr);
// ...do some things with the egraph

// Undo everything that dealt with the given enode
graph.remove(expr_id);

I know this is much easier said than done given the deduplicating nature of the egraph, but it's a neat idea none the less

[mwillsey]

What are the semantics of remove? I'm not clear from the givne example.

Would an SMT-style, push and pop meet your needs?

(also, converted from issue to discussion, as this is a ways out)

[Kixiron]

Yah, push/pop would be perfect, that's what I was thinking about with "checkpoints", I should have been more explicit

[yihozhang]

This sounds interesting. I'm thinking about backtrackable e-graphs a lot recently following this paper. I would like to experiment a little bit and see how this would look like in egg. Could you describe your potential usage (and background) in more details?

[Kixiron]

My use case is basically an incremental SMT solver, you want to be able to add and remove terms to be able to (for example) add terms when entering a branch of a program you're validating and then later remove them once you exit the branch

[yihozhang]

Here is a proof-of-concept persistent union-find I wrote during the last few days, although I'm not quite sure which direction that repo will end up going,

[mwillsey]

The ena crate used in rustc has a unionfind that supports snapshots: https://docs.rs/ena/latest/ena/index.html