Z3
Loading...
Searching...
No Matches
src
api
java
IntNum.java
Go to the documentation of this file.
1
18
package
com.microsoft.z3;
19
20
import
java.math.BigInteger;
21
25
public
class
IntNum
extends
IntExpr
26
{
27
28
IntNum
(
Context
ctx,
long
obj)
29
{
30
super(ctx, obj);
31
}
32
36
public
int
getInt
()
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
}
43
47
public
long
getInt64
()
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
}
54
58
public
BigInteger
getBigInteger
()
59
{
60
return
new
BigInteger(this.
toString
());
61
}
62
66
public
String
toString
() {
67
return
Native.getNumeralString(getContext().nCtx(), getNativeObject());
68
}
69
}
com.microsoft.z3.Context
Definition
Context.java:36
com.microsoft.z3.IntExpr
Definition
IntExpr.java:24
com.microsoft.z3.IntNum
Definition
IntNum.java:26
com.microsoft.z3.IntNum.getInt
int getInt()
Definition
IntNum.java:36
com.microsoft.z3.IntNum.getBigInteger
BigInteger getBigInteger()
Definition
IntNum.java:58
com.microsoft.z3.IntNum.toString
String toString()
Definition
IntNum.java:66
com.microsoft.z3.IntNum.getInt64
long getInt64()
Definition
IntNum.java:47
com.microsoft.z3.Z3Exception
Definition
Z3Exception.java:26
Generated on Sat Dec 20 2025 19:33:21 for Z3 by
1.9.8