Repository navigation
Fold ternaries that a fact of Found decides on an enum value - #531
Merged
Merged
Conversation
Found kept ternaries whose tests a top-level fact such as newMode == BORDERLESS already decides. A new display pass, Known Enum Values, replaces each comparison of a variable with an enum constant that another fact decides by its value, so Folding and Logical fold the ternaries. Only constants of the enum types of the chain's binders are used, which the solver translates as distinct values. Logical simplification also factors the conjuncts both disjuncts share out of a disjunction. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Collaborator
Author
|
Codex review, round 1
|
Collaborator
Author
|
Codex review, round 2: no findings ("No actionable defects were identified. The verifier test suite passes."). The loop stops here. |
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Collaborator
Author
|
Clean-code audit (clean-code-principles) SOLID and encapsulation: the new pass follows
|
CatarinaGamboa
added a commit
that referenced
this pull request
Nov 11, 2026
…th (#534) Stacked on #531 (base `feat/found-fold-decided-ternary`). Part of #523: the last step of folding A1_09's Found. ## What After #531 folds A1_09's ternary under `newMode == BORDERLESS`, the ternary no longer mentions `newMode`, yet Found still shows `newMode == BORDERLESS`. The cause is in **Relevant to Expected** (`VCRelevantFacts.addSymbols`, `VCRelevantFacts.java:125` on #531): every `Var` is a symbol, and an enum constant read in code is a `Var` named `DisplayMode.BORDERLESS`. So `newMode == BORDERLESS` and the folded ternary stay linked through the constant. (An enum constant written in a refinement is an `Enum` node, which already linked nothing.) A constant is a fixed value: two facts that only compare values with the same constant share no unknown. The relevance pass now ignores enum constants as symbols, **except** when a function or alias takes the constant, or a value one takes is compared with it. There, equality through the constant does relate facts (`x == A && state(A) == shown` gives `state(x) == shown`). This exception comes from Codex's round-1 counterexample. - `VCRelevantFacts` takes the enum constants of the chain. `VCKnownEnumValues.enumConstants` exposes the set #531 already builds. - There is still one relevance run and no new pass. The step order is unchanged: Substitution, Function Substitution, Binder, **Known Enum Values**, Folding, Arithmetic, Logical, Constraint to a fixed point, then **Relevant to Expected** once, then `ErrorMessage`'s fact selection. ## Soundness Display only; the verdict is unchanged. The relevance pass drops only facts D whose unknowns are disjoint from Expected's and from the kept facts S. Enum constants are distinct `EnumSort` values. When no function takes a value equal to a shared constant, a model of S and a model of D combine. So the premises imply S, and S fails Expected exactly when the premises do. `static final` constants are not in the set. ## A1_09 (the only study task that changes) ``` #531: found newMode == BORDERLESS && (previousMode != BORDERLESS ? display(host) == notDisplayable : display(host) == displayable) but expected display(host) == notDisplayable this: found previousMode != BORDERLESS ? display(host) == notDisplayable : display(host) == displayable but expected display(host) == notDisplayable ``` The other seven study tasks have the same output as on #531, byte for byte, with one error each on `reportedLine`. All 287 `testSuite` fixtures have the same headlines as on #531. The formatter writes a Found that is a single ternary without parentheses, as in #531's FULLSCREEN case. That is outside this PR. ## Tests - `VCSimplificationTest#relevantStepDoesNotLinkFactsThroughAConstant` (fails without the change). - `VCSimplificationTest#relevantStepLinksFactsThroughAConstantAnObjectEquals` (Codex's counterexample; fails with the naive "drop every constant" version). - `mvn test`: 735 tests, 0 failures. 🤖 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.
Closes #523.
What
Found kept ternaries whose tests a top-level fact of Found already decides, such as
newMode == BORDERLESSin A1_09.VCKnownEnumValues(step name Known Enum Values, runs after Binder, before Folding). For a factx == Corx != CwithCan enum constant, it replaces the comparisons ofxwith constants of the same enum in the other facts bytrue/false. Folding and Logical then fold the ternaries and conjunctions. It handles one fact per step and never rewrites the fact it uses.VCLogicalSimplificationnow factors the conjuncts both disjuncts share out of a disjunction:c && p || c && qbecomesc && (p || q), andc || c && pbecomesc. This shortens thesetVisible(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 (
CtEnumdeclarations). The solver translates these as distinctEnumSortvalues.static finalconstants, which may share a value, are never used: anEnumnode 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):Partial fix, adding
else if (newMode == BORDERLESS) host.dispose();(error moves to the FULLSCREEN fallback, line 64):host.dispose()only incase BORDERLESS(FULLSCREEN fallback, line 63):host.setVisible(false)beforesetUndecorated(line 50):#501 should remove the remaining
host@22versions.Note: in the two FULLSCREEN attempts,
newMode == FULLSCREENis no longer shown. Once the ternary is folded, it no longer mentionsnewMode, so Relevant to Expected drops the fact as unrelated todisplay(host). The error line is in the FULLSCREEN fallback, so the context is still visible there. In the BORDERLESS case,newMode == BORDERLESSstays only because the folded ternary still mentions the constantBORDERLESS.Tests
VCKnownEnumValuesTest: a!=fact decides only its own constant; constants read in code, which areVars 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 throughsimplifyOnce, a decided ternary folds even after its enum binder is removed.VCLogicalSimplificationTest#factorsConjunctsSharedByDisjuncts.VCTestUtilsgains aModeenum binder type.mvn test: 733 tests, 0 failures.VS Code client: the new step name is Known Enum Values.
🤖 Generated with Claude Code