public class Substitution extends 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,
TermServices services) |
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(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) |
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, TermServices services)
public Term applyWithoutCasts(Term t, TermServices services)
public boolean termContainsValue(Term term)