Public Member Functions | |
int | getInt () throws Z3Exception |
Package Functions | |
IntSymbol (Context ctx, long obj) throws Z3Exception | |
IntSymbol (Context ctx, int i) throws Z3Exception | |
void | checkNativeObject (long obj) throws Z3Exception |
Numbered symbols
Definition at line 25 of file IntSymbol.java.
IntSymbol | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
Definition at line 38 of file IntSymbol.java.
{ super(ctx, obj); }
IntSymbol | ( | Context | ctx, |
int | i | ||
) | throws Z3Exception [inline, package] |
Definition at line 43 of file IntSymbol.java.
{ super(ctx, Native.mkIntSymbol(ctx.nCtx(), i)); }
void checkNativeObject | ( | long | obj | ) | throws Z3Exception [inline, package] |
Reimplemented from Z3Object.
Definition at line 48 of file IntSymbol.java.
{ if (Native.getSymbolKind(getContext().nCtx(), obj) != Z3_symbol_kind.Z3_INT_SYMBOL .toInt()) throw new Z3Exception("Symbol is not of integer kind"); super.checkNativeObject(obj); }
int getInt | ( | ) | throws Z3Exception [inline] |
The int value of the symbol. Throws an exception if the symbol is not of int kind.
Definition at line 31 of file IntSymbol.java.
{ if (!isIntSymbol()) throw new Z3Exception("Int requested from non-Int symbol"); return Native.getSymbolInt(getContext().nCtx(), getNativeObject()); }