public class SMTTerms extends SMTTerm
SMTTerm.False, SMTTerm.True
Modifier and Type | Method and Description |
---|---|
void |
add(SMTTerm t) |
SMTTerms |
copy() |
List<SMTTerm> |
flatten() |
List<SMTTerm> |
getTerms() |
SMTTerm |
instantiate(SMTTermVariable a,
SMTTerm b) |
boolean |
occurs(SMTTermVariable a) |
boolean |
occurs(String id) |
SMTTerm |
replace(SMTTermCall a,
SMTTerm b) |
void |
setTerms(List<SMTTerm> terms) |
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, getQuantVars, 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 void add(SMTTerm t)