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;
22
23
24 namespace Microsoft.Z3
25{
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
66 if (IsUInt)
67 return m_uint.ToString();
68 else if (IsDouble)
69 return m_double.ToString();
70 else
71 throw new Z3Exception("Unknown statistical entry type");
72 }
73 }
74
78 public override string ToString()
79 {
80 return Key + ": " + Value;
81 }
82
83 #region Internal
84 readonly private bool m_is_uint = false;
85 readonly private bool m_is_double = false;
86 readonly private uint m_uint = 0;
87 readonly private double m_double = 0.0;
88 internal Entry(string k, uint v)
89 {
90 Key = k;
91 m_is_uint = true;
92 m_uint = v;
93 }
94 internal Entry(string k, double v)
95 {
96 Key = k;
97 m_is_double = true;
98 m_double = v;
99 }
100 #endregion
101 }
102
106 public override string ToString()
107 {
108 return Native.Z3_stats_to_string(Context.nCtx, NativeObject);
109 }
110
114 public uint Size
115 {
116 get { return Native.Z3_stats_size(Context.nCtx, NativeObject); }
117 }
118
122 public Entry[] Entries
123 {
124 get
125 {
126
127 uint n = Size;
128 Entry[] res = new Entry[n];
129 for (uint i = 0; i < n; i++)
130 {
131 Entry e;
132 string k = Native.Z3_stats_get_key(Context.nCtx, NativeObject, i);
133 if (Native.Z3_stats_is_uint(Context.nCtx, NativeObject, i) != 0)
134 e = new Entry(k, Native.Z3_stats_get_uint_value(Context.nCtx, NativeObject, i));
135 else if (Native.Z3_stats_is_double(Context.nCtx, NativeObject, i) != 0)
136 e = new Entry(k, Native.Z3_stats_get_double_value(Context.nCtx, NativeObject, i));
137 else
138 throw new Z3Exception("Unknown data entry value");
139 res[i] = e;
140 }
141 return res;
142 }
143 }
144
148 public string[] Keys
149 {
150 get
151 {
152
153 uint n = Size;
154 string[] res = new string[n];
155 for (uint i = 0; i < n; i++)
156 res[i] = Native.Z3_stats_get_key(Context.nCtx, NativeObject, i);
157 return res;
158 }
159 }
160
165 public Entry this[string key]
166 {
167 get
168 {
169 uint n = Size;
170 Entry[] es = Entries;
171 for (uint i = 0; i < n; i++)
172 if (es[i].Key == key)
173 return es[i];
174 return null;
175 }
176 }
177
178 #region Internal
179 internal Statistics(Context ctx, IntPtr obj)
180 : base(ctx, obj)
181 {
182 Debug.Assert(ctx != null);
183 }
184
185 internal class DecRefQueue : IDecRefQueue
186 {
187 public DecRefQueue() : base() { }
188 public DecRefQueue(uint move_limit) : base(move_limit) { }
189 internal override void IncRef(Context ctx, IntPtr obj)
190 {
191 Native.Z3_stats_inc_ref(ctx.nCtx, obj);
192 }
193
194 internal override void DecRef(Context ctx, IntPtr obj)
195 {
196 Native.Z3_stats_dec_ref(ctx.nCtx, obj);
197 }
198 };
199
200 internal override void IncRef(IntPtr o)
201 {
202 Context.Statistics_DRQ.IncAndClear(Context, o);
203 base.IncRef(o);
204 }
205
206 internal override void DecRef(IntPtr o)
207 {
208 Context.Statistics_DRQ.Add(o);
209 base.DecRef(o);
210 }
211 #endregion
212 }
213}
Microsoft.Z3.Context
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Microsoft.Z3.Context.Statistics_DRQ
IDecRefQueue Statistics_DRQ
Statistics DRQ
Definition: Context.cs:4785
Microsoft.Z3.Statistics.Entry
Statistical data is organized into pairs of [Key, Entry], where every Entry is either a DoubleEntry o...
Definition: Statistics.cs:36
Microsoft.Z3.Statistics.Entry.DoubleValue
double DoubleValue
The double-value of the entry.
Definition: Statistics.cs:48
Microsoft.Z3.Statistics.Entry.Key
readonly string Key
The key of the entry.
Definition: Statistics.cs:40
Microsoft.Z3.Statistics.Entry.UIntValue
uint UIntValue
The uint-value of the entry.
Definition: Statistics.cs:44
Microsoft.Z3.Statistics.Entry.IsDouble
bool IsDouble
True if the entry is double-valued.
Definition: Statistics.cs:56
Microsoft.Z3.Statistics.Entry.IsUInt
bool IsUInt
True if the entry is uint-valued.
Definition: Statistics.cs:52
Microsoft.Z3.Statistics.Entry.ToString
override string ToString()
The string representation of the Entry.
Definition: Statistics.cs:78
Microsoft.Z3.Statistics.Entry.Value
string Value
The string representation of the entry's value.
Definition: Statistics.cs:62
Microsoft.Z3.Statistics
Objects of this class track statistical information about solvers.
Definition: Statistics.cs:30
Microsoft.Z3.Statistics.Keys
string[] Keys
The statistical counters.
Definition: Statistics.cs:149
Microsoft.Z3.Statistics.Size
uint Size
The number of statistical data.
Definition: Statistics.cs:115
Microsoft.Z3.Statistics.ToString
override string ToString()
A string representation of the statistical data.
Definition: Statistics.cs:106
Microsoft.Z3.Statistics.Entries
Entry[] Entries
The data entries.
Definition: Statistics.cs:123
Microsoft.Z3.Z3Exception
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:32
Microsoft.Z3.Z3Object
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33
Microsoft.Z3
Definition: AlgebraicNum.cs:27