Z3 |

Public Member Functions
IntNum Class Reference
Inheritance diagram for IntNum:

## Public Member Functions
int | getInt ()
long | getInt64 ()
BigInteger | getBigInteger ()
String | toString ()

## Detailed Description

Integer Numerals

Definition at line 25 of file IntNum.java.

## Member Function Documentation

## ◆ getBigInteger()

BigInteger getBigInteger | ( |  | ) |
| inline

Retrieve the BigInteger value.

Definition at line 58 of file IntNum.java.

59 {
60 return new BigInteger(this.toString());
61 }
com.microsoft.z3.IntNum.toString
String toString()
Definition: IntNum.java:66

## ◆ getInt()

int getInt | ( |  | ) |
| inline

Retrieve the int value.

Definition at line 36 of file IntNum.java.

37 {
38 Native.IntPtr res = new Native.IntPtr();
39 if (!Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res))
40 throw new Z3Exception("Numeral is not an int");
41 return res.value;
42 }

## ◆ getInt64()

long getInt64 | ( |  | ) |
| inline

Retrieve the 64-bit int value.

Definition at line 47 of file IntNum.java.

48 {
49 Native.LongPtr res = new Native.LongPtr();
50 if (!Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res))
51 throw new Z3Exception("Numeral is not an int64");
52 return res.value;
53 }

## ◆ toString()

String toString | ( |  | ) |
| inline

Returns a string representation of the numeral.

Definition at line 66 of file IntNum.java.

66 {
67 return Native.getNumeralString(getContext().nCtx(), getNativeObject());
68 }

Referenced by RatNum.getBigIntDenominator(), IntNum.getBigInteger(), and RatNum.getBigIntNumerator().