Merge pull request #9951 from aschackmull/java/notintersect-perf

Java: Improve join-order for `not haveIntersection`.
This commit is contained in:
Anders Schack-Mulligen
2022-08-04 11:08:02 +02:00
committed by GitHub
4 changed files with 26 additions and 7 deletions

View File

@@ -1194,8 +1194,8 @@ private Type erase(Type t) {
}
/**
* Is there a common (reflexive, transitive) subtype of the erasures of
* types `t1` and `t2`?
* Holds if there is a common (reflexive, transitive) subtype of the erasures of
* types `t1` and `t2`.
*
* If there is no such common subtype, then the two types are disjoint.
* However, the converse is not true; for example, the parameterized types
@@ -1212,6 +1212,25 @@ predicate haveIntersection(RefType t1, RefType t2) {
)
}
/**
* Holds if there is no common (reflexive, transitive) subtype of the erasures
* of types `t1` and `t2`.
*
* If there is no such common subtype, then the two types are disjoint.
* However, the converse is not true; for example, the parameterized types
* `List<Integer>` and `Collection<String>` are disjoint,
* but their erasures (`List` and `Collection`, respectively)
* do have common subtypes (such as `List` itself).
*
* For the definition of the notion of *erasure* see JLS v8, section 4.6 (Type Erasure).
*/
bindingset[t1, t2]
predicate notHaveIntersection(RefType t1, RefType t2) {
exists(RefType e1, RefType e2 | e1 = erase(t1) and e2 = erase(t2) |
not erasedHaveIntersection(e1, e2)
)
}
/**
* Holds if there is a common (reflexive, transitive) subtype of the erased
* types `t1` and `t2`.