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

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

Detailed Description

Named symbols

Definition at line 25 of file StringSymbol.java.


Constructor & Destructor Documentation

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

Member Function Documentation

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