Z3 |

Data Structures | Public Member Functions | Properties
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.

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

## Property Documentation

## ◆ Entries

Entry [] Entries
| get

The data entries.

Definition at line 122 of file Statistics.cs.

123 {
124 get
125 {
126
127 uint n = Size;
128 Entry[] res = new Entry[n];
129 for (uint i = 0; i < n; i++)
130 {
131 Entry e;
132 string k = Native.Z3_stats_get_key(Context.nCtx, NativeObject, i);
133 if (Native.Z3_stats_is_uint(Context.nCtx, NativeObject, i) != 0)
134 e = new Entry(k, Native.Z3_stats_get_uint_value(Context.nCtx, NativeObject, i));
135 else if (Native.Z3_stats_is_double(Context.nCtx, NativeObject, i) != 0)
136 e = new Entry(k, Native.Z3_stats_get_double_value(Context.nCtx, NativeObject, i));
137 else
138 throw new Z3Exception("Unknown data entry value");
139 res[i] = e;
140 }
141 return res;
142 }
143 }
Microsoft.Z3.Statistics.Size
uint Size
The number of statistical data.
Definition: Statistics.cs:115

## ◆ Keys

string [] Keys
| get

The statistical counters.

Definition at line 148 of file Statistics.cs.

149 {
150 get
151 {
152
153 uint n = Size;
154 string[] res = new string[n];
155 for (uint i = 0; i < n; i++)
156 res[i] = Native.Z3_stats_get_key(Context.nCtx, NativeObject, i);
157 return res;
158 }
159 }

## ◆ Size

uint Size
| get

The number of statistical data.

Definition at line 114 of file Statistics.cs.

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

## ◆ 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 165 of file Statistics.cs.

166 {
167 get
168 {
169 uint n = Size;
170 Entry[] es = Entries;
171 for (uint i = 0; i < n; i++)
172 if (es[i].Key == key)
173 return es[i];
174 return null;
175 }
176 }
Microsoft.Z3.Statistics.Entries
Entry[] Entries
The data entries.
Definition: Statistics.cs:123