21 using System.Diagnostics.Contracts;
28 [ContractVerification(
true)]
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)
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++)
156 Contract.Ensures(Contract.Result<
string[]>() != null);
159 string[] res =
new string[n];
160 for (uint i = 0; i < n; 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)
199 internal override void DecRef(
Context ctx, IntPtr obj)
205 internal override void IncRef(IntPtr o)
211 internal override void DecRef(IntPtr o)
static string Z3_stats_to_string(Z3_context a0, Z3_stats a1)
static double Z3_stats_get_double_value(Z3_context a0, Z3_stats a1, uint a2)
static int Z3_stats_is_double(Z3_context a0, Z3_stats a1, uint a2)
static string Z3_stats_get_key(Z3_context a0, Z3_stats a1, uint a2)
IDecRefQueue Statistics_DRQ
Statistics DRQ
static uint Z3_stats_size(Z3_context a0, Z3_stats a1)
Objects of this class track statistical information about solvers.
static void Z3_stats_dec_ref(Z3_context a0, Z3_stats a1)
static void Z3_stats_inc_ref(Z3_context a0, Z3_stats a1)
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
static int Z3_stats_is_uint(Z3_context a0, Z3_stats a1, uint a2)
Internal base class for interfacing with native Z3 objects. Should not be used externally.
static uint Z3_stats_get_uint_value(Z3_context a0, Z3_stats a1, uint a2)