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

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

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

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