Data Structures | |
class | Entry |
Public Member Functions | |
String | toString () |
int | size () throws Z3Exception |
Entry[] | getEntries () throws Z3Exception |
String[] | getKeys () throws Z3Exception |
Entry | get (String key) throws Z3Exception |
![]() | |
void | dispose () throws Z3Exception |
![]() | |
void | dispose () throws Z3Exception |
Additional Inherited Members | |
![]() | |
void | finalize () throws Z3Exception |
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.
Returns null if the key is unknown.
Z3Exception |
Definition at line 184 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.