Z3
src
api
java
FiniteDomainNum.java
Go to the documentation of this file.
1
18
package
com.microsoft.z3;
19
20
import
java.math.BigInteger;
21
25
public
class
FiniteDomainNum
extends
FiniteDomainExpr
26
{
27
28
FiniteDomainNum
(
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
}
42
return
res.value;
43
}
44
48
public
long
getInt64
()
49
{
50
Native
.
LongPtr
res =
new
Native
.
LongPtr
();
51
if
(!
Native
.
getNumeralInt64
(getContext().nCtx(), getNativeObject(), res)) {
52
throw
new
Z3Exception
(
"Numeral is not an int64"
);
53
}
54
return
res.value;
55
}
56
60
public
BigInteger
getBigInteger
()
61
{
62
return
new
BigInteger(this.
toString
());
63
}
64
68
@Override
69
public
String
toString
()
70
{
71
return
Native
.
getNumeralString
(getContext().nCtx(), getNativeObject());
72
}
73
}
com.microsoft.z3.FiniteDomainNum.getInt
int getInt()
Definition:
FiniteDomainNum.java:36
com.microsoft.z3.FiniteDomainNum
Definition:
FiniteDomainNum.java:25
com.microsoft.z3.Native.IntPtr
Definition:
Native.java:5
com.microsoft.z3.Context
Definition:
Context.java:29
com.microsoft.z3.Native
Definition:
Native.java:4
com.microsoft.z3.Native.getNumeralInt
static boolean getNumeralInt(long a0, long a1, IntPtr a2)
Definition:
Native.java:2861
com.microsoft.z3.Native.getNumeralString
static String getNumeralString(long a0, long a1)
Definition:
Native.java:2816
com.microsoft.z3.Native.LongPtr
Definition:
Native.java:6
com.microsoft.z3.FiniteDomainExpr
Definition:
FiniteDomainExpr.java:23
com.microsoft.z3.FiniteDomainNum.toString
String toString()
Definition:
FiniteDomainNum.java:69
com.microsoft.z3.Z3Exception
Definition:
Z3Exception.java:25
com.microsoft.z3.FiniteDomainNum.getBigInteger
BigInteger getBigInteger()
Definition:
FiniteDomainNum.java:60
com.microsoft.z3.Native.getNumeralInt64
static boolean getNumeralInt64(long a0, long a1, LongPtr a2)
Definition:
Native.java:2888
z3py.String
def String(name, ctx=None)
Definition:
z3py.py:9443
com.microsoft.z3.FiniteDomainNum.getInt64
long getInt64()
Definition:
FiniteDomainNum.java:48
Generated on Sat Nov 12 2016 23:18:40 for Z3 by
1.8.12