de.uka.ilkd.key.strategy.quantifierHeuristics

Class TwoSidedMatching

java.lang.Object

de.uka.ilkd.key.strategy.quantifierHeuristics.TwoSidedMatching

class TwoSidedMatching
extends java.lang.Object

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

Field Summary

Fields

Modifier and Type	Field and Description
private Substitution	targetSubstWithMVs
private Term	targetWithMVs
private UniTrigger	trigger
private Substitution	triggerSubstWithMVs
private Term	triggerWithMVs

Constructor Summary

Constructors

Constructor and Description
TwoSidedMatching(UniTrigger trigger, Term targetTerm, Services services) creates an instance of a two sided matching

Method Summary

Modifier and Type	Method and Description
private ImmutableSet<Substitution>	getAllSubstitutions(Term target, Services services)
(package private) ImmutableSet<Substitution>	getSubstitutions(Services services) returns the found matchings
private boolean	isGround(Term t)
private Substitution	match(Term triggerTerm, Term targetTerm, Services services) find a substitution in a allterm by using unification

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

trigger

private final UniTrigger trigger

triggerWithMVs

private final Term triggerWithMVs

targetSubstWithMVs

private final Substitution targetSubstWithMVs

triggerSubstWithMVs

private final Substitution triggerSubstWithMVs

targetWithMVs

private final Term targetWithMVs

Constructor Detail

TwoSidedMatching

TwoSidedMatching(UniTrigger trigger,
                 Term targetTerm,
                 Services services)

creates an instance of a two sided matching

Parameters:

trigger - the UniTrigger

targetTerm - the term to match

services - the Services

Method Detail

getSubstitutions

ImmutableSet<Substitution> getSubstitutions(Services services)

returns the found matchings

Parameters:

services - the Services

Returns:

the found matchings

getAllSubstitutions

private ImmutableSet<Substitution> getAllSubstitutions(Term target,
                                                       Services services)

match

private Substitution match(Term triggerTerm,
                           Term targetTerm,
                           Services services)

find a substitution in a allterm by using unification

isGround

private boolean isGround(Term t)