public class SMTTermITE extends SMTTerm
SMTTerm.False, SMTTerm.True
Modifier and Type | Field and Description |
---|---|
(package private) SMTTerm |
condition |
(package private) SMTTerm |
falseCase |
private static java.lang.String |
ITE_STRING |
(package private) SMTTerm |
trueCase |
Constructor and Description |
---|
SMTTermITE(SMTTerm condition,
SMTTerm trueCase,
SMTTerm falseCase) |
Modifier and Type | Method and Description |
---|---|
SMTTerm |
copy() |
boolean |
equals(java.lang.Object that) |
SMTTerm |
getCondition() |
SMTTerm |
getFalseCase() |
java.util.List<SMTTermVariable> |
getQuantVars() |
SMTTerm |
getTrueCase() |
SMTTerm |
instantiate(SMTTermVariable a,
SMTTerm b) |
boolean |
occurs(SMTTermVariable a) |
boolean |
occurs(java.lang.String id) |
SMTTerm |
replace(SMTTermCall a,
SMTTerm b) |
void |
setCondition(SMTTerm condition) |
void |
setFalseCase(SMTTerm falseCase) |
void |
setTrueCase(SMTTerm trueCase) |
SMTSort |
sort() |
SMTTerm |
substitute(SMTTerm a,
SMTTerm b) |
SMTTerm |
substitute(SMTTermVariable a,
SMTTerm b) |
java.lang.String |
toString() |
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, getSubs, getUQVars, getVars, 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, unaryOp
SMTTerm condition
SMTTerm trueCase
SMTTerm falseCase
private static final java.lang.String ITE_STRING
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 boolean equals(java.lang.Object that)
equals
in class java.lang.Object
public SMTTerm getCondition()
public SMTTerm getTrueCase()
public SMTTerm getFalseCase()
public void setCondition(SMTTerm condition)
condition
- the condition to setpublic void setTrueCase(SMTTerm trueCase)
trueCase
- the trueCase to setpublic void setFalseCase(SMTTerm falseCase)
falseCase
- the falseCase to setpublic java.util.List<SMTTermVariable> getQuantVars()
getQuantVars
in class SMTTerm