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) ^ true)
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) ^ true)
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  {
68  try
69  {
70  return Native.getNumeralString(getContext().nCtx(), getNativeObject());
71  } catch (Z3Exception e)
72  {
73  return "Z3Exception: " + e.getMessage();
74  }
75  }
76 }
BigInteger getBigInteger()
Definition: IntNum.java:58
static boolean getNumeralInt(long a0, long a1, IntPtr a2)
Definition: Native.java:2594
static String getNumeralString(long a0, long a1)
Definition: Native.java:2549
static boolean getNumeralInt64(long a0, long a1, LongPtr a2)
Definition: Native.java:2621