Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Data Fields | Package Functions
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

Package Functions

 Entry (String k, int v)
 Entry (String k, double v)

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.


Constructor & Destructor Documentation

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

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.

Referenced by Statistics.Entry.Entry(), and Statistics.Entry.toString().

 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines