de.uka.ilkd.key.strategy.quantifierHeuristics

Class BasicMatching

java.lang.Object

de.uka.ilkd.key.strategy.quantifierHeuristics.BasicMatching

class BasicMatching
extends java.lang.Object

Constructor Summary

Constructors

Modifier	Constructor and Description
private	BasicMatching()

Method Summary

Modifier and Type	Method and Description
(package private) static ImmutableSet<Substitution>	getSubstitutions(Term trigger, Term targetTerm) matching trigger to targetTerm recursively
private static ImmutableMap<QuantifiableVariable,Term>	mapVarWithCheck(ImmutableMap<QuantifiableVariable,Term> varMap, QuantifiableVariable var, Term instance) match a variable to a instance.
private static Substitution	match(Term pattern, Term instance)
private static ImmutableMap<QuantifiableVariable,Term>	matchRec(ImmutableMap<QuantifiableVariable,Term> varMap, Term pattern, Term instance) match the pattern to instance recursively.

Methods inherited from class java.lang.Object

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

Constructor Detail

BasicMatching

private BasicMatching()

Method Detail

getSubstitutions

static ImmutableSet<Substitution> getSubstitutions(Term trigger,
                                                   Term targetTerm)

matching trigger to targetTerm recursively

Parameters:

trigger - a uni-trigger

targetTerm - a gound term

Returns:

all substitution found from this matching

match

private static Substitution match(Term pattern,
                                  Term instance)

Parameters:

pattern -

instance -

Returns:

all substitution that a given pattern(ex: a term of a uniTrigger) match in the instance.

matchRec

private static ImmutableMap<QuantifiableVariable,Term> matchRec(ImmutableMap<QuantifiableVariable,Term> varMap,
                                                                Term pattern,
                                                                Term instance)

match the pattern to instance recursively.

mapVarWithCheck

private static ImmutableMap<QuantifiableVariable,Term> mapVarWithCheck(ImmutableMap<QuantifiableVariable,Term> varMap,
                                                                       QuantifiableVariable var,
                                                                       Term instance)

match a variable to a instance.

Returns:

true if it is a new vaiable or the instance it matched is the same as that it matched before.