Z3
src
api
java
BitVecNum.java
Go to the documentation of this file.
1
18
package
com.microsoft.z3;
19
20
import
java.math.BigInteger;
21
25
public
class
BitVecNum
extends
BitVecExpr
26
{
32
public
int
getInt
()
33
{
34
Native
.
IntPtr
res =
new
Native
.
IntPtr
();
35
if
(!
Native
.
getNumeralInt
(getContext().nCtx(), getNativeObject(), res)) {
36
throw
new
Z3Exception
(
"Numeral is not an int"
);
37
}
38
return
res.value;
39
}
40
46
public
long
getLong
()
47
{
48
Native
.
LongPtr
res =
new
Native
.
LongPtr
();
49
if
(!
Native
.
getNumeralInt64
(getContext().nCtx(), getNativeObject(), res)) {
50
throw
new
Z3Exception
(
"Numeral is not a long"
);
51
}
52
return
res.value;
53
}
54
58
public
BigInteger
getBigInteger
()
59
{
60
return
new
BigInteger(this.
toString
());
61
}
62
66
@Override
67
public
String
toString
()
68
{
69
return
Native
.
getNumeralString
(getContext().nCtx(), getNativeObject());
70
}
71
72
BitVecNum
(
Context
ctx,
long
obj)
73
{
74
super(ctx, obj);
75
}
76
}
com.microsoft.z3.BitVecNum.getLong
long getLong()
Definition:
BitVecNum.java:46
com.microsoft.z3.BitVecNum.toString
String toString()
Definition:
BitVecNum.java:67
com.microsoft.z3.BitVecNum.getInt
int getInt()
Definition:
BitVecNum.java:32
com.microsoft.z3.Native.IntPtr
Definition:
Native.java:5
com.microsoft.z3.BitVecNum
Definition:
BitVecNum.java:25
com.microsoft.z3.BitVecExpr
Definition:
BitVecExpr.java:23
com.microsoft.z3.Native.getNumeralInt64
static boolean getNumeralInt64(long a0, long a1, LongPtr a2)
Definition:
Native.java:3262
com.microsoft.z3.Native.LongPtr
Definition:
Native.java:6
com.microsoft.z3.Native
Definition:
Native.java:4
com.microsoft.z3.Native.getNumeralString
static String getNumeralString(long a0, long a1)
Definition:
Native.java:3181
com.microsoft.z3.Z3Exception
Definition:
Z3Exception.java:25
com.microsoft.z3.Native.getNumeralInt
static boolean getNumeralInt(long a0, long a1, IntPtr a2)
Definition:
Native.java:3235
com.microsoft.z3.Context
Definition:
Context.java:35
com.microsoft.z3.BitVecNum.getBigInteger
BigInteger getBigInteger()
Definition:
BitVecNum.java:58
z3py.String
def String(name, ctx=None)
Definition:
z3py.py:10111
Generated on Thu May 14 2020 00:00:00 for Z3 by
1.8.17