Z3
src/api/java/IntNum.java
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines