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