improve search graph docs, reset encountered_overflow between reruns
#142617
Conversation
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
rustbot
added
S-waiting-on-review
lcnr
commented
Jun 17, 2025
| // optimization. However, given that the proof tree will likely | ||
| // look similar to the previous iterations when reevaluating, it's | ||
| // better for caching if the reevaluation also starts out with `false` | ||
| encountered_overflow: false, |
There was a problem hiding this comment.
I've reworked this to use EvaluationResult as I've accidentally dropped heads from previous iterations while working on this change and it took me a bit to actually figure out what's going on. This now makes it clear that we need to track everything correctly.
lcnr
commented
Jun 17, 2025
| @@ -26,6 +26,10 @@ pub(super) struct StackEntry<X: Cx> { | |||
| /// The available depth of a given goal, immutable. | |||
| pub available_depth: AvailableDepth, | |||
|
|
|||
| /// Starts out as `None` and gets set when rerunning this | |||
| /// goal in case we encounter a cycle. | |||
| pub provisional_result: Option<X::Result>, | |||
There was a problem hiding this comment.
moving this field as this type is now all the immutable fields and then the mutable ones
lcnr
changed the title
encountered_overflow between rerunsencountered_overflow between reruns
This comment was marked as outdated.
This comment was marked as outdated.
also return `EvaluationResult` instead of the final `StackEntry` to make sure we correctly track information between reruns.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
I think this shouldn't really matter for now. It will be more relevant for my current rework as we otherwise cannot partially reevaluate the root goal in case there has been overflow during the prervious iteration.
r? @BoxyUwU