Statistics.java

Go to the documentation of this file.

 
package com.microsoft.z3;
 
import java.lang.ref.ReferenceQueue;
 
public class Statistics extends Z3Object {
    public static class Entry
    {
        public String Key;
 
        public int getUIntValue()
        {
            return m_int;
        }
 
        public double getDoubleValue()
        {
            return m_double;
        }
 
        public boolean isUInt()
        {
            return m_is_int;
        }
 
        public boolean isDouble()
        {
            return m_is_double;
        }
 
        public String getValueString()
        {
            if (isUInt()) {
                return Integer.toString(m_int);
            } else if (isDouble()) {
                return Double.toString(m_double);
            } else {
                throw new Z3Exception("Unknown statistical entry type");
            }
        }
 
        @Override
        public String toString() {
            return Key + ": " + getValueString();
        }
 
        private boolean m_is_int = false;
        private boolean m_is_double = false;
        private int m_int = 0;
        private double m_double = 0.0;
 
        Entry(String k, int v)
        {
            Key = k;
            m_is_int = true;
            m_int = v;
        }
 
        Entry(String k, double v)
        {
            Key = k;
            m_is_double = true;
            m_double = v;
        }
    }
 
    @Override
    public String toString()
    {
        return Native.statsToString(getContext().nCtx(), getNativeObject());
    }
 
    public int size()
    {
        return Native.statsSize(getContext().nCtx(), getNativeObject());
    }
 
    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;
    }
 
    public String[] getKeys()
    {
        int n = size();
        String[] res = new String[n];
        for (int i = 0; i < n; i++)
            res[i] = Native.statsGetKey(getContext().nCtx(), getNativeObject(), i);
        return res;
    }
 
    public Entry get(String key)
    {
        int n = size();
        Entry[] es = getEntries();
        for (int i = 0; i < n; i++) {
            if (es[i].Key.equals(key)) {
                return es[i];
            }
        }
        return null;
    }
 
    Statistics(Context ctx, long obj)
    {
        super(ctx, obj);
    }
 
    @Override
    void incRef() {
        Native.statsIncRef(getContext().nCtx(), getNativeObject());
    }
 
    @Override
    void addToReferenceQueue() {
        getContext().getReferenceQueue().storeReference(this, StatisticsRef::new);
    }
 
    private static class StatisticsRef extends Z3ReferenceQueue.Reference<Statistics> {
 
        private StatisticsRef(Statistics referent, ReferenceQueue<Z3Object> q) {
            super(referent, q);
        }
 
        @Override
        void decRef(Context ctx, long z3Obj) {
            Native.statsDecRef(ctx.nCtx(), z3Obj);
        }
    }
}