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