de.uka.ilkd.key.strategy.quantifierHeuristics

Class Substitution

java.lang.Object

de.uka.ilkd.key.strategy.quantifierHeuristics.Substitution

public class Substitution
extends java.lang.Object

This class decribes a substitution,which store a map(varMap) from quantifiable variable to a term(instance).

Field Summary

Fields

Modifier and Type	Field and Description
private ImmutableMap<QuantifiableVariable,Term>	varMap

Constructor Summary

Constructors

Constructor and Description
Substitution(ImmutableMap<QuantifiableVariable,Term> map)

Method Summary

Modifier and Type	Method and Description
Term	apply(Term t, TermServices services)
private Term	applySubst(QuantifiableVariable var, Term instance, Term t, TermBuilder tb)
Term	applyWithoutCasts(Term t, TermServices services) Try to apply the substitution to a term, introducing casts if necessary (may never be the case any more, XXX)
boolean	equals(java.lang.Object arg0)
Term	getSubstitutedTerm(QuantifiableVariable var)
ImmutableMap<QuantifiableVariable,Term>	getVarMap()
int	hashCode()
boolean	isGround()
boolean	isTotalOn(ImmutableSet<QuantifiableVariable> vars)
private boolean	recOccurCheck(Term sub, Term term) check whether term "sub" is in term "term"
boolean	termContainsValue(Term term)
java.lang.String	toString()

Methods inherited from class java.lang.Object

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

Field Detail

varMap

private final ImmutableMap<QuantifiableVariable,Term> varMap

Constructor Detail

Substitution

public Substitution(ImmutableMap<QuantifiableVariable,Term> map)

Method Detail

getVarMap

public ImmutableMap<QuantifiableVariable,Term> getVarMap()

getSubstitutedTerm

public Term getSubstitutedTerm(QuantifiableVariable var)

isTotalOn

public boolean isTotalOn(ImmutableSet<QuantifiableVariable> vars)

isGround

public boolean isGround()

Returns:

true if every instance in the varMap does not contain variable.

apply

public Term apply(Term t,
                  TermServices services)

applySubst

private Term applySubst(QuantifiableVariable var,
                        Term instance,
                        Term t,
                        TermBuilder tb)

applyWithoutCasts

public Term applyWithoutCasts(Term t,
                              TermServices services)

Try to apply the substitution to a term, introducing casts if necessary (may never be the case any more, XXX)

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

termContainsValue

public boolean termContainsValue(Term term)

recOccurCheck

private boolean recOccurCheck(Term sub,
                              Term term)

check whether term "sub" is in term "term"