Go to the documentation of this file.00001
00018 package com.microsoft.z3;
00019
00020 import java.math.BigInteger;
00021
00025 public class BitVecNum extends BitVecExpr
00026 {
00032 public int getInt() throws Z3Exception
00033 {
00034 Native.IntPtr res = new Native.IntPtr();
00035 if (Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res) ^ true)
00036 throw new Z3Exception("Numeral is not an int");
00037 return res.value;
00038 }
00039
00045 public long getLong() throws Z3Exception
00046 {
00047 Native.LongPtr res = new Native.LongPtr();
00048 if (Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res) ^ true)
00049 throw new Z3Exception("Numeral is not a long");
00050 return res.value;
00051 }
00052
00056 public BigInteger getBigInteger()
00057 {
00058 return new BigInteger(this.toString());
00059 }
00060
00064 public String toString()
00065 {
00066 try
00067 {
00068 return Native.getNumeralString(getContext().nCtx(), getNativeObject());
00069 } catch (Z3Exception e)
00070 {
00071 return "Z3Exception: " + e.getMessage();
00072 }
00073 }
00074
00075 BitVecNum(Context ctx, long obj) throws Z3Exception
00076 {
00077 super(ctx, obj);
00078 }
00079 }