Objects of this class track statistical information about solvers.
More...
|
class | DecRefQueue |
|
class | Entry |
| Statistical data is organized into pairs of [Key, Entry], where every Entry is either a DoubleEntry or a UIntEntry More...
|
|
Objects of this class track statistical information about solvers.
Definition at line 29 of file Statistics.cs.
◆ ToString()
override string ToString |
( |
| ) |
|
|
inline |
A string representation of the statistical data.
Definition at line 106 of file Statistics.cs.
108 return Native.Z3_stats_to_string(Context.nCtx, NativeObject);
◆ Entries
The data entries.
Definition at line 123 of file Statistics.cs.
128 Entry[] res =
new Entry[n];
129 for (uint i = 0; i < n; i++)
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));
138 throw new Z3Exception(
"Unknown data entry value");
◆ Keys
The statistical counters.
Definition at line 149 of file Statistics.cs.
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);
◆ Size
The number of statistical data.
Definition at line 115 of file Statistics.cs.
116 get {
return Native.Z3_stats_size(Context.nCtx, NativeObject); }
◆ this[string key]
The value of a particular statistical counter.
Returns null if the key is unknown.
Definition at line 166 of file Statistics.cs.
171 for (uint i = 0; i < n; i++)
172 if (es[i].Key == key)