Public Member Functions | |
int | getUIntValue () |
double | getDoubleValue () |
boolean | isUInt () |
boolean | isDouble () |
String | getValueString () throws Z3Exception |
String | toString () |
Data Fields | |
String | Key |
Package Functions | |
Entry (String k, int v) | |
Entry (String k, double v) |
Statistical data is organized into pairs of [Key, Entry], where every Entry is either a DoubleEntry
or a UIntEntry
Definition at line 29 of file Statistics.java.
Entry | ( | String | k, |
int | v | ||
) | [inline, package] |
Definition at line 102 of file Statistics.java.
{ Key = k; m_is_int = true; m_int = v; }
Entry | ( | String | k, |
double | v | ||
) | [inline, package] |
Definition at line 109 of file Statistics.java.
{ Key = k; m_is_double = true; m_double = v; }
double getDoubleValue | ( | ) | [inline] |
int getUIntValue | ( | ) | [inline] |
String getValueString | ( | ) | throws Z3Exception [inline] |
The string representation of the the entry's value.
Z3Exception |
Definition at line 73 of file Statistics.java.
Referenced by Statistics.Entry.toString().
boolean isDouble | ( | ) | [inline] |
True if the entry is double-valued.
Definition at line 63 of file Statistics.java.
Referenced by Statistics.Entry.getValueString().
{
return m_is_double;
}
boolean isUInt | ( | ) | [inline] |
True if the entry is uint-valued.
Definition at line 55 of file Statistics.java.
Referenced by Statistics.Entry.getValueString().
{
return m_is_int;
}
String toString | ( | ) | [inline] |
The string representation of the Entry.
Definition at line 86 of file Statistics.java.
{ try { return Key + ": " + getValueString(); } catch (Z3Exception e) { return new String("Z3Exception: " + e.getMessage()); } }
String Key |
The key of the entry.
Definition at line 34 of file Statistics.java.
Referenced by Statistics.Entry.Entry(), and Statistics.Entry.toString().