public class SMTTermVariable extends SMTTerm
SMTTerm.False, SMTTerm.True
Modifier and Type | Field and Description |
---|---|
(package private) java.lang.String |
id |
(package private) SMTTerm |
quant |
(package private) SMTSort |
sort |
Constructor and Description |
---|
SMTTermVariable(java.lang.String id,
SMTSort sort) |
Modifier and Type | Method and Description |
---|---|
SMTTermVariable |
copy() |
boolean |
equals(java.lang.Object term) |
java.lang.String |
getId() |
SMTTerm |
getQuant() |
SMTSort |
getSort() |
java.util.List<SMTTermVariable> |
getVars() |
int |
hashCode() |
SMTTerm |
instantiate(SMTTermVariable a,
SMTTerm b) |
boolean |
occurs(SMTTermVariable a) |
boolean |
occurs(java.lang.String id) |
SMTTerm |
replace(SMTTermCall a,
SMTTerm b) |
void |
setId(java.lang.String id) |
void |
setQuant(SMTTerm quant) |
void |
setSort(SMTSort sort) |
SMTSort |
sort() |
SMTTerm |
substitute(SMTTerm a,
SMTTerm b) |
SMTTerm |
substitute(SMTTermVariable a,
SMTTerm b) |
java.lang.String |
toSting() |
java.lang.String |
toString(int nestPos) |
and, and, binOp, c, call, call, call, call, call, call, call, call, concat, div, equal, equal, exists, exists, exists, exists, exists, exists, exists, exists, forall, forall, forall, forall, forall, forall, forall, forall, forall, forall, forall, getComment, getEQVars, getQuantVars, getSubs, getUQVars, gt, gte, iff, implies, implies, isCons, ite, lt, lte, minus, mul, multOp, not, not, number, number, or, or, plus, quant, quant, rem, setComment, sign, terms, terms, toList, toList, toString, unaryOp
public SMTTermVariable(java.lang.String id, SMTSort sort)
public java.lang.String getId()
public void setId(java.lang.String id)
public SMTSort getSort()
public void setSort(SMTSort sort)
public SMTTerm getQuant()
public void setQuant(SMTTerm quant)
quant
- the quant to setpublic boolean equals(java.lang.Object term)
equals
in class java.lang.Object
public int hashCode()
hashCode
in class java.lang.Object
public java.lang.String toSting()
public java.util.List<SMTTermVariable> getVars()
public boolean occurs(SMTTermVariable a)
public SMTTerm substitute(SMTTermVariable a, SMTTerm b)
substitute
in class SMTTerm
public SMTTerm substitute(SMTTerm a, SMTTerm b)
substitute
in class SMTTerm
public SMTTerm replace(SMTTermCall a, SMTTerm b)
public SMTTerm instantiate(SMTTermVariable a, SMTTerm b)
instantiate
in class SMTTerm
public SMTTermVariable copy()