public class Substitution
extends java.lang.Object
Modifier and Type | Field and Description |
---|---|
private ImmutableMap<QuantifiableVariable,Term> |
varMap |
Constructor and Description |
---|
Substitution(ImmutableMap<QuantifiableVariable,Term> map) |
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() |
private final ImmutableMap<QuantifiableVariable,Term> varMap
public Substitution(ImmutableMap<QuantifiableVariable,Term> map)
public ImmutableMap<QuantifiableVariable,Term> getVarMap()
public Term getSubstitutedTerm(QuantifiableVariable var)
public boolean isTotalOn(ImmutableSet<QuantifiableVariable> vars)
public boolean isGround()
public Term apply(Term t, TermServices services)
private Term applySubst(QuantifiableVariable var, Term instance, Term t, TermBuilder tb)
public Term applyWithoutCasts(Term t, TermServices services)
public boolean equals(java.lang.Object arg0)
equals
in class java.lang.Object
public int hashCode()
hashCode
in class java.lang.Object
public java.lang.String toString()
toString
in class java.lang.Object
public boolean termContainsValue(Term term)