ConstraintAnalysis: Properly handle local changes#8878
Conversation
|
|
||
| inline bool isRelationalSymmetric(Op op) { return op == Eq || op == Ne; } | ||
|
|
||
| inline bool isRelationalAntisymmetric(Op op) { |
There was a problem hiding this comment.
I'm getting weirdly caught up on whether the *-or-equal variants count as antisymmetric. Taking <= as an example, antisymmetry means that for all x and y we have x <= y /\ y <= x ==> x == y. If the domain is integer or real values, that's certainly true, but my mental model is that the domain is terms, in which case this is not true. We can easily have distinct variables x and y where both x <= y and y <= x. In that case we know the values of x and y are equal, but x is not identical to y.
| if (flip) { | ||
| // Build a flipped constraint, referring to index. | ||
| auto otherIndex = std::get<Index>(actual.term); | ||
| actual.term = Term{index}; | ||
| index = otherIndex; | ||
| if (Abstract::isRelationalAntisymmetric(actual.op)) { | ||
| actual.op = Abstract::negateRelational(actual.op); | ||
| } else { | ||
| // All we support for now are symmetric and antisymmetric operations. | ||
| assert(Abstract::isRelationalSymmetric(actual.op)); | ||
| } | ||
| } |
There was a problem hiding this comment.
Can we pull this flip operation out into a helper function, maybe on LocalConstraint?
| // Cross-local constraints (like x == y) are duplicated, that is, they appear in | ||
| // the constraints for both x and y. This makes things simple by having all | ||
| // constraints related to a local in the same place. |
There was a problem hiding this comment.
Instead of storing each variable-variable constraint in both directions (which uses the limited space in our bounded conjunctions), we could arbitrarily just store it in one direction (possibly by choosing the variable with the most remaining free space for constraints), then on lookup rely on refs to tell us where else we might find relevant constraints. But then I guess you wouldn't have all the relevant constraints packaged up as a single bounded conjunction :/
| // If we can prove nothing, we should have removed it from the map. | ||
| assert(!constraints.provesNothing()); |
There was a problem hiding this comment.
We can also assert that it's not a contradiction, right?
| constraints.set(set->index, Constraint{Abstract::Eq, {value}}); | ||
| } else if (auto* get = set->value->dynCast<LocalGet>()) { | ||
| // Apply a constraint to this local. | ||
| constraints.set(set->index, Constraint{Abstract::Eq, {get->index}}); |
There was a problem hiding this comment.
You could also look up everything we previously knew about get->index and apply it to set->index. This would help optimize situations where we need to know transitive constraints.
2 participants
Track references of a local among the constraints of the rest. When a local
is updated, remove its stale references (claims about its old value no
longer hold).
Also, formalize how we represent info: when we see
x == y, we now storethat on both
xandy, ensuring a single place where we can find allconstraints about a local.