FuncDecl Class Reference

Inheritance diagram for FuncDecl:

Data Structures
class	Parameter

Public Member Functions
boolean	equals (Object o)
int	hashCode ()
String	toString ()
int	getId ()
int	getArity ()
int	getDomainSize ()
Sort[]	getDomain ()
Sort	getRange ()
Z3_decl_kind	getDeclKind ()
Symbol	getName ()
int	getNumParameters ()
Parameter[]	getParameters ()
Expr	apply (Expr...args)
Public Member Functions inherited from AST
boolean	equals (Object o)
int	compareTo (Object other)
int	hashCode ()
int	getId ()
AST	translate (Context ctx)
Z3_ast_kind	getASTKind ()
boolean	isExpr ()
boolean	isApp ()
boolean	isVar ()
boolean	isQuantifier ()
boolean	isSort ()
boolean	isFuncDecl ()
String	toString ()
String	getSExpr ()
Public Member Functions inherited from Z3Object
void	dispose ()
Public Member Functions inherited from IDisposable
void	dispose ()

Additional Inherited Members
Protected Member Functions inherited from Z3Object
void	finalize ()

Detailed Description

Function declarations.

Definition at line 27 of file FuncDecl.java.

Member Function Documentation

Expr apply ( Expr...  args )

inline

Create expression that applies function to arguments.

Parameters

args

Returns

Definition at line 377 of file FuncDecl.java.

Referenced by Tactic.__call__().

    {
        getContext().checkContextMatch(args);
        return Expr.create(getContext(), this, args);
    }

boolean equals ( Object  o )

inline

Object comparison.

Definition at line 32 of file FuncDecl.java.

    {
        FuncDecl casted = null;

        try {
            casted = FuncDecl.class.cast(o);
        } catch (ClassCastException e) {
            return false;
        }

        return  
            (this == casted) || 
            (this != null) &&
            (casted != null) &&
            (getContext().nCtx() == casted.getContext().nCtx()) &&
            (Native.isEqFuncDecl(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
    }

int getArity ( )

inline

The arity of the function declaration

Definition at line 83 of file FuncDecl.java.

Referenced by Model.getConstInterp(), and Model.getFuncInterp().

    {
        return Native.getArity(getContext().nCtx(), getNativeObject());
    }

Z3_decl_kind getDeclKind ( )

inline

The kind of the function declaration.

Definition at line 125 of file FuncDecl.java.

    {
        return Z3_decl_kind.fromInt(Native.getDeclKind(getContext().nCtx(),
                getNativeObject()));
    }

Sort [] getDomain ( )

inline

The domain of the function declaration

Definition at line 100 of file FuncDecl.java.

    {

        int n = getDomainSize();

        Sort[] res = new Sort[n];
        for (int i = 0; i < n; i++)
            res[i] = Sort.create(getContext(),
                    Native.getDomain(getContext().nCtx(), getNativeObject(), i));
        return res;
    }

int getDomainSize ( )

inline

The size of the domain of the function declaration

See Also

getArity

Definition at line 92 of file FuncDecl.java.

Referenced by FuncDecl.getDomain().

    {
        return Native.getDomainSize(getContext().nCtx(), getNativeObject());
    }

int getId ( )

inline

Returns a unique identifier for the function declaration.

Definition at line 75 of file FuncDecl.java.

    {
        return Native.getFuncDeclId(getContext().nCtx(), getNativeObject());
    }

Symbol getName ( )

inline

The name of the function declaration

Definition at line 134 of file FuncDecl.java.

    {

        return Symbol.create(getContext(),
                Native.getDeclName(getContext().nCtx(), getNativeObject()));
    }

int getNumParameters ( )

inline

The number of parameters of the function declaration

Definition at line 144 of file FuncDecl.java.

Referenced by FuncDecl.getParameters().

    {
        return Native.getDeclNumParameters(getContext().nCtx(), getNativeObject());
    }

Parameter [] getParameters ( )

inline

The parameters of the function declaration

Definition at line 152 of file FuncDecl.java.

    {

        int num = getNumParameters();
        Parameter[] res = new Parameter[num];
        for (int i = 0; i < num; i++)
        {
            Z3_parameter_kind k = Z3_parameter_kind.fromInt(Native
                    .getDeclParameterKind(getContext().nCtx(), getNativeObject(), i));
            switch (k)
            {
            case Z3_PARAMETER_INT:
                res[i] = new Parameter(k, Native.getDeclIntParameter(getContext()
                        .nCtx(), getNativeObject(), i));
                break;
            case Z3_PARAMETER_DOUBLE:
                res[i] = new Parameter(k, Native.getDeclDoubleParameter(
                        getContext().nCtx(), getNativeObject(), i));
                break;
            case Z3_PARAMETER_SYMBOL:
                res[i] = new Parameter(k, Symbol.create(getContext(), Native
                        .getDeclSymbolParameter(getContext().nCtx(),
                                getNativeObject(), i)));
                break;
            case Z3_PARAMETER_SORT:
                res[i] = new Parameter(k, Sort.create(getContext(), Native
                        .getDeclSortParameter(getContext().nCtx(), getNativeObject(),
                                i)));
                break;
            case Z3_PARAMETER_AST:
                res[i] = new Parameter(k, new AST(getContext(),
                        Native.getDeclAstParameter(getContext().nCtx(),
                                getNativeObject(), i)));
                break;
            case Z3_PARAMETER_FUNC_DECL:
                res[i] = new Parameter(k, new FuncDecl(getContext(),
                        Native.getDeclFuncDeclParameter(getContext().nCtx(),
                                getNativeObject(), i)));
                break;
            case Z3_PARAMETER_RATIONAL:
                res[i] = new Parameter(k, Native.getDeclRationalParameter(
                        getContext().nCtx(), getNativeObject(), i));
                break;
            default:
                throw new Z3Exception(
                        "Unknown function declaration parameter kind encountered");
            }
        }
        return res;
    }

Sort getRange ( )

inline

The range of the function declaration

Definition at line 115 of file FuncDecl.java.

    {

        return Sort.create(getContext(),
                Native.getRange(getContext().nCtx(), getNativeObject()));
    }

int hashCode ( )

inline

A hash code.

Definition at line 53 of file FuncDecl.java.

    {
        return super.hashCode();
    }

String toString ( )

inline

A string representations of the function declaration.

Definition at line 61 of file FuncDecl.java.

    {
        try
        {
            return Native.funcDeclToString(getContext().nCtx(), getNativeObject());
        } catch (Z3Exception e)
        {
            return "Z3Exception: " + e.getMessage();
        }
    }