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