Data Structures | |
class | Entry |
Public Member Functions | |
String | toString () |
int | size () |
Entry[] | getEntries () |
String[] | getKeys () |
Entry | get (String key) |
![]() | |
void | dispose () |
![]() | |
void | dispose () |
Additional Inherited Members | |
![]() | |
void | finalize () |
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 185 of file Statistics.java.
|
inline |
The data entries.
Z3Exception |
Definition at line 144 of file Statistics.java.
Referenced by Statistics.get().
|
inline |
|
inline |
The number of statistical data.
Definition at line 134 of file Statistics.java.
Referenced by Statistics.get(), Statistics.getEntries(), and Statistics.getKeys().
|
inline |
A string representation of the statistical data.
Definition at line 120 of file Statistics.java.