Repository navigation
A saturation check compared two things that have no value (#1162) - #1166
Merged
Merged
Conversation
EqualitySaturationNeverChangesTheValueItClaimsToPreserve substitutes a real for every free variable and compares what the two sides evaluate to. Its catch was meant to skip the boolean and set-valued corpus entries -- its own comment says "not this test's claim" -- and it does not skip them, because nothing throws. Substituting 0.37 into `a and b` does not raise and does not give NaN: it hands back `37/100 and 37/100`, unevaluated. Two different unevaluated forms of a thing with no truth value then compare unequal, and the test reports a value changing where no value exists. `a and b or a and not b` distributing to `a and (b or not b)` failed for that reason alone. It is a boolean identity and it was right all along. Skipped now only when neither side has a value, and made stricter in the case that matters: one side evaluating and the other not is a rewrite that lost a value, which is precisely what this test is for and which it would previously have compared structurally and might have passed. With that, the two boolean distributions can say their growth. The count was never in doubt -- the shared operand is matched twice and written once, so -(1 + |k|) -- only whether declaring it was safe, since a declaration is what puts a rule into the set equality saturation fires. This retracts what #1162 says. I filed it as a rule marked Sound that changes the value, and blamed IsLogic for admitting a free variable. The mechanism was stated before the values were measured; measuring them shows both sides stuck rather than disagreeing. Full suite 9554 passed, 0 failed. Closes #1162. Part of #825. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
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
1 participant
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.
#1162 says a rule marked
Soundchanges the value. It does not, and this retracts that.I filed it while declaring growths, blamed
IsLogicfor admitting a free variable, and stated themechanism before measuring the values it makes a claim about. Measuring them:
A boolean operation on a non-boolean does not evaluate to
NaN— it does not evaluate at all.Both sides are stuck. Neither has a truth value. Nothing changed.
(a and b) or (a and not b) = a and (b or not b)is a boolean identity and was right all along.The defect is in the check
EqualitySaturationNeverChangesTheValueItClaimsToPreservesubstitutes a real for every freevariable, calls
.Evaledon both sides inside atry, and hasThat skip never fires.
.Evaledon0.37 and 0.37throws nothing; it returns the nodeunevaluated. So
EqualsImpreciselycompares two different unevaluated forms of a thing with novalue and reports a disagreement. The test's own comment names the entries it means to exclude, and
its mechanism for excluding them has never worked —
"a and b or a and not b"is in its corpusprecisely so the boolean rules are exercised.
The fix is strictly stronger than what it replaces
Skipped only when neither side has a value. One side evaluating and the other not now fails
loudly — that is a rewrite which lost a value, exactly what this test exists to catch, and today it
would have been compared structurally and might well have passed.
What it unblocks
Both boolean distributions can now say their growth. The count was never in doubt — the shared
operand is matched twice and written once, so
-(1 + |k|)— only whether declaring it was safe,since a declaration is what puts a rule into the set equality saturation fires. 152 rules sit at
Unknown, down from 154.Verification
Full suite 9554 passed, 0 failed, 14 skipped.
Closes #1162. Part of #825.