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 }