Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Package Functions
IntSymbol Class Reference
+ Inheritance diagram for IntSymbol:

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

Detailed Description

Numbered symbols

Definition at line 25 of file IntSymbol.java.


Constructor & Destructor Documentation

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));
    }

Member Function Documentation

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());
    }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines