feat(alias_elimination): detect x ~ -y perfect aliases#4540
feat(alias_elimination): detect x ~ -y perfect aliases#4540oscardssmith wants to merge 10 commits into
x ~ -y perfect aliases#4540Conversation
Extend `find_perfect_aliases!` to recognize the negated alias pattern `c1*v1 + c2*v2 ~ 0` with `c1 == c2` (i.e. `x ~ -y`) in addition to the existing `c1 == -c2` case (`x ~ y`). Each candidate alias edge carries an `Int8` sign, and a BFS from each group's chosen target propagates signs to every member -- so transitive chains including double negation (`x ~ -y` and `y ~ -z` ⇒ `x ~ z`) are resolved correctly. When a group's signed edges are inconsistent (e.g. `x ~ y` and `x ~ -y` both appear), every non-sticky variable in that group is substituted with `0` and a `v ~ 0` equation is added to `additional_observed`; irreducibles remain unknowns and the surviving alias equations carry the resulting `irr ~ 0` constraint into the system. Substitution rhs and derivative-cascade substitutions both honor the propagated sign. Tests cover: basic `y ~ -x`, mixed chain `x ~ y, y ~ -z`, double-negation transitivity, negated alias with irreducible target, and the sign-conflict force-to-zero case. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
I think for the 0 case it's worth including sticky non-irreducible variables too (i.e. ones with positive state priority). The variable cannot possibly be anything else, so it serves no purpose participating in state selection. Substituting zeros into other equations may also simplify them drastically. Knowing something is zero is very useful information. |
|
Good point. Irreducible can just leave the variable with the equation x~0. |
Split the loop over `candidate_eqs` into separate conflict-group and
consistent-group passes. The conflict-group pass now eagerly pins one
irreducible per claimed alias equation by rewriting it to `v ~ 0` (and
stripping the bipartite edge to the other endpoint), which both:
- correctly handles the previously-incorrect case where both
endpoints of a conflict-group alias equation are irreducible (the
surviving `c1*v1 + c2*v2 = 0` did not individually pin either to
zero), and
- eliminates the need for a separate `pinned_eqs` data structure
living across the substitution pass.
The main alias_sets loop now only needs to distinguish "irreducible in
a conflict group" (just mark `always_present`, since the pin is already
written) from non-irreducibles (substitute to 0 / to ±target as
before). Priority>0 non-irreducibles in conflict groups are eliminated
normally instead of being kept as unconstrained unknowns.
Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Switch the negated-alias testset from `@mtkcompile` to `TearingState` + `eliminate_perfect_aliases!` so we verify the behavior of this pass in isolation rather than the cumulative output of `mtkcompile`. Assertions now target `state.additional_observed`, `equations(state.sys)`, `state.fullvars`, and `state.always_present`. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
I've actually gone a step further and have included irreducibles as well in this. Just because we are irreducible doesn't mean we can't substitute away all users. We now make irreducibles remain as |
Co-authored-by: Aayush Sabharwal <aayush.sabharwal@gmail.com>
Co-authored-by: Aayush Sabharwal <aayush.sabharwal@gmail.com>
AayushSabharwal
left a comment
AayushSabharwal
left a comment
There was a problem hiding this comment.
I just realized, if we eliminate a variable as zero and substitute the zero into other equations, we have to update the incidence of those equations.
Is this just for cases where we have Edit: this is wrong. there's lots of nonlinear cases as well. |
|
Should be fixed. |
3 participants
Extend
find_perfect_aliases!to recognize the negated alias patternc1*v1 + c2*v2 ~ 0withc1 == c2(i.e.x ~ -y) in addition to the existingc1 == -c2case (x ~ y). Each candidate alias edge carries anInt8sign, and a BFS from each group's chosen target propagates signs to every member -- so transitive chains including double negation (x ~ -yandy ~ -z⇒x ~ z) are resolved correctly.When a group's signed edges are inconsistent (e.g.
x ~ yandx ~ -yboth appear), every non-sticky variable in that group is substituted with0and av ~ 0equation is added toadditional_observed; irreducibles remain unknowns and the surviving alias equations carry the resultingirr ~ 0constraint into the system. Substitution rhs and derivative-cascade substitutions both honor the propagated sign.Tests cover: basic
y ~ -x, mixed chainx ~ y, y ~ -z, double-negation transitivity, negated alias with irreducible target, and the sign-conflict force-to-zero case.Claude wrote most of this, but it seems pretty reasonably implemented.