Statistics Class Reference

Objects of this class track statistical information about solvers. More...

Inheritance diagram for Statistics:

Data Structures
class	DecRefQueue
class	Entry
	Statistical data is organized into pairs of [Key, Entry], where every Entry is either a DoubleEntry or a UIntEntry More...

Public Member Functions
override string	ToString ()
	A string representation of the statistical data. More...
Public Member Functions inherited from Z3Object
void	Dispose ()
	Disposes of the underlying native Z3 object. More...

Properties
uint	Size [get]
	The number of statistical data. More...
Entry[]	Entries [get]
	The data entries. More...
string[]	Keys [get]
	The statistical counters. More...
Entry	this[string key] [get]
	The value of a particular statistical counter. More...

Detailed Description

Objects of this class track statistical information about solvers.

Definition at line 29 of file Statistics.cs.

Member Function Documentation

ToString()

override string ToString ( )

inline

A string representation of the statistical data.

Definition at line 106 of file Statistics.cs.

        {
            return Native.Z3_stats_to_string(Context.nCtx, NativeObject);
        }

Property Documentation

Entries

Entry [] Entries

get

The data entries.

Definition at line 123 of file Statistics.cs.

        {
            get
            {
 
                uint n = Size;
                Entry[] res = new Entry[n];
                for (uint i = 0; i < n; i++)
                {
                    Entry e;
                    string k = Native.Z3_stats_get_key(Context.nCtx, NativeObject, i);
                    if (Native.Z3_stats_is_uint(Context.nCtx, NativeObject, i) != 0)
                        e = new Entry(k, Native.Z3_stats_get_uint_value(Context.nCtx, NativeObject, i));
                    else if (Native.Z3_stats_is_double(Context.nCtx, NativeObject, i) != 0)
                        e = new Entry(k, Native.Z3_stats_get_double_value(Context.nCtx, NativeObject, i));
                    else
                        throw new Z3Exception("Unknown data entry value");
                    res[i] = e;
                }
                return res;
            }
        }

Keys

string [] Keys

get

The statistical counters.

Definition at line 149 of file Statistics.cs.

        {
            get
            {
 
                uint n = Size;
                string[] res = new string[n];
                for (uint i = 0; i < n; i++)
                    res[i] = Native.Z3_stats_get_key(Context.nCtx, NativeObject, i);
                return res;
            }
        }

Size

uint Size

get

The number of statistical data.

Definition at line 115 of file Statistics.cs.

        {
            get { return Native.Z3_stats_size(Context.nCtx, NativeObject); }
        }

this[string key]

Entry this[string key]

get

The value of a particular statistical counter.

Returns null if the key is unknown.

Definition at line 166 of file Statistics.cs.

        {
            get
            {
                uint n = Size;
                Entry[] es = Entries;
                for (uint i = 0; i < n; i++)
                    if (es[i].Key == key)
                        return es[i];
                return null;
            }
        }