Data Structures | |
class | Entry |
Public Member Functions | |
String | toString () |
int | size () |
Entry [] | getEntries () |
String [] | getKeys () |
Entry | get (String key) |
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.
|
inline |
The data entries.
Z3Exception |
Definition at line 133 of file Statistics.java.
Referenced by Statistics.get().
|
inline |
|
inline |
The number of statistical data.
Definition at line 123 of file Statistics.java.
Referenced by Statistics.get(), Statistics.getEntries(), and Statistics.getKeys().
|
inline |
A string representation of the statistical data.
Definition at line 115 of file Statistics.java.