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)
Public Member Functions inherited from Z3Object
void	dispose ()
Public Member Functions inherited from IDisposable
void	dispose ()

Additional Inherited Members
Protected Member Functions inherited from Z3Object
void	finalize ()

Detailed Description

Objects of this class track statistical information about solvers.

Definition at line 23 of file Statistics.java.

Member Function Documentation

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 185 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 ( )

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 ( )

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

int size ( )

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