| java.lang.Object de.uka.ilkd.key.strategy.quantifierHeuristics.TwoSidedMatching
TwoSidedMatching | class TwoSidedMatching (Code) | | Matching triggers within another quantifier expression. Problems with the
current implementation:
the usage of EqualityConstraint for unification implies that a variable is
never instantiated with non-rigid terms
it is unclear whether certain instantiations are lost due to too strict type
checks in EqualityConstraint
|
getSubstitutions | SetOfSubstitution getSubstitutions()(Code) | | |
|
|