21using System.Diagnostics;
40 readonly
public string Key;
52 public bool IsUInt {
get {
return m_is_uint; } }
56 public bool IsDouble {
get {
return m_is_double; } }
67 return m_uint.ToString();
69 return m_double.ToString();
71 throw new Z3Exception(
"Unknown statistical entry type");
84 readonly
private bool m_is_uint =
false;
85 readonly
private bool m_is_double =
false;
86 readonly
private uint m_uint = 0;
87 readonly
private double m_double = 0.0;
88 internal Entry(
string k, uint v)
94 internal Entry(
string k,
double v)
108 return Native.Z3_stats_to_string(
Context.nCtx, NativeObject);
116 get {
return Native.Z3_stats_size(
Context.nCtx, NativeObject); }
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));
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);
171 for (uint i = 0; i < n; i++)
172 if (es[i].Key == key)
182 Debug.Assert(ctx !=
null);
185 internal class DecRefQueue : IDecRefQueue
187 public DecRefQueue() : base() { }
188 public DecRefQueue(uint move_limit) : base(move_limit) { }
189 internal override void IncRef(Context ctx, IntPtr obj)
191 Native.Z3_stats_inc_ref(ctx.nCtx, obj);
194 internal override void DecRef(Context ctx, IntPtr obj)
196 Native.Z3_stats_dec_ref(ctx.nCtx, obj);
200 internal override void IncRef(IntPtr o)
206 internal override void DecRef(IntPtr o)
The main interaction with Z3 happens via the Context.
IDecRefQueue Statistics_DRQ
Statistics DRQ
Statistical data is organized into pairs of [Key, Entry], where every Entry is either a DoubleEntry o...
double DoubleValue
The double-value of the entry.
readonly string Key
The key of the entry.
uint UIntValue
The uint-value of the entry.
bool IsDouble
True if the entry is double-valued.
bool IsUInt
True if the entry is uint-valued.
override string ToString()
The string representation of the Entry.
string Value
The string representation of the entry's value.
Objects of this class track statistical information about solvers.
string[] Keys
The statistical counters.
uint Size
The number of statistical data.
override string ToString()
A string representation of the statistical data.
Entry[] Entries
The data entries.
The exception base class for error reporting from Z3
Internal base class for interfacing with native Z3 objects. Should not be used externally.