Z3
Public Member Functions | Data Fields
Statistics.Entry Class Reference

Public Member Functions

int getUIntValue ()
 
double getDoubleValue ()
 
boolean isUInt ()
 
boolean isDouble ()
 
String getValueString ()
 
String toString ()
 

Data Fields

String Key
 

Detailed Description

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.

Member Function Documentation

double getDoubleValue ( )
inline

The double-value of the entry.

Definition at line 47 of file Statistics.java.

48  {
49  return m_double;
50  }
int getUIntValue ( )
inline

The uint-value of the entry.

Definition at line 39 of file Statistics.java.

40  {
41  return m_int;
42  }
String getValueString ( )
inline

The string representation of the the entry's value.

Exceptions
Z3Exception

Definition at line 73 of file Statistics.java.

Referenced by Statistics.Entry.toString().

74  {
75  if (isUInt())
76  return Integer.toString(m_int);
77  else if (isDouble())
78  return Double.toString(m_double);
79  else
80  throw new Z3Exception("Unknown statistical entry type");
81  }
boolean isUInt()
Definition: Statistics.java:55
boolean isDouble()
Definition: Statistics.java:63
boolean isDouble ( )
inline

True if the entry is double-valued.

Definition at line 63 of file Statistics.java.

Referenced by Statistics.Entry.getValueString().

64  {
65  return m_is_double;
66  }
boolean isUInt ( )
inline

True if the entry is uint-valued.

Definition at line 55 of file Statistics.java.

Referenced by Statistics.Entry.getValueString().

56  {
57  return m_is_int;
58  }
String toString ( )
inline

The string representation of the Entry.

Definition at line 86 of file Statistics.java.

87  {
88  try
89  {
90  return Key + ": " + getValueString();
91  } catch (Z3Exception e)
92  {
93  return new String("Z3Exception: " + e.getMessage());
94  }
95  }
String Key
Definition: Statistics.java:34
String getValueString()
Definition: Statistics.java:73

Field Documentation

String Key

The key of the entry.

Definition at line 34 of file Statistics.java.

Referenced by Statistics.get().