Statistics Class Reference

Inheritance diagram for Statistics:

Data Structures
class	Entry
Public Member Functions
String	toString ()
int	size () throws Z3Exception
Entry[]	getEntries () throws Z3Exception
String[]	getKeys () throws Z3Exception
Entry	get (String key) throws Z3Exception
Package Functions
	Statistics (Context ctx, long obj) throws Z3Exception
void	incRef (long o) throws Z3Exception
void	decRef (long o) throws Z3Exception

---

Detailed Description

Objects of this class track statistical information about solvers.

Definition at line 23 of file Statistics.java.

---

Constructor & Destructor Documentation

Statistics	(	Context	ctx,
		long	obj
	)		throws Z3Exception [inline, package]

Definition at line 194 of file Statistics.java.

    {
        super(ctx, obj);
    }

---

Member Function Documentation

void decRef

(

long

o

)

throws Z3Exception [inline, package]

Reimplemented from Z3Object.

Definition at line 205 of file Statistics.java.

    {
        getContext().statistics_DRQ().add(o);
        super.decRef(o);
    }

Entry get

(

String

key

)

throws Z3Exception [inline]

The value of a particular statistical counter. Returns null if the key is unknown.

Exceptions:

Z3Exception

Definition at line 184 of file Statistics.java.

    {
        int n = size();
        Entry[] es = getEntries();
        for (int i = 0; i < n; i++)
            if (es[i].Key == key)
                return es[i];
        return null;
    }

Entry [] getEntries

(

)

throws Z3Exception [inline]

The data entries.

Exceptions:

Z3Exception

Definition at line 144 of file Statistics.java.

Referenced by Statistics.get().

    {

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

String [] getKeys

(

)

throws Z3Exception [inline]

The statistical counters.

Definition at line 169 of file Statistics.java.

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

void incRef

(

long

o

)

throws Z3Exception [inline, package]

Reimplemented from Z3Object.

Definition at line 199 of file Statistics.java.

    {
        getContext().statistics_DRQ().incAndClear(getContext(), o);
        super.incRef(o);
    }

int size

(

)

throws Z3Exception [inline]

The number of statistical data.

Definition at line 134 of file Statistics.java.

Referenced by Statistics.get(), Statistics.getEntries(), and Statistics.getKeys().

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

String toString

(

)

[inline]

A string representation of the statistical data.

Definition at line 120 of file Statistics.java.

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