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