[CatarinaGamboa]

Closes #523.

What

Found kept ternaries whose tests a top-level fact of Found already decides, such as newMode == BORDERLESS in A1_09.

• New display pass VCKnownEnumValues (step name Known Enum Values, runs after Binder, before Folding). For a fact x == C or x != C with C an enum constant, it replaces the comparisons of x with constants of the same enum in the other facts by true/false. Folding and Logical then fold the ternaries and conjunctions. It handles one fact per step and never rewrites the fact it uses.
• VCLogicalSimplification now factors the conjuncts both disjuncts share out of a disjunction: c && p || c && q becomes c && (p || q), and c || c && p becomes c. This shortens the setVisible(false) attempt.

Soundness

The change is display only, so the verdict does not change. The pass uses only the constants of the enum types of the chain's binders (CtEnum declarations). The solver translates these as distinct EnumSort values. static final constants, which may share a value, are never used: an Enum node with a resolved literal is skipped. Each rewrite is an equivalence, given the fact it uses, and that fact stays in Found.

A1_09: Found before and after

Exercise as given (setUndecorated, line 49):

before: found newMode == BORDERLESS && (previousMode == BORDERLESS && newMode != BORDERLESS ? display(host) == notDisplayable : (previousMode != BORDERLESS && newMode == BORDERLESS ? display(host) == notDisplayable : display(host) == displayable)) but expected display(host) == notDisplayable
after:  found newMode == BORDERLESS && (previousMode != BORDERLESS ? display(host) == notDisplayable : display(host) == displayable) but expected display(host) == notDisplayable

Partial fix, adding else if (newMode == BORDERLESS) host.dispose(); (error moves to the FULLSCREEN fallback, line 64):

before: found newMode == FULLSCREEN && (previousMode == BORDERLESS && newMode != BORDERLESS ? display(host) == notDisplayable : (previousMode != BORDERLESS && newMode == BORDERLESS ? display(host) == notDisplayable : (newMode == BORDERLESS ? display(host) == notDisplayable : display(host) == displayable))) but expected display(host) == notDisplayable
after:  found previousMode == BORDERLESS ? display(host) == notDisplayable : display(host) == displayable but expected display(host) == notDisplayable

host.dispose() only in case BORDERLESS (FULLSCREEN fallback, line 63):

before: found newMode == FULLSCREEN && (previousMode == BORDERLESS && newMode != BORDERLESS ? display(host) == notDisplayable : (previousMode != BORDERLESS && newMode == BORDERLESS ? display(host) == notDisplayable : display(host) == displayable)) but expected display(host) == notDisplayable
after:  found previousMode == BORDERLESS ? display(host) == notDisplayable : display(host) == displayable but expected display(host) == notDisplayable

host.setVisible(false) before setUndecorated (line 50):

before: found (previousMode == BORDERLESS && newMode != BORDERLESS ? display(host@22) == notDisplayable : (previousMode != BORDERLESS && newMode == BORDERLESS ? display(host@22) == notDisplayable : display(host@22) == displayable)) && newMode == BORDERLESS && (display(host@22) == notDisplayable && display(host) == notDisplayable && (previousMode == BORDERLESS && newMode != BORDERLESS ? display(host) == notDisplayable : (previousMode != BORDERLESS && newMode == BORDERLESS ? display(host) == notDisplayable : display(host) == displayable)) || display(host@22) == displayable && display(host) == displayable && (previousMode == BORDERLESS && newMode != BORDERLESS ? display(host) == notDisplayable : (previousMode != BORDERLESS && newMode == BORDERLESS ? display(host) == notDisplayable : display(host) == displayable))) but expected display(host) == notDisplayable
after:  found (previousMode != BORDERLESS ? display(host@22) == notDisplayable : display(host@22) == displayable) && newMode == BORDERLESS && (previousMode != BORDERLESS ? display(host) == notDisplayable : display(host) == displayable) && (display(host@22) == notDisplayable && display(host) == notDisplayable || display(host@22) == displayable && display(host) == displayable) but expected display(host) == notDisplayable

#501 should remove the remaining host@22 versions.

Note: in the two FULLSCREEN attempts, newMode == FULLSCREEN is no longer shown. Once the ternary is folded, it no longer mentions newMode, so Relevant to Expected drops the fact as unrelated to display(host). The error line is in the FULLSCREEN fallback, so the context is still visible there. In the BORDERLESS case, newMode == BORDERLESS stays only because the folded ternary still mentions the constant BORDERLESS.

Tests

• VCKnownEnumValuesTest: a != fact decides only its own constant; constants read in code, which are Vars named after the constant, are decided; a fact of the last row, which may be the conclusion, does not rewrite the premises; and step by step through simplifyOnce, a decided ternary folds even after its enum binder is removed.
• VCLogicalSimplificationTest#factorsConjunctsSharedByDisjuncts.
• VCTestUtils gains a Mode enum binder type.
• mvn test: 733 tests, 0 failures.

VS Code client: the new step name is Known Enum Values.

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex review, round 1

1. [P2] Facts from a goal row rewrite premises (VCKnownEnumValues): fixed. The Found chains passed to simplification hold premises only, because joinPredicates clones the chain before it appends expected. The other passes still treat the last row as a possible conclusion: VCConstraintSimplification and the conclusion tests in VCSubstitutionTest do. So a fact of the last row now decides only that row. A1_09 output is unchanged. Test: keepsPremisesTheConclusionWouldDecide.
2. [P2] Stepwise simplifyOnce loses enum types after a binder is removed: fixed. simplifyOnce now builds the pass from getOriginal(), the chain before any step. Test: foldsTheTernariesAFactDecides now goes step by step through simplifyOnce, which also covers the wiring.

mvn test: 733 tests, 0 failures.

[CatarinaGamboa]

Codex review, round 2: no findings ("No actionable defects were identified. The verifier test suite passes."). The loop stops here.

[CatarinaGamboa]

Clean-code audit (clean-code-principles)

VCKnownEnumValues.java:31  - [name-meaningful] record KnownValue described both the deciding fact and every comparison it tests.   -> fixed: renamed to EnumComparison(expression, ...), and knownValue() to enumComparison()
VCKnownEnumValues.java:46  - [doc-self-documenting] the javadoc "Decides the comparisons that the first fact deciding any decides" was hard to parse.   -> fixed: reworded
VCKnownEnumValues.java:64  - [name-consistent] two overloads named decide(), one over rows and one over expressions, with different contracts.   -> fixed: the row version is now decideRows()
VCKnownEnumValues.java:82  - [func-single-purpose] the true/false decision is inline in decide(). Not changed: it is five lines and reads in place
VCLogicalSimplification.java:172 - [core-dry] conjunction(List) repeats the reduce-to-&& in VCRelevantFacts.rebuild and VCSimplificationUtils.linkedToExpected. Not changed: a shared helper would touch two unrelated passes; worth doing in a separate cleanup
VCTestUtils.java:26 - [core-yagni] one fixed Mode enum type rather than a general enum builder. Not changed on purpose: the tests need only this one

SOLID and encapsulation: the new pass follows VCSimplificationPass like its siblings. Its only state is the enum constants collected from the original chain, so it cannot depend on pass order. No issues found there.

mvn test: 733 tests, 0 failures.