Z3
Data Structures | Public Member Functions | Properties
Statistics Class Reference

Objects of this class track statistical information about solvers. More...

+ Inheritance diagram for Statistics:

Data Structures

class  DecRefQueue
 
class  Entry
 Statistical data is organized into pairs of [Key, Entry], where every Entry is either a DoubleEntry or a UIntEntry More...
 

Public Member Functions

override string ToString ()
 A string representation of the statistical data. More...
 
- Public Member Functions inherited from Z3Object
void Dispose ()
 Disposes of the underlying native Z3 object. More...
 

Properties

uint Size [get]
 The number of statistical data. More...
 
Entry [] Entries [get]
 The data entries. More...
 
string [] Keys [get]
 The statistical counters. More...
 
Entry this[string key] [get]
 The value of a particular statistical counter. More...
 

Detailed Description

Objects of this class track statistical information about solvers.

Definition at line 29 of file Statistics.cs.

Member Function Documentation

◆ ToString()

override string ToString ( )
inline

A string representation of the statistical data.

Definition at line 107 of file Statistics.cs.

108  {
109  return Native.Z3_stats_to_string(Context.nCtx, NativeObject);
110  }

Property Documentation

◆ Entries

Entry [] Entries
get

The data entries.

Definition at line 124 of file Statistics.cs.

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  }
uint Size
The number of statistical data.
Definition: Statistics.cs:116

◆ Keys

string [] Keys
get

The statistical counters.

Definition at line 153 of file Statistics.cs.

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  }
uint Size
The number of statistical data.
Definition: Statistics.cs:116

◆ Size

uint Size
get

The number of statistical data.

Definition at line 116 of file Statistics.cs.

116  {
117  get { return Native.Z3_stats_size(Context.nCtx, NativeObject); }
118  }

◆ this[string key]

Entry this[string key]
get

The value of a particular statistical counter.

Returns null if the key is unknown.

Definition at line 171 of file Statistics.cs.

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  }
Entry [] Entries
The data entries.
Definition: Statistics.cs:124
uint Size
The number of statistical data.
Definition: Statistics.cs:116