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
UndoLog
to theAnalysis
trait 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
pop
currently requires explanations to be enabled since it usesid_to_node
, theUndoLog
could 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_X
methods not require explanations to be enabled. Would it be worth doing a separate PR for this first?Calling
pop
also 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
push
requirespending
/analysis_pending
to be empty, users can deal with this by callingrebuild
beforepush
but technically callingprocess_unions
is sufficient. I've been wondering if it is worth makingprocess_unions
public sincerebuild_classes
is only necessary forSearcher
s. This would also allowpop
to be optimized for the case whererebuild_classes
hasn't been called since the lastpush
.