| java.lang.Object de.uka.ilkd.key.strategy.quantifierHeuristics.Substitution
Substitution | class Substitution (Code) | | This class decribes a substitution,which store a map(varMap) from quantifiable
variable to a term(instance).
|
Constructor Summary | |
public | Substitution(MapFromQuantifiableVariableToTerm map) |
Substitution | public Substitution(MapFromQuantifiableVariableToTerm map)(Code) | | |
applyWithoutCasts | public Term applyWithoutCasts(Term t)(Code) | | Try to apply the substitution to a term, widening by removing casts to
jbyte, jint whenever possible
|
getVarMap | public MapFromQuantifiableVariableToTerm getVarMap()(Code) | | |
hashCode | public int hashCode()(Code) | | |
isGround | public boolean isGround()(Code) | | true if every instance in the varMap does not contain variable. |
isTotalOn | public boolean isTotalOn(SetOfQuantifiableVariable vars)(Code) | | |
termContainsValue | public boolean termContainsValue(Term term)(Code) | | |
|
|