Z3
Data Structures | Public Member Functions
Statistics Class Reference
+ Inheritance diagram for Statistics:

Data Structures

class  Entry
 

Public Member Functions

String toString ()
 
int size ()
 
Entry[] getEntries ()
 
String[] getKeys ()
 
Entry get (String key)
 
- Public Member Functions inherited from Z3Object
void dispose ()
 
- Public Member Functions inherited from IDisposable
void dispose ()
 

Additional Inherited Members

- Protected Member Functions inherited from Z3Object
void finalize ()
 

Detailed Description

Objects of this class track statistical information about solvers.

Definition at line 23 of file Statistics.java.

Member Function Documentation

Entry get ( String  key)
inline

The value of a particular statistical counter. Remarks: Returns null if the key is unknown.

Exceptions
Z3Exception

Definition at line 185 of file Statistics.java.

186  {
187  int n = size();
188  Entry[] es = getEntries();
189  for (int i = 0; i < n; i++)
190  if (es[i].Key == key)
191  return es[i];
192  return null;
193  }
Entry [] getEntries ( )
inline

The data entries.

Exceptions
Z3Exception

Definition at line 144 of file Statistics.java.

Referenced by Statistics.get().

145  {
146 
147  int n = size();
148  Entry[] res = new Entry[n];
149  for (int i = 0; i < n; i++)
150  {
151  Entry e;
152  String k = Native.statsGetKey(getContext().nCtx(), getNativeObject(), i);
153  if (Native.statsIsUint(getContext().nCtx(), getNativeObject(), i))
154  e = new Entry(k, Native.statsGetUintValue(getContext().nCtx(),
155  getNativeObject(), i));
156  else if (Native.statsIsDouble(getContext().nCtx(), getNativeObject(), i))
157  e = new Entry(k, Native.statsGetDoubleValue(getContext().nCtx(),
158  getNativeObject(), i));
159  else
160  throw new Z3Exception("Unknown data entry value");
161  res[i] = e;
162  }
163  return res;
164  }
String [] getKeys ( )
inline

The statistical counters.

Definition at line 169 of file Statistics.java.

170  {
171  int n = size();
172  String[] res = new String[n];
173  for (int i = 0; i < n; i++)
174  res[i] = Native.statsGetKey(getContext().nCtx(), getNativeObject(), i);
175  return res;
176  }
int size ( )
inline

The number of statistical data.

Definition at line 134 of file Statistics.java.

Referenced by Statistics.get(), Statistics.getEntries(), and Statistics.getKeys().

135  {
136  return Native.statsSize(getContext().nCtx(), getNativeObject());
137  }
String toString ( )
inline

A string representation of the statistical data.

Definition at line 120 of file Statistics.java.

121  {
122  try
123  {
124  return Native.statsToString(getContext().nCtx(), getNativeObject());
125  } catch (Z3Exception e)
126  {
127  return "Z3Exception: " + e.getMessage();
128  }
129  }