Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Data Structures | Public Member Functions | Package Functions
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();
        }
    }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines