GeezerVison

Problem

After #459, Found still shows true rows for variables that another row already shows (#375):

• A1_56 (JabRef EditAction, state error): ∀getUndoManager true.
• A1_09 (PlayfieldWindow, state error): ∀previousMode true, ∀DisplayMode.BORDERLESS true and ∀newMode true, above the ternary that uses them.

#459 kept a true binder when a fact linked to Expected constrains its value. That fact is always a row the user already sees, and it already names the variable. So the extra true row adds no fact. It also reads as if the variable's value were true, which is what #375 is about. The A1_09 rows are not needed: the ternary row shows previousMode, newMode and BORDERLESS, and that row explains why host may still be displayable. DisplayMode.BORDERLESS is an enum constant, so a binder row for it says nothing.

Rule

A binder refined only by true is shown only when all of these hold:

1. the error is a refinement error, so it has a counterexample;
2. Expected constrains the variable's value;
3. no other row of Found mentions the variable.

When all three hold, the row is the only place the variable appears in Found. It tells the user that nothing is known about a value the error depends on (∀t true, counterexample t == 0). In every other case the row goes, because the variable is either shown in the rows that use it or not needed.

No variable disappears from what the user sees:

• A dropped binder's variable still appears in the rows that mention it.
• The counterexample is unchanged. RefinementError.filterCounterexample takes its terms from Expected and from Found's facts, not from the binders, so for example Basket.served == -1 still shows after its row goes.

NeededVariables no longer links facts to Expected. Two pieces of code had no other use, so this PR removes them:

• splitConjuncts and linkedConjuncts in VCSimplificationUtils;
• the VCBinderOrdering pass and its test. That pass only moved kept true binders before their first use. A kept binder now has no other use, so the pass could never fire.

Before / after

A1_56 (undoManager.redo() on a manager from a getter)

before: ∀getUndoManager¹²⁹   true
        ∀#fresh¹¹²           !#fresh¹¹¹
        ∀#fresh¹²⁶           !(#fresh¹²⁴ || #fresh¹²⁵)
        ∀undoManager¹³¹      undoManager¹³¹ == getUndoManager¹²⁹
after:  ∀#fresh¹¹²           !#fresh¹¹¹
        ∀#fresh¹²⁶           !(#fresh¹²⁴ || #fresh¹²⁵)
        ∀undoManager¹³¹      undoManager¹³¹ == getUndoManager¹²⁹

A1_09 (host.setUndecorated(true) after a conditional dispose())

before: ∀previousMode            true
        ∀DisplayMode.BORDERLESS  true
        ∀newMode                 true
        ∀host¹²¹   previousMode == BORDERLESS && newMode != BORDERLESS ? notDisplayable(host¹²¹) : (previousMode != BORDERLESS && newMode == BORDERLESS ? notDisplayable(host¹²¹) : displayable(host¹²¹))
after:  ∀host¹²¹   previousMode == BORDERLESS && newMode != BORDERLESS ? notDisplayable(host¹²¹) : (previousMode != BORDERLESS && newMode == BORDERLESS ? notDisplayable(host¹²¹) : displayable(host¹²¹))

Test suite fixture (classes/found_binders_error)

In the same way, ErrorStateHintPathDependent now shows only ready ? open(f) : created(f), without ∀ready true.

What the fixed #fresh path rows still show (∀#fresh¹¹² !#fresh¹¹¹) is the separate part of #375 that ties in with #373. They are not true rows, and this PR leaves them alone.

Tests

• TestFoundBinders:
  • variablesAnotherRowShowsGetNoTrueRow (positive): new addUp fixture, the A1_09 pattern as a refinement error.
  • variableOnlyExpectedNamesKeepsItsTrueRow (negative): new forward fixture. The informative ∀t true row and its counterexample stay.
  • staticFieldIsWrittenWithItsClass updated: the Basket.served row goes, and its counterexample value stays.
• VCBinderSimplificationTest:
  • Tests that encoded the old linking rule now expect the row to go: removesTrueBinderThatALaterRowShows, removesTrueBinderThatIsTheArgumentOfAGhost, and removesTrueBindersThatAConditionalStateShows (the A1_09 shape).
  • New removesTrueBinderOfExpectedVariableThatAnotherRowShows.
  • keepsTrueBinderOfExpectedVariableNoOtherRowMentions (renamed) still keeps the row.
  • skipsInapplicableTrueBinderAndSimplifiesLaterBinder now uses a row that does not mention x, so x is still the inapplicable binder.
• Without the fix (main sources, new tests kept), 6 of the 22 tests in these two classes fail, including both positive tests. The negative test passes on both, as it should.
• mvn test: 667 tests, 0 failures.

Part of #375. The #fresh path rows are left for #373.

🤖 Generated with Claude Code