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 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(Object that) |
SMTTerm |
getCondition() |
SMTTerm |
getFalseCase() |
List<SMTTermVariable> |
getQuantVars() |
SMTTerm |
getTrueCase() |
SMTTerm |
instantiate(SMTTermVariable a,
SMTTerm b) |
boolean |
occurs(SMTTermVariable a) |
boolean |
occurs(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) |
String |
toString() |
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 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 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 List<SMTTermVariable> getQuantVars()
getQuantVars
in class SMTTerm