Public Member Functions | |
String | getString () throws Z3Exception |
Package Functions | |
StringSymbol (Context ctx, long obj) throws Z3Exception | |
StringSymbol (Context ctx, String s) throws Z3Exception | |
void | checkNativeObject (long obj) throws Z3Exception |
Named symbols
Definition at line 25 of file StringSymbol.java.
StringSymbol | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
Definition at line 36 of file StringSymbol.java.
{ super(ctx, obj); }
StringSymbol | ( | Context | ctx, |
String | s | ||
) | throws Z3Exception [inline, package] |
Definition at line 41 of file StringSymbol.java.
{ super(ctx, Native.mkStringSymbol(ctx.nCtx(), s)); }
void checkNativeObject | ( | long | obj | ) | throws Z3Exception [inline, package] |
Reimplemented from Z3Object.
Definition at line 46 of file StringSymbol.java.
{ if (Native.getSymbolKind(getContext().nCtx(), obj) != Z3_symbol_kind.Z3_STRING_SYMBOL .toInt()) throw new Z3Exception("Symbol is not of String kind"); super.checkNativeObject(obj); }
String getString | ( | ) | throws Z3Exception [inline] |
The string value of the symbol. Throws an exception if the symbol is not of string kind.
Definition at line 31 of file StringSymbol.java.
{ return Native.getSymbolString(getContext().nCtx(), getNativeObject()); }