Package io.github.cvc5

Class Stat

  • public class Stat
extends java.lang.Object
    Represents a snapshot of a single statistic value. A value can be of type long, double, String or a histogram (Map<String, Long>). The value type can be queried (using isInt(), isDouble(), etc.) and the stored value can be accessed (using getInt(), getDouble(), etc.). It is possible to query whether this statistic is an internal statistic by isInternal() and whether its value is the default value by isDefault().

    • Field Summary

      Fields 
      Modifier and Type Field Description
      protected long pointer  

    • Method Summary

      All Methods Instance Methods Concrete Methods 
      Modifier and Type Method Description
      void deletePointer()  
      protected void deletePointer​(long pointer)  
      double getDouble()
      Return the double value.
      java.util.Map<java.lang.String,​java.lang.Long> getHistogram()
      Return the histogram value.
      long getInt()
      Return the integer value.
      long getPointer()  
      java.lang.String getString()
      Return the string value.
      boolean isDefault()
      Does this value hold the default value?
      boolean isDouble()
      Is this value a double?
      boolean isHistogram()
      Is this value a histogram?
      boolean isInt()
      Is this value an integer?
      boolean isInternal()
      Is this value intended for internal use only?
      boolean isString()
      Is this value a string?
      java.lang.String toString()  
      protected java.lang.String toString​(long pointer)  

      • Methods inherited from class java.lang.Object

        clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

    • Field Detail

      • pointer

        protected long pointer

    • Method Detail

      • deletePointer

        protected void deletePointer​(long pointer)

      • getPointer

        public long getPointer()

      • toString

        protected java.lang.String toString​(long pointer)
        Returns:
        A string representation of this Stat.

      • isInternal

        public boolean isInternal()
        Is this value intended for internal use only?
        Returns:
        Whether this is an internal statistic.

      • isDefault

        public boolean isDefault()
        Does this value hold the default value?
        Returns:
        Whether this is a defaulted statistic.

      • isInt

        public boolean isInt()
        Is this value an integer?
        Returns:
        Whether the value is an integer.

      • getInt

        public long getInt()
        Return the integer value.
        Returns:
        The integer value.

      • isDouble

        public boolean isDouble()
        Is this value a double?
        Returns:
        Whether the value is a double.

      • getDouble

        public double getDouble()
        Return the double value.
        Returns:
        The double value.

      • isString

        public boolean isString()
        Is this value a string?
        Returns:
        Whether the value is a string.

      • getString

        public java.lang.String getString()
        Return the string value.
        Returns:
        The string value.

      • isHistogram

        public boolean isHistogram()
        Is this value a histogram?
        Returns:
        Whether the value is a histogram.

      • getHistogram

        public java.util.Map<java.lang.String,​java.lang.Long> getHistogram()
        Return the histogram value.
        Returns:
        The histogram value.

      • deletePointer

        public void deletePointer()

      • toString

        public java.lang.String toString()
        Overrides:
        toString in class java.lang.Object