Z3
Statistics.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  Statistics.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Statistics
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-03-22
15 
16 Notes:
17 
18 --*/
19 
20 using System;
21 using System.Diagnostics.Contracts;
22 
23 namespace Microsoft.Z3
24 {
28  [ContractVerification(true)]
29  public class Statistics : Z3Object
30  {
35  public class Entry
36  {
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; } }
57 
61  public string Value
62  {
63  get
64  {
65  Contract.Ensures(Contract.Result<string>() != null);
66 
67  if (IsUInt)
68  return m_uint.ToString();
69  else if (IsDouble)
70  return m_double.ToString();
71  else
72  throw new Z3Exception("Unknown statistical entry type");
73  }
74  }
75 
79  public override string ToString()
80  {
81  return Key + ": " + Value;
82  }
83 
84  #region Internal
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)
90  {
91  Key = k;
92  m_is_uint = true;
93  m_uint = v;
94  }
95  internal Entry(string k, double v)
96  {
97  Key = k;
98  m_is_double = true;
99  m_double = v;
100  }
101  #endregion
102  }
103 
107  public override string ToString()
108  {
109  return Native.Z3_stats_to_string(Context.nCtx, NativeObject);
110  }
111 
115  public uint Size
116  {
117  get { return Native.Z3_stats_size(Context.nCtx, NativeObject); }
118  }
119 
123  public Entry[] Entries
124  {
125  get
126  {
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));
130 
131  uint n = Size;
132  Entry[] res = new Entry[n];
133  for (uint i = 0; i < n; i++)
134  {
135  Entry e;
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));
141  else
142  throw new Z3Exception("Unknown data entry value");
143  res[i] = e;
144  }
145  return res;
146  }
147  }
148 
152  public string[] Keys
153  {
154  get
155  {
156  Contract.Ensures(Contract.Result<string[]>() != null);
157 
158  uint n = Size;
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);
162  return res;
163  }
164  }
165 
170  public Entry this[string key]
171  {
172  get
173  {
174  uint n = Size;
175  Entry[] es = Entries;
176  for (uint i = 0; i < n; i++)
177  if (es[i].Key == key)
178  return es[i];
179  return null;
180  }
181  }
182 
183  #region Internal
184  internal Statistics(Context ctx, IntPtr obj)
185  : base(ctx, obj)
186  {
187  Contract.Requires(ctx != null);
188  }
189 
190  internal class DecRefQueue : IDecRefQueue
191  {
192  public DecRefQueue() : base() { }
193  public DecRefQueue(uint move_limit) : base(move_limit) { }
194  internal override void IncRef(Context ctx, IntPtr obj)
195  {
196  Native.Z3_stats_inc_ref(ctx.nCtx, obj);
197  }
198 
199  internal override void DecRef(Context ctx, IntPtr obj)
200  {
201  Native.Z3_stats_dec_ref(ctx.nCtx, obj);
202  }
203  };
204 
205  internal override void IncRef(IntPtr o)
206  {
207  Context.Statistics_DRQ.IncAndClear(Context, o);
208  base.IncRef(o);
209  }
210 
211  internal override void DecRef(IntPtr o)
212  {
213  Context.Statistics_DRQ.Add(o);
214  base.DecRef(o);
215  }
216  #endregion
217  }
218 }
static string Z3_stats_to_string(Z3_context a0, Z3_stats a1)
Definition: Native.cs:5493
static double Z3_stats_get_double_value(Z3_context a0, Z3_stats a1, uint a2)
Definition: Native.cs:5555
using System
static int Z3_stats_is_double(Z3_context a0, Z3_stats a1, uint a2)
Definition: Native.cs:5539
static string Z3_stats_get_key(Z3_context a0, Z3_stats a1, uint a2)
Definition: Native.cs:5523
IDecRefQueue Statistics_DRQ
Statistics DRQ
Definition: Context.cs:4524
static uint Z3_stats_size(Z3_context a0, Z3_stats a1)
Definition: Native.cs:5515
Objects of this class track statistical information about solvers.
Definition: Statistics.cs:29
static void Z3_stats_dec_ref(Z3_context a0, Z3_stats a1)
Definition: Native.cs:5508
static void Z3_stats_inc_ref(Z3_context a0, Z3_stats a1)
Definition: Native.cs:5501
Statistical data is organized into pairs of [Key, Entry], where every Entry is either a DoubleEntry o...
Definition: Statistics.cs:35
readonly string Key
The key of the entry.
Definition: Statistics.cs:40
override string ToString()
A string representation of the statistical data.
Definition: Statistics.cs:107
override string ToString()
The string representation of the Entry.
Definition: Statistics.cs:79
DecRefQueue interface
Definition: IDecRefQueue.cs:32
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:27
static int Z3_stats_is_uint(Z3_context a0, Z3_stats a1, uint a2)
Definition: Native.cs:5531
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:31
static uint Z3_stats_get_uint_value(Z3_context a0, Z3_stats a1, uint a2)
Definition: Native.cs:5547