Java: Improve join-order by properly annotating haveIntersection.

This commit is contained in:
Anders Schack-Mulligen
2025-07-18 11:48:50 +02:00
parent 7883124abd
commit d9f47bdec9

View File

@@ -1261,14 +1261,21 @@ private Type erase(Type t) {
*
* For the definition of the notion of *erasure* see JLS v8, section 4.6 (Type Erasure).
*/
bindingset[t1, t2]
overlay[caller?]
pragma[inline]
pragma[inline_late]
predicate haveIntersection(RefType t1, RefType t2) {
exists(RefType e1, RefType e2 | e1 = erase(t1) and e2 = erase(t2) |
erasedHaveIntersection(e1, e2)
erasedHaveIntersectionFilter(e1, e2)
)
}
bindingset[t1, t2]
pragma[inline_late]
private predicate erasedHaveIntersectionFilter(RefType t1, RefType t2) {
erasedHaveIntersection(t1, t2)
}
/**
* Holds if there is no common (reflexive, transitive) subtype of the erasures
* of types `t1` and `t2`.