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 28 of file Statistics.java.

Member Function Documentation

getDoubleValue()

double getDoubleValue ( )

inline

The double-value of the entry.

Definition at line 46 of file Statistics.java.

        {
            return m_double;
        }

getUIntValue()

int getUIntValue ( )

inline

The uint-value of the entry.

Definition at line 38 of file Statistics.java.

        {
            return m_int;
        }

getValueString()

String getValueString ( )

inline

The string representation of the entry's value.

Exceptions

Z3Exception

Definition at line 72 of file Statistics.java.

        {
            if (isUInt()) {
                return Integer.toString(m_int);
            } else if (isDouble()) {
                return Double.toString(m_double);
            } else {
                throw new Z3Exception("Unknown statistical entry type");
            }
        }

Referenced by Statistics.Entry.toString().

isDouble()

boolean isDouble ( )

inline

True if the entry is double-valued.

Definition at line 62 of file Statistics.java.

        {
            return m_is_double;
        }

Referenced by Statistics.Entry.getValueString().

isUInt()

boolean isUInt ( )

inline

True if the entry is uint-valued.

Definition at line 54 of file Statistics.java.

        {
            return m_is_int;
        }

Referenced by Statistics.Entry.getValueString().

toString()

String toString ( )

inline

The string representation of the Entry.

Definition at line 87 of file Statistics.java.

                                 {
            return Key + ": " + getValueString();
        }

Field Documentation

Key

String Key

The key of the entry.

Definition at line 33 of file Statistics.java.

Referenced by Statistics.Entry.toString().