de.uka.ilkd.key.strategy.quantifierHeuristics

Class UniTrigger

java.lang.Object

de.uka.ilkd.key.strategy.quantifierHeuristics.UniTrigger

All Implemented Interfaces:

Trigger

class UniTrigger
extends java.lang.Object
implements Trigger

Field Summary

Fields

Modifier and Type	Field and Description
private boolean	isElementOfMultitrigger
private LRUCache<Term,ImmutableSet<Substitution>>	matchResults
private boolean	onlyUnify
private Term	trigger
private TriggersSet	triggerSetThisBelongsTo
private ImmutableSet<QuantifiableVariable>	uqvs

Constructor Summary

Constructors

Constructor and Description
UniTrigger(Term trigger, ImmutableSet<QuantifiableVariable> uqvs, boolean isUnify, boolean isElementOfMultitrigger, TriggersSet triggerSetThisBelongsTo)

Method Summary

Modifier and Type	Method and Description
private static boolean	containsLoop(ImmutableMap<QuantifiableVariable,Term> varMap, QuantifiableVariable var) Code copied from logic.EqualityConstraint
private static boolean	containsLoop(Substitution subst) Test whether this substitution constains loop.
boolean	equals(java.lang.Object arg0)
private ImmutableSet<Substitution>	getSubstitutionsFromTerm(Term t, Services services)
private ImmutableSet<Substitution>	getSubstitutionsFromTermHelp(Term t, Services services)
ImmutableSet<Substitution>	getSubstitutionsFromTerms(ImmutableSet<Term> targetTerm, Services services)
TriggersSet	getTriggerSetThisBelongsTo()
Term	getTriggerTerm()
(package private) ImmutableSet<QuantifiableVariable>	getUniVariables()
int	hashCode()
(package private) boolean	isElementOfMultitrigger()
static boolean	passedLoopTest(Term candidate, Term searchTerm) use similar algorithm as basic matching to detect loop
java.lang.String	toString()

Methods inherited from class java.lang.Object

clone, finalize, getClass, notify, notifyAll, wait, wait, wait

Field Detail

trigger

private final Term trigger

uqvs

private final ImmutableSet<QuantifiableVariable> uqvs

triggerSetThisBelongsTo

private final TriggersSet triggerSetThisBelongsTo

onlyUnify

private final boolean onlyUnify

isElementOfMultitrigger

private final boolean isElementOfMultitrigger

matchResults

private final LRUCache<Term,ImmutableSet<Substitution>> matchResults

Constructor Detail

UniTrigger

UniTrigger(Term trigger,
           ImmutableSet<QuantifiableVariable> uqvs,
           boolean isUnify,
           boolean isElementOfMultitrigger,
           TriggersSet triggerSetThisBelongsTo)

Method Detail

getSubstitutionsFromTerms

public ImmutableSet<Substitution> getSubstitutionsFromTerms(ImmutableSet<Term> targetTerm,
                                                            Services services)

Specified by:

getSubstitutionsFromTerms in interface Trigger

Returns:

all substitution that found from the targeTerm by matching this trigger to targeTerm.

getSubstitutionsFromTerm

private ImmutableSet<Substitution> getSubstitutionsFromTerm(Term t,
                                                            Services services)

getSubstitutionsFromTermHelp

private ImmutableSet<Substitution> getSubstitutionsFromTermHelp(Term t,
                                                                Services services)

getTriggerTerm

public Term getTriggerTerm()

Specified by:

getTriggerTerm in interface Trigger

equals

public boolean equals(java.lang.Object arg0)

Overrides:

equals in class java.lang.Object

hashCode

public int hashCode()

Overrides:

hashCode in class java.lang.Object

toString

public java.lang.String toString()

Overrides:

toString in class java.lang.Object

getUniVariables

ImmutableSet<QuantifiableVariable> getUniVariables()

getTriggerSetThisBelongsTo

public TriggersSet getTriggerSetThisBelongsTo()

passedLoopTest

public static boolean passedLoopTest(Term candidate,
                                     Term searchTerm)

use similar algorithm as basic matching to detect loop

Parameters:

candidate -

searchTerm -

containsLoop

private static boolean containsLoop(Substitution subst)

Test whether this substitution constains loop. It is mainly used for unitrigger's loop test.

containsLoop

private static boolean containsLoop(ImmutableMap<QuantifiableVariable,Term> varMap,
                                    QuantifiableVariable var)

Code copied from logic.EqualityConstraint

isElementOfMultitrigger

boolean isElementOfMultitrigger()