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)
 

Additional Inherited Members

- Static Public Member Functions inherited from Z3Object
static long[] arrayToNative (Z3Object[] a)
 
static int arrayLength (Z3Object[] a)
 

Detailed Description

Objects of this class track statistical information about solvers.

Definition at line 25 of file Statistics.java.

Member Function Documentation

◆ get()

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 177 of file Statistics.java.

178  {
179  int n = size();
180  Entry[] es = getEntries();
181  for (int i = 0; i < n; i++) {
182  if (es[i].Key.equals(key)) {
183  return es[i];
184  }
185  }
186  return null;
187  }

Referenced by Goal.__getitem__(), and Goal.as_expr().

◆ getEntries()

Entry [] getEntries ( )
inline

The data entries.

Exceptions
Z3Exception

Definition at line 135 of file Statistics.java.

136  {
137 
138  int n = size();
139  Entry[] res = new Entry[n];
140  for (int i = 0; i < n; i++)
141  {
142  Entry e;
143  String k = Native.statsGetKey(getContext().nCtx(), getNativeObject(), i);
144  if (Native.statsIsUint(getContext().nCtx(), getNativeObject(), i)) {
145  e = new Entry(k, Native.statsGetUintValue(getContext().nCtx(),
146  getNativeObject(), i));
147  } else if (Native.statsIsDouble(getContext().nCtx(), getNativeObject(), i)) {
148  e = new Entry(k, Native.statsGetDoubleValue(getContext().nCtx(),
149  getNativeObject(), i));
150  } else {
151  throw new Z3Exception("Unknown data entry value");
152  }
153  res[i] = e;
154  }
155  return res;
156  }
def String(name, ctx=None)
Definition: z3py.py:11061

Referenced by Statistics.get().

◆ getKeys()

String [] getKeys ( )
inline

The statistical counters.

Definition at line 161 of file Statistics.java.

162  {
163  int n = size();
164  String[] res = new String[n];
165  for (int i = 0; i < n; i++)
166  res[i] = Native.statsGetKey(getContext().nCtx(), getNativeObject(), i);
167  return res;
168  }

◆ size()

int size ( )
inline

The number of statistical data.

Definition at line 125 of file Statistics.java.

126  {
127  return Native.statsSize(getContext().nCtx(), getNativeObject());
128  }

Referenced by ParamDescrsRef.__len__(), Goal.__len__(), BitVecNumRef.as_signed_long(), Statistics.get(), Statistics.getEntries(), Statistics.getKeys(), and BitVecSortRef.subsort().

◆ toString()

String toString ( )
inline

A string representation of the statistical data.

Definition at line 117 of file Statistics.java.

118  {
119  return Native.statsToString(getContext().nCtx(), getNativeObject());
120  }