Symbol Class Reference

Inheritance diagram for Symbol:

Public Member Functions
boolean	isIntSymbol ()
boolean	isStringSymbol ()
boolean	equals (Object o)
String	toString ()

Protected Member Functions
Z3_symbol_kind	getKind ()
	Symbol (Context ctx, long obj)

Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[]	arrayToNative (Z3Object[] a)
static int	arrayLength (Z3Object[] a)

Detailed Description

Symbols are used to name several term and type constructors.

Definition at line 25 of file Symbol.java.

Constructor & Destructor Documentation

Symbol()

Symbol ( Context  ctx, long  obj  )

inlineprotected

Symbol constructor

Definition at line 77 of file Symbol.java.

    {
        super(ctx, obj);
    }

Referenced by Symbol.equals().

Member Function Documentation

equals()

boolean equals ( Object  o )

inline

Definition at line 52 of file Symbol.java.

    {
        if (o == this) return true;
        if (!(o instanceof Symbol)) return false;
        Symbol other = (Symbol) o;
        return this.getNativeObject() == other.getNativeObject();
    }

getKind()

Z3_symbol_kind getKind ( )

inlineprotected

The kind of the symbol (int or string)

Definition at line 29 of file Symbol.java.

    {
        return Z3_symbol_kind.fromInt(Native.getSymbolKind(getContext().nCtx(),
                getNativeObject()));
    }

Referenced by Symbol.isIntSymbol(), and Symbol.isStringSymbol().

isIntSymbol()

boolean isIntSymbol ( )

inline

Indicates whether the symbol is of Int kind

Definition at line 38 of file Symbol.java.

    {
        return getKind() == Z3_symbol_kind.Z3_INT_SYMBOL;
    }

Referenced by IntSymbol.getInt(), and Symbol.toString().

isStringSymbol()

boolean isStringSymbol ( )

inline

Indicates whether the symbol is of string kind.

Definition at line 46 of file Symbol.java.

    {
        return getKind() == Z3_symbol_kind.Z3_STRING_SYMBOL;
    }

Referenced by Symbol.toString().

toString()

String toString ( )

inline

A string representation of the symbol.

Definition at line 64 of file Symbol.java.

                             {
        if (isIntSymbol()) {
            return Integer.toString(((IntSymbol) this).getInt());
        } else if (isStringSymbol()) {
            return ((StringSymbol) this).getString();
        } else {
            return "Z3Exception: Unknown symbol kind encountered.";
        }
    }