public class SMTTermUnaryOp extends SMTTerm
Modifier and Type | Class and Description |
---|---|
static class |
SMTTermUnaryOp.Op |
SMTTerm.False, SMTTerm.True
Modifier and Type | Field and Description |
---|---|
private SMTTermUnaryOp.Op |
operator |
private SMTTerm |
sub |
Constructor and Description |
---|
SMTTermUnaryOp(SMTTermUnaryOp.Op operator,
SMTTerm sub) |
Modifier and Type | Method and Description |
---|---|
SMTTermUnaryOp |
copy() |
boolean |
equals(java.lang.Object term) |
java.util.List<SMTTermVariable> |
getEQVars() |
SMTTermUnaryOp.Op |
getOperator() |
java.util.List<SMTTermVariable> |
getQuantVars() |
SMTTerm |
getSub() |
java.util.List<SMTTermVariable> |
getUQVars() |
java.util.List<SMTTermVariable> |
getVars() |
int |
hashCode() |
SMTTerm |
instantiate(SMTTermVariable a,
SMTTerm b) |
boolean |
occurs(SMTTermVariable a) |
boolean |
occurs(java.lang.String id) |
SMTTerm |
replace(SMTTermCall a,
SMTTerm b) |
void |
setOperator(SMTTermUnaryOp.Op operator) |
void |
setSub(SMTTerm subForm) |
SMTSort |
sort() |
SMTTerm |
substitute(SMTTerm a,
SMTTerm b) |
SMTTerm |
substitute(SMTTermVariable a,
SMTTerm b) |
java.lang.String |
toSting() |
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, getSubs, 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, toString, unaryOp
private SMTTermUnaryOp.Op operator
private SMTTerm sub
public SMTTermUnaryOp(SMTTermUnaryOp.Op operator, SMTTerm sub)
operator
- sub
- public SMTTermUnaryOp.Op getOperator()
public void setOperator(SMTTermUnaryOp.Op operator)
operator
- the operator to setpublic SMTTerm getSub()
public void setSub(SMTTerm subForm)
subForm
- the subForm to setpublic java.util.List<SMTTermVariable> getQuantVars()
getQuantVars
in class SMTTerm
public java.util.List<SMTTermVariable> getUQVars()
public java.util.List<SMTTermVariable> getEQVars()
public java.util.List<SMTTermVariable> getVars()
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 SMTTermUnaryOp copy()
public boolean equals(java.lang.Object term)
equals
in class java.lang.Object
public int hashCode()
hashCode
in class java.lang.Object
public java.lang.String toSting()