Public Member Functions | |
int | getInt () throws Z3Exception |
long | getInt64 () throws Z3Exception |
BigInteger | getBigInteger () throws Z3Exception |
String | toString () |
Package Functions | |
IntNum (Context ctx, long obj) throws Z3Exception |
Integer Numerals
Definition at line 25 of file IntNum.java.
IntNum | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
Definition at line 28 of file IntNum.java.
{ super(ctx, obj); }
BigInteger getBigInteger | ( | ) | throws Z3Exception [inline] |
Retrieve the BigInteger value.
Definition at line 58 of file IntNum.java.
{ return new BigInteger(this.toString()); }
int getInt | ( | ) | throws Z3Exception [inline] |
Retrieve the int value.
Definition at line 36 of file IntNum.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 getInt64 | ( | ) | throws Z3Exception [inline] |
Retrieve the 64-bit int value.
Definition at line 47 of file IntNum.java.
{ Native.LongPtr res = new Native.LongPtr(); if (Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res) ^ true) throw new Z3Exception("Numeral is not an int64"); return res.value; }
String toString | ( | ) | [inline] |
Returns a string representation of the numeral.
Reimplemented from Expr.
Definition at line 66 of file IntNum.java.
Referenced by RatNum.getBigIntDenominator(), IntNum.getBigInteger(), and RatNum.getBigIntNumerator().
{ try { return Native.getNumeralString(getContext().nCtx(), getNativeObject()); } catch (Z3Exception e) { return "Z3Exception: " + e.getMessage(); } }