public class SMTTermITE extends SMTTerm
SMTTerm.False, SMTTerm.True
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
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
Copyright © 2003-2019 The KeY-Project.