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  }

◆ 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().

com.microsoft.z3.IntNum.toString
String toString()
Definition: IntNum.java:66