00001 00018 package com.microsoft.z3; 00019 00020 import com.microsoft.z3.enumerations.Z3_symbol_kind; 00021 00025 public class StringSymbol extends Symbol 00026 { 00031 public String getString() throws Z3Exception 00032 { 00033 return Native.getSymbolString(getContext().nCtx(), getNativeObject()); 00034 } 00035 00036 StringSymbol(Context ctx, long obj) throws Z3Exception 00037 { 00038 super(ctx, obj); 00039 } 00040 00041 StringSymbol(Context ctx, String s) throws Z3Exception 00042 { 00043 super(ctx, Native.mkStringSymbol(ctx.nCtx(), s)); 00044 } 00045 00046 void checkNativeObject(long obj) throws Z3Exception 00047 { 00048 if (Native.getSymbolKind(getContext().nCtx(), obj) != Z3_symbol_kind.Z3_STRING_SYMBOL 00049 .toInt()) 00050 throw new Z3Exception("Symbol is not of String kind"); 00051 00052 super.checkNativeObject(obj); 00053 } 00054 }