Public Member Functions | |
boolean | isIntSymbol () throws Z3Exception |
boolean | isStringSymbol () throws Z3Exception |
String | toString () |
Protected Member Functions | |
Z3_symbol_kind | getKind () throws Z3Exception |
Symbol (Context ctx, long obj) throws Z3Exception | |
Static Package Functions | |
static Symbol | create (Context ctx, long obj) throws Z3Exception |
Symbols are used to name several term and type constructors.
Definition at line 25 of file Symbol.java.
Symbol | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, protected] |
static Symbol create | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, static, package] |
Definition at line 80 of file Symbol.java.
Referenced by Quantifier.getBoundVariableNames(), Sort.getName(), FuncDecl.getName(), ParamDescrs.getNames(), and FuncDecl.getParameters().
{ switch (Z3_symbol_kind.fromInt(Native.getSymbolKind(ctx.nCtx(), obj))) { case Z3_INT_SYMBOL: return new IntSymbol(ctx, obj); case Z3_STRING_SYMBOL: return new StringSymbol(ctx, obj); default: throw new Z3Exception("Unknown symbol kind encountered"); } }
Z3_symbol_kind getKind | ( | ) | throws Z3Exception [inline, protected] |
The kind of the symbol (int or string)
Definition at line 30 of file Symbol.java.
Referenced by Symbol.isIntSymbol(), and Symbol.isStringSymbol().
{ return Z3_symbol_kind.fromInt(Native.getSymbolKind(getContext().nCtx(), getNativeObject())); }
boolean isIntSymbol | ( | ) | throws Z3Exception [inline] |
Indicates whether the symbol is of Int kind
Definition at line 39 of file Symbol.java.
Referenced by IntSymbol.getInt(), and Symbol.toString().
{ return getKind() == Z3_symbol_kind.Z3_INT_SYMBOL; }
boolean isStringSymbol | ( | ) | throws Z3Exception [inline] |
Indicates whether the symbol is of string kind.
Definition at line 47 of file Symbol.java.
Referenced by Symbol.toString().
{ return getKind() == Z3_symbol_kind.Z3_STRING_SYMBOL; }
String toString | ( | ) | [inline] |
A string representation of the symbol.
Definition at line 55 of file Symbol.java.
{ try { if (isIntSymbol()) return Integer.toString(((IntSymbol) this).getInt()); else if (isStringSymbol()) return ((StringSymbol) this).getString(); else return new String( "Z3Exception: Unknown symbol kind encountered."); } catch (Z3Exception ex) { return new String("Z3Exception: " + ex.getMessage()); } }