Z3
FiniteDomainNum.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
20import java.math.BigInteger;
21
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
70 {
71 return Native.getNumeralString(getContext().nCtx(), getNativeObject());
72 }
73}
static boolean getNumeralInt(long a0, long a1, IntPtr a2)
Definition: Native.java:3233
static boolean getNumeralInt64(long a0, long a1, LongPtr a2)
Definition: Native.java:3260
static String getNumeralString(long a0, long a1)
Definition: Native.java:3179
def String(name, ctx=None)
Definition: z3py.py:10085