Go to the documentation of this file.00001
00018 package com.microsoft.z3;
00019
00020 import java.math.BigInteger;
00021
00025 public class IntNum extends IntExpr
00026 {
00027
00028 IntNum(Context ctx, long obj) throws Z3Exception
00029 {
00030 super(ctx, obj);
00031 }
00032
00036 public int getInt() throws Z3Exception
00037 {
00038 Native.IntPtr res = new Native.IntPtr();
00039 if (Native.getNumeralInt(getContext().nCtx(), getNativeObject(), res) ^ true)
00040 throw new Z3Exception("Numeral is not an int");
00041 return res.value;
00042 }
00043
00047 public long getInt64() throws Z3Exception
00048 {
00049 Native.LongPtr res = new Native.LongPtr();
00050 if (Native.getNumeralInt64(getContext().nCtx(), getNativeObject(), res) ^ true)
00051 throw new Z3Exception("Numeral is not an int64");
00052 return res.value;
00053 }
00054
00058 public BigInteger getBigInteger() throws Z3Exception
00059 {
00060 return new BigInteger(this.toString());
00061 }
00062
00066 public String toString()
00067 {
00068 try
00069 {
00070 return Native.getNumeralString(getContext().nCtx(), getNativeObject());
00071 } catch (Z3Exception e)
00072 {
00073 return "Z3Exception: " + e.getMessage();
00074 }
00075 }
00076 }