Repository navigation
Ask the solver only about the state sets a refinement names - #475
Merged
Merged
Conversation
Collaborator
Author
|
[Codex review] I reviewed the state-set lookup, the cache keys for entry and resulting states, and the guard prefilter against #474. The change preserves unnamed state sets and treats aliases conservatively. I found no correctness issue in this diff; CI is green. This PR is stacked on #474, where I left a separate guard-text comment. |
CatarinaGamboa
force-pushed
the
state-hints-relevant-guards
branch
from
November 4, 2026 15:15
0dfbcd5 to
54abd0f
Compare
The verifier keeps the state of every set a refinement's to does not name, and the states of different sets are different ghost functions. So: - whether a from holds is asked once per state of the sets it names; - the states a call can lead to are only those that keep the other sets, and are asked once per state of the sets its to names for old(this); - a guard whose refinements name no state of the sets the failing call checks is not tried when the receiver can be in any combination of states. On the study's UndoManager this takes 1419 queries to 258, with the same hints. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
CatarinaGamboa
changed the base branch from
state-hints-guards-and-argument-conditions
to
main
November 4, 2026 16:19
CatarinaGamboa
force-pushed
the
state-hints-relevant-guards
branch
from
November 4, 2026 16:19
54abd0f to
bc2ad0c
Compare
CatarinaGamboa
added a commit
that referenced
this pull request
Nov 4, 2026
Closes #482. ## What With more than one `@StateSet`, the call-sequence hint named every state set, including the ones the suggested calls leave as they are. It now names only the sets whose states differ before and after the calls. Only the displayed hint changes; no solver query changes. Reproducer from the issue: ``` before: Call s.mark() before this call to move s from open and unmarked to open and marked after: Call s.mark() before this call to move s from unmarked to marked ``` Existing fixture `ErrorStateHintMultipleSets`: ``` before: Call d.unlock() before this call to move d from closed and locked to closed and unlocked after: Call d.unlock() before this call to move d from locked to unlocked ``` ## How - `StateMachine.stateSetsChanged(before, after)`: the sets whose states differ. If the sets it would leave out, taken together, differ too (how states of different sets are combined changed), every set is named, as before. - `StateMachine.describeOnly(subset, sets)`: names `subset` only in the given sets, reusing `StateCover` (the naming from #474/#475) on the states that agree with `subset` in those sets. - `StateHints.callSequence` names both sides with these. `from any state` is unchanged. ## Not changed, on purpose - **`In state open and unmarked, s can call: mark()`** still names the full state: which calls are allowed depends on every set, so dropping `open` would make the hint less accurate. - **Found/expected** (`found open(s) && unmarked(s) but expected marked(s) && open(s)`) is left as it is. These are the verifier's real predicates (the simplified premise chain and the `from` disjunction, with arguments, ghosts and aliases). The IDE reads them too. Dropping or reordering conjuncts that hold on both sides would need a semantic check on arbitrary predicates. Doing that only for display is riskier than this PR should be. It could be a follow-up if the study needs it. ## Tests - `TestStateHints.callSequenceNamesOnlyTheStateSetsItChanges` (the renamed multi-set test; fails on main). - `StateMachineTest`: `statesAreNamedOnlyInTheSetsShown`, `setsChangedAreThoseWhoseStatesDiffer` (including the cases where how the sets are combined changes). - `mvn test`: 692 tests, 0 failures. No other expectation changed. The dcm4che hint (`from startCompression to compressionExplicit`) already named a single set. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
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
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.
Follow-up to #474, stacked on it: review and merge #474 first. The diff here is only the last commit.
What
State hints asked Z3 about every state set, even the ones a refinement never names. This PR stops asking about those sets and changes no hint.
The verifier already keeps the state of every set a refinement's
todoes not name (AuxStateHandler.addOldStatesaddsstateK(this) == stateK(old(this))). Different state sets are different ghost functions. So:fromholds depends only on the sets it names, so it is asked once for each state of those sets, not once for each of the 12 combined states. This is done both when building the state machine (StateMachineBuilder.transitionsOf) and for hint variants (SolverEffects.entry).todoes not name. Where the call leads in the sets it does name depends only on the state before in the sets it names forold(this), so that answer is reused across states (statesAfter,SolverEffects.computeAfter).An alias is assumed to name every set, because its body is not expanded at this point.
Numbers: the study's UndoManager (A1_56 fixture, 12 states in 3 sets)
Checks
liquidjava-dev/fixtures, errors and hints are identical to Suggest result checks and argument conditions in state hints #474.StateMachineTestfornamedSets,namedSetsBefore(onlyold(this)mentions count), the alias case andkeeping.hasNext()with_ == hasMore(this)keep their state in the return refinement, so the guard filter now looks there too. Before this fix, it dropped thehasNext(),canUndo()and!isDisplayable()guards.🤖 Generated with Claude Code