Symbol Class Reference

Inheritance diagram for Symbol:

Public Member Functions
boolean	isIntSymbol () throws Z3Exception
boolean	isStringSymbol () throws Z3Exception
String	toString ()
Protected Member Functions
Z3_symbol_kind	getKind () throws Z3Exception
	Symbol (Context ctx, long obj) throws Z3Exception
Static Package Functions
static Symbol	create (Context ctx, long obj) 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 [inline, protected]

Symbol constructor

Definition at line 75 of file Symbol.java.

    {
        super(ctx, obj);
    }

---

Member Function Documentation

static Symbol create	(	Context	ctx,
		long	obj
	)		throws Z3Exception [inline, static, package]

Definition at line 80 of file Symbol.java.

Referenced by Quantifier.getBoundVariableNames(), Sort.getName(), FuncDecl.getName(), ParamDescrs.getNames(), and FuncDecl.getParameters().

    {
        switch (Z3_symbol_kind.fromInt(Native.getSymbolKind(ctx.nCtx(), obj)))
        {
        case Z3_INT_SYMBOL:
            return new IntSymbol(ctx, obj);
        case Z3_STRING_SYMBOL:
            return new StringSymbol(ctx, obj);
        default:
            throw new Z3Exception("Unknown symbol kind encountered");
        }
    }

Z3_symbol_kind getKind

(

)

throws Z3Exception [inline, protected]

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