Z3
src/api/java/Symbol.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 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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines