de.uka.ilkd.key.strategy.quantifierHeuristics

Class Matching

java.lang.Object

de.uka.ilkd.key.strategy.quantifierHeuristics.Matching

class Matching
extends java.lang.Object

Two kind of matching algorithm are coded in two nested classes BaseMatching TwosideMatching

Constructor Summary

Constructors

Modifier	Constructor and Description
private	Matching()

Method Summary

Modifier and Type	Method and Description
static ImmutableSet<Substitution>	basicMatching(Trigger trigger, Term targetTerm) matching trigger to targetTerm recursively
static ImmutableSet<Substitution>	twoSidedMatching(UniTrigger trigger, Term targetTerm, Services services)

Methods inherited from class java.lang.Object

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

Constructor Detail

Matching

private Matching()

Method Detail

basicMatching

public static ImmutableSet<Substitution> basicMatching(Trigger trigger,
                                                       Term targetTerm)

matching trigger to targetTerm recursively

Parameters:

trigger - a uni-trigger

targetTerm - a gound term

Returns:

all substitution found from this matching

twoSidedMatching

public static ImmutableSet<Substitution> twoSidedMatching(UniTrigger trigger,
                                                          Term targetTerm,
                                                          Services services)