Z3
src/api/java/IntSymbol.java
Go to the documentation of this file.
00001 
00018 package com.microsoft.z3;
00019 
00020 import com.microsoft.z3.enumerations.Z3_symbol_kind;
00021 
00025 public class IntSymbol extends Symbol
00026 {
00031     public int getInt() throws Z3Exception
00032     {
00033         if (!isIntSymbol())
00034             throw new Z3Exception("Int requested from non-Int symbol");
00035         return Native.getSymbolInt(getContext().nCtx(), getNativeObject());
00036     }
00037 
00038     IntSymbol(Context ctx, long obj) throws Z3Exception
00039     {
00040         super(ctx, obj);
00041     }
00042 
00043     IntSymbol(Context ctx, int i) throws Z3Exception
00044     {
00045         super(ctx, Native.mkIntSymbol(ctx.nCtx(), i));
00046     }
00047 
00048     void checkNativeObject(long obj) throws Z3Exception
00049     {
00050         if (Native.getSymbolKind(getContext().nCtx(), obj) != Z3_symbol_kind.Z3_INT_SYMBOL
00051                 .toInt())
00052             throw new Z3Exception("Symbol is not of integer kind");
00053         super.checkNativeObject(obj);
00054     }
00055 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines