Go to the documentation of this file.00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 using System;
00021 using System.Diagnostics.Contracts;
00022
00023 namespace Microsoft.Z3
00024 {
00028 [ContractVerification(true)]
00029 public class Statistics : Z3Object
00030 {
00035 public class Entry
00036 {
00040 readonly public string Key;
00044 public uint UIntValue { get { return m_uint; } }
00048 public double DoubleValue { get { return m_double; } }
00052 public bool IsUInt { get { return m_is_uint; } }
00056 public bool IsDouble { get { return m_is_double; } }
00057
00061 public string Value
00062 {
00063 get
00064 {
00065 Contract.Ensures(Contract.Result<string>() != null);
00066
00067 if (IsUInt)
00068 return m_uint.ToString();
00069 else if (IsDouble)
00070 return m_double.ToString();
00071 else
00072 throw new Z3Exception("Unknown statistical entry type");
00073 }
00074 }
00075
00079 public override string ToString()
00080 {
00081 return Key + ": " + Value;
00082 }
00083
00084 #region Internal
00085 readonly private bool m_is_uint = false;
00086 readonly private bool m_is_double = false;
00087 readonly private uint m_uint = 0;
00088 readonly private double m_double = 0.0;
00089 internal Entry(string k, uint v)
00090 {
00091 Key = k;
00092 m_is_uint = true;
00093 m_uint = v;
00094 }
00095 internal Entry(string k, double v)
00096 {
00097 Key = k;
00098 m_is_double = true;
00099 m_double = v;
00100 }
00101 #endregion
00102 }
00103
00107 public override string ToString()
00108 {
00109 return Native.Z3_stats_to_string(Context.nCtx, NativeObject);
00110 }
00111
00115 public uint Size
00116 {
00117 get { return Native.Z3_stats_size(Context.nCtx, NativeObject); }
00118 }
00119
00123 public Entry[] Entries
00124 {
00125 get
00126 {
00127 Contract.Ensures(Contract.Result<Entry[]>() != null);
00128 Contract.Ensures(Contract.Result<Entry[]>().Length == this.Size);
00129 Contract.Ensures(Contract.ForAll(0, Contract.Result<Entry[]>().Length, j => Contract.Result<Entry[]>()[j] != null));
00130
00131 uint n = Size;
00132 Entry[] res = new Entry[n];
00133 for (uint i = 0; i < n; i++)
00134 {
00135 Entry e;
00136 string k = Native.Z3_stats_get_key(Context.nCtx, NativeObject, i);
00137 if (Native.Z3_stats_is_uint(Context.nCtx, NativeObject, i) != 0)
00138 e = new Entry(k, Native.Z3_stats_get_uint_value(Context.nCtx, NativeObject, i));
00139 else if (Native.Z3_stats_is_double(Context.nCtx, NativeObject, i) != 0)
00140 e = new Entry(k, Native.Z3_stats_get_double_value(Context.nCtx, NativeObject, i));
00141 else
00142 throw new Z3Exception("Unknown data entry value");
00143 res[i] = e;
00144 }
00145 return res;
00146 }
00147 }
00148
00152 public string[] Keys
00153 {
00154 get
00155 {
00156 Contract.Ensures(Contract.Result<string[]>() != null);
00157
00158 uint n = Size;
00159 string[] res = new string[n];
00160 for (uint i = 0; i < n; i++)
00161 res[i] = Native.Z3_stats_get_key(Context.nCtx, NativeObject, i);
00162 return res;
00163 }
00164 }
00165
00170 public Entry this[string key]
00171 {
00172 get
00173 {
00174 uint n = Size;
00175 Entry[] es = Entries;
00176 for (uint i = 0; i < n; i++)
00177 if (es[i].Key == key)
00178 return es[i];
00179 return null;
00180 }
00181 }
00182
00183 #region Internal
00184 internal Statistics(Context ctx, IntPtr obj)
00185 : base(ctx, obj)
00186 {
00187 Contract.Requires(ctx != null);
00188 }
00189
00190 internal class DecRefQueue : IDecRefQueue
00191 {
00192 public override void IncRef(Context ctx, IntPtr obj)
00193 {
00194 Native.Z3_stats_inc_ref(ctx.nCtx, obj);
00195 }
00196
00197 public override void DecRef(Context ctx, IntPtr obj)
00198 {
00199 Native.Z3_stats_dec_ref(ctx.nCtx, obj);
00200 }
00201 };
00202
00203 internal override void IncRef(IntPtr o)
00204 {
00205 Context.Statistics_DRQ.IncAndClear(Context, o);
00206 base.IncRef(o);
00207 }
00208
00209 internal override void DecRef(IntPtr o)
00210 {
00211 Context.Statistics_DRQ.Add(o);
00212 base.DecRef(o);
00213 }
00214 #endregion
00215 }
00216 }