00001 00018 package com.microsoft.z3; 00019 00020 import com.microsoft.z3.enumerations.Z3_symbol_kind; 00021 00025 public class IntSymbol extends Symbol 00026 { 00032 public int getInt() 00033 { 00034 if (!isIntSymbol()) 00035 throw new Z3Exception("Int requested from non-Int symbol"); 00036 return Native.getSymbolInt(getContext().nCtx(), getNativeObject()); 00037 } 00038 00039 IntSymbol(Context ctx, long obj) 00040 { 00041 super(ctx, obj); 00042 } 00043 00044 IntSymbol(Context ctx, int i) 00045 { 00046 super(ctx, Native.mkIntSymbol(ctx.nCtx(), i)); 00047 } 00048 00049 void checkNativeObject(long obj) 00050 { 00051 if (Native.getSymbolKind(getContext().nCtx(), obj) != Z3_symbol_kind.Z3_INT_SYMBOL 00052 .toInt()) 00053 throw new Z3Exception("Symbol is not of integer kind"); 00054 super.checkNativeObject(obj); 00055 } 00056 }
1.7.6.1