Method getEntries

src/api/java/Statistics.java:135–156

The data entries. @throws Z3Exception

()

     * @throws Z3Exception
     **/
    public Entry[] getEntries()
    {

        int n = size();
        Entry[] res = new Entry[n];
        for (int i = 0; i < n; i++)
        {
            Entry e;
            String k = Native.statsGetKey(getContext().nCtx(), getNativeObject(), i);
            if (Native.statsIsUint(getContext().nCtx(), getNativeObject(), i)) {
                e = new Entry(k, Native.statsGetUintValue(getContext().nCtx(),
                    getNativeObject(), i));
            } else if (Native.statsIsDouble(getContext().nCtx(), getNativeObject(), i)) {
                e = new Entry(k, Native.statsGetDoubleValue(getContext().nCtx(),
                    getNativeObject(), i));
            } else {
                throw new Z3Exception("Unknown data entry value");
            }
            res[i] = e;
        }
        return res;
    }

    /**
     * The statistical counters.