public class SMTTermUnaryOp extends SMTTerm
Modifier and Type | Class and Description |
---|---|
static class |
SMTTermUnaryOp.Op |
SMTTerm.False, SMTTerm.True
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
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()
Copyright © 2003-2019 The KeY-Project.