public class SMTTermNumber extends SMTTerm
SMTTerm.False, SMTTerm.True
Modifier and Type | Field and Description |
---|---|
private long |
bitSize |
private long |
intValue |
private SMTSort |
sort |
private SMTTerm |
upp |
Constructor and Description |
---|
SMTTermNumber(int n) |
SMTTermNumber(long n) |
SMTTermNumber(long intValue,
long bitSize,
SMTSort sort) |
Modifier and Type | Method and Description |
---|---|
SMTTermNumber |
copy() |
boolean |
equals(java.lang.Object term) |
boolean |
equals(SMTTerm term) |
boolean |
equals(SMTTermNumber tn) |
long |
getBitSize() |
long |
getIntValue() |
SMTTerm |
getUpp() |
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 |
setBitSize(int bitSize) |
void |
setIntValue(int intValue) |
void |
setUpp(SMTTerm upp) |
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, 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, toString, unaryOp
private long intValue
private long bitSize
private SMTTerm upp
private SMTSort sort
public SMTTermNumber(int n)
public SMTTermNumber(long n)
public SMTTermNumber(long intValue, long bitSize, SMTSort sort)
public long getIntValue()
public void setIntValue(int intValue)
intValue
- the intValue to setpublic long getBitSize()
public void setBitSize(int bitSize)
bitSize
- the bitSize to setpublic SMTTerm getUpp()
public void setUpp(SMTTerm upp)
upp
- the upp 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 SMTTermNumber copy()
public java.lang.String toSting()
public boolean equals(java.lang.Object term)
equals
in class java.lang.Object
public boolean equals(SMTTerm term)
public boolean equals(SMTTermNumber tn)
public int hashCode()
hashCode
in class java.lang.Object