Statistics.Entry

java.lang.Object

com.microsoft.z3.Statistics.Entry

Enclosing class:: Statistics

public class Statistics.Entry extends Object

Statistical data is organized into pairs of [Key, Entry], where every Entry is either a DoubleEntry or a UIntEntry

Field Summary

Fields

Modifier and Type

Field

Description

String

Key

The key of the entry.
Method Summary

Modifier and Type

Method

Description

double

getDoubleValue()

The double-value of the entry.

int

getUIntValue()

The uint-value of the entry.

String

getValueString()

The string representation of the entry's value.

boolean

isDouble()

True if the entry is double-valued.

boolean

isUInt()

True if the entry is uint-valued.

String

toString()

The string representation of the Entry.

Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Field Details
- Key
  
  public String Key
  
  The key of the entry.
Method Details
- getUIntValue
  
  public int getUIntValue()
  
  The uint-value of the entry.
- getDoubleValue
  
  public double getDoubleValue()
  
  The double-value of the entry.
- isUInt
  
  public boolean isUInt()
  
  True if the entry is uint-valued.
- isDouble
  
  public boolean isDouble()
  
  True if the entry is double-valued.
- getValueString
  
  public String getValueString()
  
  The string representation of the entry's value.
  
  Throws:
  
  Z3Exception
- toString
  
  public String toString()
  
  The string representation of the Entry.
  
  Overrides:
  
  toString in class Object