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 }
com.microsoft.z3.Statistics.getEntries
Entry[] getEntries()
Definition: Statistics.java:133
com.microsoft.z3.Statistics.size
int size()
Definition: Statistics.java:123

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

## ◆ 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 }
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10693

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

116 {
117 return Native.statsToString(getContext().nCtx(), getNativeObject());
118 }