Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Fixes #188
I think I was able to get a decent version of push/pop working. I added a few tests for it but it may still be buggy, so we should probably add some more before merging this.
I added an associate type
UndoLogto theAnalysistrait to allow users to opt-in to the extra cost tracking this information. Ideally, it would default to()which restores the old behaviour, but unfortunately, associated type defaults are not stable so this is a breaking change. This idea could also be used for explanations so calling an explanation-related method when explanations are disabled would be a compile-time error rather than a run-time error.Calling
popcurrently requires explanations to be enabled since it usesid_to_node, theUndoLogcould store its own copy of this information but this would be redundant if explanations and push/pop were both enabled. Another idea would be to store each uncanonical id's original node directly in the egraph, this would allow us to avoid storing nodes inEClass.parents,EGraph.pending, andEGraph.analysis_pending, eliminateExplainNode.node, and make theEgraph::id_to_Xmethods not require explanations to be enabled. Would it be worth doing a separate PR for this first?Calling
popalso currently requires that the analysis doesn't do anything, as I am still trying to figure out the best way to revert an arbitrary merge implementation.Calling
pushrequirespending/analysis_pendingto be empty, users can deal with this by callingrebuildbeforepushbut technically callingprocess_unionsis sufficient. I've been wondering if it is worth makingprocess_unionspublic sincerebuild_classesis only necessary forSearchers. This would also allowpopto be optimized for the case whererebuild_classeshasn't been called since the lastpush.