Symbol Class Reference

Inheritance diagram for Symbol:

Public Member Functions
boolean	isIntSymbol ()
boolean	isStringSymbol ()
String	toString ()
Public Member Functions inherited from Z3Object
void	dispose ()
Public Member Functions inherited from IDisposable
void	dispose ()

Protected Member Functions
Z3_symbol_kind	getKind ()
	Symbol (Context ctx, long obj)
Protected Member Functions inherited from Z3Object
void	finalize ()

Detailed Description

Symbols are used to name several term and type constructors.

Definition at line 25 of file Symbol.java.

Constructor & Destructor Documentation

Symbol ( Context  ctx, long  obj  )

inlineprotected

Symbol constructor

Definition at line 75 of file Symbol.java.

    {
        super(ctx, obj);
    }

Member Function Documentation

Z3_symbol_kind getKind ( )

inlineprotected

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 ( )

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 ( )

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