Z3
src/api/dotnet/Statistics.cs
Go to the documentation of this file.
00001 /*++
00002 Copyright (c) 2012 Microsoft Corporation
00003 
00004 Module Name:
00005 
00006     Statistics.cs
00007 
00008 Abstract:
00009 
00010     Z3 Managed API: Statistics
00011 
00012 Author:
00013 
00014     Christoph Wintersteiger (cwinter) 2012-03-22
00015 
00016 Notes:
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines