Symbol Class Reference

Inheritance diagram for Symbol:

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

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

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  ) throws Z3Exception

inlineprotected

Symbol constructor

Definition at line 75 of file Symbol.java.

    {
        super(ctx, obj);
    }

Member Function Documentation

Z3_symbol_kind getKind ( ) throws Z3Exception

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