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

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

◆ getEntries()

Entry [] getEntries ( )
inline

The data entries.

Exceptions
Z3Exception

Definition at line 133 of file Statistics.java.

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

Referenced by Statistics.get().

◆ getKeys()

String [] getKeys ( )
inline

The statistical counters.

Definition at line 159 of file Statistics.java.

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

◆ size()

int size ( )
inline

The number of statistical data.

Definition at line 123 of file Statistics.java.

124  {
125  return Native.statsSize(getContext().nCtx(), getNativeObject());
126  }

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

◆ toString()

String toString ( )
inline

A string representation of the statistical data.

Definition at line 115 of file Statistics.java.

116  {
117  return Native.statsToString(getContext().nCtx(), getNativeObject());
118  }
com.microsoft.z3.Statistics.size
int size()
Definition: Statistics.java:123
com.microsoft.z3.Statistics.getEntries
Entry[] getEntries()
Definition: Statistics.java:133
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10130