Statistics Class Reference

Inheritance diagram for Statistics:

Data Structures
class	Entry

Public Member Functions
String	toString ()
int	size ()
Entry[]	getEntries ()
String[]	getKeys ()
Entry	get (String key)

Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[]	arrayToNative (Z3Object[] a)
static int	arrayLength (Z3Object[] a)

Detailed Description

Objects of this class track statistical information about solvers.

Definition at line 25 of file Statistics.java.

Member Function Documentation

get()

Entry get ( String  key )

inline

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

Exceptions

Z3Exception

Definition at line 177 of file Statistics.java.

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

Referenced by Goal.__getitem__(), and Goal.as_expr().

getEntries()

Entry[] getEntries ( )

inline

The data entries.

Exceptions

Z3Exception

Definition at line 135 of file Statistics.java.

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

Referenced by Statistics.get().

getKeys()

String[] getKeys ( )

inline

The statistical counters.

Definition at line 161 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;
    }

size()

int size ( )

inline

The number of statistical data.

Definition at line 125 of file Statistics.java.

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

Referenced by ParamDescrsRef.__len__(), Goal.__len__(), BitVecNumRef.as_signed_long(), Statistics.get(), Statistics.getEntries(), Statistics.getKeys(), and BitVecSortRef.subsort().

toString()

String toString ( )

inline

A string representation of the statistical data.

Definition at line 117 of file Statistics.java.

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