Statistics.Entry Class Reference

Public Member Functions
int	getUIntValue ()
double	getDoubleValue ()
boolean	isUInt ()
boolean	isDouble ()
String	getValueString () throws Z3Exception
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.

        {
            return m_double;
        }

int getUIntValue ( )

inline

The uint-value of the entry.

Definition at line 39 of file Statistics.java.

        {
            return m_int;
        }

String getValueString ( ) throws Z3Exception

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().

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

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());
            }
        }

Field Documentation

String Key

The key of the entry.

Definition at line 34 of file Statistics.java.