Method getParameters

src/api/java/FuncDecl.java:147–196

The parameters of the function declaration

()

     * The parameters of the function declaration
     **/
    public Parameter[] getParameters()
    {

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

    /**
     * Function declarations can have Parameters associated with them.