Z3
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) ^ true)
36  throw new Z3Exception("Numeral is not an int");
37  return res.value;
38  }
39 
45  public long getLong()
46  {
47  Native.LongPtr res = new Native.LongPtr();
48  if (Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res) ^ true)
49  throw new Z3Exception("Numeral is not a long");
50  return res.value;
51  }
52 
56  public BigInteger getBigInteger()
57  {
58  return new BigInteger(this.toString());
59  }
60 
64  public String toString()
65  {
66  try
67  {
68  return Native.getNumeralString(getContext().nCtx(), getNativeObject());
69  } catch (Z3Exception e)
70  {
71  return "Z3Exception: " + e.getMessage();
72  }
73  }
74 
75  BitVecNum(Context ctx, long obj)
76  {
77  super(ctx, obj);
78  }
79 }
BigInteger getBigInteger()
Definition: BitVecNum.java:56
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