00001 00018 package com.microsoft.z3; 00019 00020 import com.microsoft.z3.enumerations.Z3_symbol_kind; 00021 00025 public class Symbol extends Z3Object 00026 { 00030 protected Z3_symbol_kind getKind() throws Z3Exception 00031 { 00032 return Z3_symbol_kind.fromInt(Native.getSymbolKind(getContext().nCtx(), 00033 getNativeObject())); 00034 } 00035 00039 public boolean isIntSymbol() throws Z3Exception 00040 { 00041 return getKind() == Z3_symbol_kind.Z3_INT_SYMBOL; 00042 } 00043 00047 public boolean isStringSymbol() throws Z3Exception 00048 { 00049 return getKind() == Z3_symbol_kind.Z3_STRING_SYMBOL; 00050 } 00051 00055 public String toString() 00056 { 00057 try 00058 { 00059 if (isIntSymbol()) 00060 return Integer.toString(((IntSymbol) this).getInt()); 00061 else if (isStringSymbol()) 00062 return ((StringSymbol) this).getString(); 00063 else 00064 return new String( 00065 "Z3Exception: Unknown symbol kind encountered."); 00066 } catch (Z3Exception ex) 00067 { 00068 return new String("Z3Exception: " + ex.getMessage()); 00069 } 00070 } 00071 00075 protected Symbol(Context ctx, long obj) throws Z3Exception 00076 { 00077 super(ctx, obj); 00078 } 00079 00080 static Symbol create(Context ctx, long obj) throws Z3Exception 00081 { 00082 switch (Z3_symbol_kind.fromInt(Native.getSymbolKind(ctx.nCtx(), obj))) 00083 { 00084 case Z3_INT_SYMBOL: 00085 return new IntSymbol(ctx, obj); 00086 case Z3_STRING_SYMBOL: 00087 return new StringSymbol(ctx, obj); 00088 default: 00089 throw new Z3Exception("Unknown symbol kind encountered"); 00090 } 00091 } 00092 }