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 }

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 }
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 }