SMTTerm.False, SMTTerm.True
Constructor and Description |
---|
False() |
Modifier and Type | Method and Description |
---|---|
SMTTerm |
and(SMTTerm right) |
SMTTerm |
copy() |
SMTTerm |
forall(java.util.List<SMTTermVariable> bindVars,
java.util.List<java.util.List<SMTTerm>> pats) |
SMTTerm |
iff(SMTTerm right) |
SMTTerm |
implies(SMTTerm right) |
SMTTerm |
instantiate(SMTTermVariable a,
SMTTerm b) |
boolean |
occurs(SMTTermVariable a) |
boolean |
occurs(java.lang.String id) |
SMTTerm |
or(SMTTerm right) |
SMTTerm |
replace(SMTTermCall a,
SMTTerm b) |
SMTTerm |
sign(boolean pol) |
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, 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, getComment, getEQVars, getQuantVars, getSubs, getUQVars, getVars, gt, gte, implies, isCons, ite, lt, lte, minus, mul, multOp, not, not, number, number, or, plus, quant, quant, rem, setComment, 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 SMTTerm forall(java.util.List<SMTTermVariable> bindVars, java.util.List<java.util.List<SMTTerm>> pats)