Z3 |

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
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10693