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