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) |
Objects of this class track statistical information about solvers.
Definition at line 23 of file Statistics.java.
|
inline |
The value of a particular statistical counter. Remarks: Returns null if the key is unknown.
Z3Exception |
Definition at line 175 of file Statistics.java.
Referenced by Goal.__getitem__(), and Goal.as_expr().
|
inline |
The data entries.
Z3Exception |
Definition at line 133 of file Statistics.java.
Referenced by Statistics.get().
|
inline |
The statistical counters.
Definition at line 159 of file Statistics.java.
|
inline |
The number of statistical data.
Definition at line 123 of file Statistics.java.
Referenced by ParamDescrsRef.__len__(), Goal.__len__(), BitVecNumRef.as_signed_long(), Statistics.get(), Statistics.getEntries(), Statistics.getKeys(), and BitVecSortRef.subsort().
|
inline |
A string representation of the statistical data.
Definition at line 115 of file Statistics.java.