Method getNames

src/api/java/ParamDescrs.java:62–72

Retrieve all names of parameters. @throws Z3Exception

()

     * @throws Z3Exception
     **/
    public Symbol[] getNames()
    {
        int sz = Native.paramDescrsSize(getContext().nCtx(), getNativeObject());
        Symbol[] names = new Symbol[sz];
        for (int i = 0; i < sz; ++i)
        {
            names[i] = Symbol.create(getContext(), Native.paramDescrsGetName(
                    getContext().nCtx(), getNativeObject(), i));
        }
        return names;
    }

    /**
     * The size of the ParamDescrs.