GeezerVison

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 `to`
does not name (`AuxStateHandler.addOldStates` adds `stateK(this) ==
stateK(old(this))`). Different state sets are different ghost functions.
So:

- **Entry.** Whether a `from` holds 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`).
- **States after.** The only candidates are those that keep the sets
`to` does not name. Where the call leads in the sets it does name
depends only on the state before in the sets it names for `old(this)`,
so that answer is reused across states (`statesAfter`,
`SolverEffects.computeAfter`).
- **Guards.** If the receiver can be in any combination of states, a
guard whose state or return refinements name no state of the sets the
failing call checks cannot change them. It is skipped before any query.

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)
| | #474 | this PR |
|---|---|---|
| Solver queries (whole file) | 1419 | 258 |
| Machine build (entry + states after) | 951 | 187 |
| Hint queries | 432 | 35 |
| Wall time, whole run (3 runs) | 10.0–10.2 s | 5.0–6.1 s |

## Checks
- **Same output.** On every test-suite path and every fixture project
under `liquidjava-dev/fixtures`, errors and hints are identical to #474.
- **Sweep time.** The test suite went from 1m25s to 1m07s and the
fixtures from 25 s to 17 s.
- **Full suite.** Passes locally: 685 tests, 0 failures.
- **New unit tests** in `StateMachineTest` for `namedSets`,
`namedSetsBefore` (only `old(this)` mentions count), the alias case and
`keeping`.
- **A bug the sweep caught.** Query guards such as `hasNext()` with `_
== hasMore(this)` keep their state in the return refinement, so the
guard filter now looks there too. Before this fix, it dropped the
`hasNext()`, `canUndo()` and `!isDisplayable()` guards.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5.5 <[email protected]>

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 <[email protected]>