Merged
Conversation
oflatt
commented
Feb 11, 2022
| self[child].parents.push(tup); | ||
| }); | ||
| // now that we updated explanations, run the analysis for the new eclass | ||
| N::modify(self, id); |
Member
Author
There was a problem hiding this comment.
@mwillsey it is key that we do modify after all the explanations stuff, so this version is different than the one we discussed.
oflatt
commented
Feb 11, 2022
| // TODO is this needed? | ||
| self.pending.push((enode.clone(), id)); | ||
| /// This function makes a new eclass in the egraph (but doesn't touch explanations) | ||
| fn make_new_eclass(&mut self, enode: L) -> Id { |
Member
Author
There was a problem hiding this comment.
This is roughly the same as the old add
oflatt
commented
Feb 11, 2022
| rule_name: impl Into<Symbol>, | ||
| ) -> (Id, bool) { | ||
| let id1 = self.add_instantiation(from_pat, subst); | ||
| let id1 = self.add_instantiation_internal(from_pat, subst); |
Member
Author
There was a problem hiding this comment.
"Internal" functions now return uncanonicalized ids so we can track which enode explanations use.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.
[#115] Introduces explanations- proofs of equality between two terms in the egraph. To support the PR, egg was modified so that all unions were delayed until rebuild is called. This made explanations easier to implement because there is an up-to-date hashcons (memo for enodes in the egraph).
However, it turns out that carefully re-writing how enodes are added to the egraph avoids this issue. This PR restores egg's functionality to perform unions immediately. It also restores the rebuild algorithm to what it was before proofs were added. The core idea of the PR is to make sure that proofs have access to the correct uncanonicalized enode.