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

47 {
48 return m_double;
49 }

## ◆ getUIntValue()

int getUIntValue | ( |  | ) |
| inline

The uint-value of the entry.

Definition at line 38 of file Statistics.java.

39 {
40 return m_int;
41 }

## ◆ getValueString()

String getValueString | ( |  | ) |
| inline

The string representation of the entry's value.

Exceptions

  Z3Exception |

Definition at line 72 of file Statistics.java.

73 {
74 if (isUInt()) {
75 return Integer.toString(m_int);
76 } else if (isDouble()) {
77 return Double.toString(m_double);
78 } else {
79 throw new Z3Exception("Unknown statistical entry type");
80 }
81 }
com.microsoft.z3.Statistics.Entry.isDouble
boolean isDouble()
Definition: Statistics.java:62
com.microsoft.z3.Statistics.Entry.isUInt
boolean isUInt()
Definition: Statistics.java:54

Referenced by Statistics.Entry.toString().

## ◆ isDouble()

boolean isDouble | ( |  | ) |
| inline

True if the entry is double-valued.

Definition at line 62 of file Statistics.java.

63 {
64 return m_is_double;
65 }

Referenced by Statistics.Entry.getValueString().

## ◆ isUInt()

boolean isUInt | ( |  | ) |
| inline

True if the entry is uint-valued.

Definition at line 54 of file Statistics.java.

55 {
56 return m_is_int;
57 }

Referenced by Statistics.Entry.getValueString().

## ◆ toString()

String toString | ( |  | ) |
| inline

The string representation of the Entry.

Definition at line 87 of file Statistics.java.

87 {
88 return Key + ": " + getValueString();
89 }
com.microsoft.z3.Statistics.Entry.Key
String Key
Definition: Statistics.java:33
com.microsoft.z3.Statistics.Entry.getValueString
String getValueString()
Definition: Statistics.java:72

## Field Documentation

## ◆ Key

String Key

The key of the entry.

Definition at line 33 of file Statistics.java.

Referenced by Statistics.Entry.toString().