40 readonly
public string Key;
44 public uint UIntValue {
get {
return m_uint; } }
48 public double DoubleValue {
get {
return m_double; } }
52 public bool IsUInt {
get {
return m_is_uint; } }
56 public bool IsDouble {
get {
return m_is_double; } }
65 Contract.Ensures(Contract.Result<
string>() != null);
68 return m_uint.ToString();
70 return m_double.ToString();
72 throw new Z3Exception(
"Unknown statistical entry type");
81 return Key +
": " + Value;
85 readonly
private bool m_is_uint =
false;
86 readonly
private bool m_is_double =
false;
87 readonly
private uint m_uint = 0;
88 readonly
private double m_double = 0.0;
89 internal Entry(
string k, uint v)
95 internal Entry(
string k,
double v)
109 return Native.Z3_stats_to_string(
Context.nCtx, NativeObject);
117 get {
return Native.Z3_stats_size(
Context.nCtx, NativeObject); }
123 public Entry[] Entries
127 Contract.Ensures(Contract.Result<
Entry[]>() != null);
128 Contract.Ensures(Contract.Result<
Entry[]>().Length ==
this.Size);
129 Contract.Ensures(Contract.ForAll(0, Contract.Result<
Entry[]>().Length, j => Contract.Result<
Entry[]>()[j] != null));
133 for (uint i = 0; i < n; i++)
136 string k = Native.Z3_stats_get_key(
Context.nCtx, NativeObject, i);
137 if (Native.Z3_stats_is_uint(
Context.nCtx, NativeObject, i) != 0)
138 e =
new Entry(k, Native.Z3_stats_get_uint_value(
Context.nCtx, NativeObject, i));
139 else if (Native.Z3_stats_is_double(
Context.nCtx, NativeObject, i) != 0)
140 e =
new Entry(k, Native.Z3_stats_get_double_value(
Context.nCtx, NativeObject, i));
156 Contract.Ensures(Contract.Result<
string[]>() != null);
159 string[] res =
new string[n];
160 for (uint i = 0; i < n; i++)
161 res[i] = Native.Z3_stats_get_key(
Context.nCtx, NativeObject, i);
170 public Entry this[
string key]
175 Entry[] es = Entries;
176 for (uint i = 0; i < n; i++)
177 if (es[i].Key == key)
187 Contract.Requires(ctx != null);
192 public DecRefQueue() : base() { }
193 public DecRefQueue(uint move_limit) : base(move_limit) { }
194 internal override void IncRef(
Context ctx, IntPtr obj)
196 Native.Z3_stats_inc_ref(ctx.nCtx, obj);
199 internal override void DecRef(
Context ctx, IntPtr obj)
201 Native.Z3_stats_dec_ref(ctx.nCtx, obj);
205 internal override void IncRef(IntPtr o)
211 internal override void DecRef(IntPtr o)
IDecRefQueue Statistics_DRQ
Statistics DRQ
Objects of this class track statistical information about solvers.
Statistical data is organized into pairs of [Key, Entry], where every Entry is either a DoubleEntry o...
readonly string Key
The key of the entry.
override string ToString()
A string representation of the statistical data.
override string ToString()
The string representation of the Entry.
The main interaction with Z3 happens via the Context.
The exception base class for error reporting from Z3
Internal base class for interfacing with native Z3 objects. Should not be used externally.