-
Notifications
You must be signed in to change notification settings - Fork 3k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Do not generate redundant straddling predicates by equality inference #16520
Conversation
8ca7065
to
f63c4c1
Compare
rebased |
2887dc5
to
e8dd270
Compare
if (matchingCanonical != null) { | ||
straddlingExpressions.add(matchingCanonical); | ||
} | ||
else if (complementCanonical != null) { | ||
straddlingExpressions.add(complementCanonical); | ||
} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
What if both are non-null? What are the implications of adding one but not the other?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
So you have three groups of expressions:
scope
complement
straddling (these are guaranteed to have symbols from from scope and non-scope)
They are all equal.
Therefore you need to generate equalities
- within
scope
- within
complement
- within
straddling
- between
scope<->complement
- between ONE OF
(scope, complement) <-> straddling
let's say:
scope = (l.x; l.y)
complement = (r.x; r.y)
straddling = (l.i + r.j; l.m + r.n)
Then you generate:
for scope: l.x = l.y
for complement: r.x = r.y
for straddling: l.i + r.j = l.m + r.n
You also need to generate one canonical equality between scope and complement:
l.x = r.y
But you also need to connect straddling
group with the rest of expressions somehow. The way you do it is by choosing canonical expression from EITHER scope
or complement
and generate equality with any straddling expression, e.g:
l.x = l.i + r.j
This way yo generate all needed equalities, but not more.
If you were to choose canonical expression from both scope
and complement
, then you would generate redundant equality. Specifically this is important for constants, e.g:
equalitySet = [1, l.r, r.y, l.i + r.j]
scope = [1, l.r]
complement = [1, r.y]
straddling = [l.i + r.j]
generated equalities:
1 = l.r; 1 = r.y; 1 = l.i + r.j
If you were to choose canonical expression from both scope
and complement
, then it would generate equalities:
1 = l.r; 1 = r.y; 1 = 1; 1 = l.i + r.j
because 1
is canonical on both scope
and complement
side.
This step is not needed anymore as corresponding tests do not fail.
When there are predicates like a1 = b1 and a2 = a1 + 1, then equality inference would derive staddling predicate for a2 = b1 + 1, which is redundant to a1 = b1, a2 = a1 + 1. This commit makes sure that redundant straddling predicates are not generated.
e8dd270
to
d3da589
Compare
Release notes
( ) This is not user-visible or docs only and no release notes are required.
(x) Release notes are required, please propose a release note for me.
( ) Release notes are required, with the following suggested text: