Public Member Functions | |
int | getInt () throws Z3Exception |
long | getLong () throws Z3Exception |
BigInteger | getBigInteger () |
String | toString () |
Package Functions | |
BitVecNum (Context ctx, long obj) throws Z3Exception |
Bit-vector numerals
Definition at line 25 of file BitVecNum.java.
BitVecNum | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
Definition at line 75 of file BitVecNum.java.
{ super(ctx, obj); }
BigInteger getBigInteger | ( | ) | [inline] |
Retrieve the BigInteger value.
Definition at line 56 of file BitVecNum.java.
{ return new BigInteger(this.toString()); }
int getInt | ( | ) | throws Z3Exception [inline] |
Retrieve the int value.
Z3Exception |
Definition at line 32 of file BitVecNum.java.
{ Native.IntPtr res = new Native.IntPtr(); if (Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res) ^ true) throw new Z3Exception("Numeral is not an int"); return res.value; }
long getLong | ( | ) | throws Z3Exception [inline] |
Retrieve the 64-bit int value.
Z3Exception |
Definition at line 45 of file BitVecNum.java.
{ Native.LongPtr res = new Native.LongPtr(); if (Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res) ^ true) throw new Z3Exception("Numeral is not a long"); return res.value; }
String toString | ( | ) | [inline] |
Returns a string representation of the numeral.
Reimplemented from Expr.
Definition at line 64 of file BitVecNum.java.
Referenced by BitVecNum.getBigInteger().
{ try { return Native.getNumeralString(getContext().nCtx(), getNativeObject()); } catch (Z3Exception e) { return "Z3Exception: " + e.getMessage(); } }