镜像站点 · 本页由第三方 GitHub 只读镜像提供,非 GitHub 官方站点,不接受任何登录或凭据输入。前往 github.com
Skip to content

An undecided member of an intersection stays in it - #1681

Merged
Rafael-SOWNet merged 1 commit into
masterfrom
an-undecided-member-of-an-intersection-stays-in-it
Oct 2, 2026
Merged

Rafael-SOWNet merged 1 commit into
masterfrom
an-undecided-member-of-an-intersection-stays-in-it

Conversation

@Rafael-SOWNet

Copy link
Copy Markdown
Member

Closes #1680.

A member of a listed set whose membership in the other set can't be decided was kept in their intersection unconditionally. So { y } /\ { 2 } was { y }, which is wrong at every y but 2. Solve meets the solution sets of a conjunction's two sides, so the same thing dropped an equation with a parameter in it. Now such a member stays intersected with the other set, beside the members that are decided:

2.5.0 and master this
{ y } /\ { 2 } { y } { y } /\ { 2 }
{ y, 3 } /\ { 3 } { y } \/ { 3 } { 3 } \/ { y } /\ { 3 }
"x = y and x = 2".Solve("x") { y }, which reads { 1 } at y = 1 { y } /\ { 2 }, empty at y = 1
"x + y = 3 and x - y = 1".Solve("x") { 3 - y } { 3 - y } /\ { 1 + y }: { 2 } at y = 1, empty elsewhere
"x^2 = 4 and x = y".Solve("x") { 2, -2 } { 2, -2 } /\ { y }

A conjunction whose members are all decided is unchanged: x = 2 and x = 3 is { }, x^2 = 4 and not x = 2 is { -2 }.

Tests: ConjunctionFilterTest.ListedSetsWithAParameterMeetWhereTheyAgree (six rows, each with the parameter pinned on both sides of where the sets meet) and AnUndecidedMemberOfAnIntersectionStaysInIt (four). SolveEquationWithConstraints.TestFiniteIntersection, skipped as "Sets require more work", runs now and asserts the right answer: x^2 = a and x = a is { 0 } at a = 0, { 1 } at a = 1, and empty elsewhere.

The suite passes, 14,334 tests. CasBench (120/121, 0 wrong), BoundCheck (0 disagreements), CanonCheck and Confluence (findings unchanged) pass, and so does the allocation gate.

🤖 Generated with Claude Code

https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura

A member of a listed set whose membership in the other set could not be decided was kept in their
intersection unconditionally, so { y } /\ { 2 } was { y }, wrong at every y but 2, and Solve,
which meets the solution sets of a conjunction's sides, dropped an equation with a parameter in
it: x = y and x = 2 solved to { y }. Such a member now stays intersected with the other set,
beside the members that are decided.

Closes #1680.

Co-Authored-By: Claude Opus 5.5 (1M context) <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_012sonx8iAspMiwRwokT1Ura
@Rafael-SOWNet Rafael-SOWNet added this to the 2.6.0 milestone Oct 2, 2026
@Rafael-SOWNet
Rafael-SOWNet merged commit 6e2b2eb into master Oct 2, 2026
34 checks passed
@Rafael-SOWNet
Rafael-SOWNet deleted the an-undecided-member-of-an-intersection-stays-in-it branch October 29, 2026 00:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Solve drops an equation of a conjunction once it has a parameter: x = y and x = 2 is { y }

1 participant