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

Data Structures

class  Entry
 

Public Member Functions

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

Additional Inherited Members

- Protected Member Functions inherited from Z3Object
void finalize () throws Z3Exception
 

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) throws Z3Exception
inline

The value of a particular statistical counter.

Returns null if the key is unknown.

Exceptions
Z3Exception

Definition at line 184 of file Statistics.java.

185  {
186  int n = size();
187  Entry[] es = getEntries();
188  for (int i = 0; i < n; i++)
189  if (es[i].Key == key)
190  return es[i];
191  return null;
192  }
Entry [] getEntries ( ) throws Z3Exception
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 ( ) throws Z3Exception
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 ( ) throws Z3Exception
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  }