Class Statistics

  • All Implemented Interfaces:
    java.lang.Iterable<java.util.Map.Entry<java.lang.String,​Stat>>

    public class Statistics
    extends java.lang.Object
    implements java.lang.Iterable<java.util.Map.Entry<java.lang.String,​Stat>>
    • Field Detail

      • pointer

        protected long pointer
    • Method Detail

      • deletePointer

        protected void deletePointer​(long pointer)
      • toString

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

        public Stat get​(java.lang.String name)
        Retrieve the statistic with the given name. Asserts that a statistic with the given name actually exists and throws a CVC5ApiRecoverableException if it does not.
        Parameters:
        name - Name of the statistic.
        Returns:
        The statistic with the given name.
      • iterator

        public Statistics.ConstIterator iterator()
        Specified by:
        iterator in interface java.lang.Iterable<java.util.Map.Entry<java.lang.String,​Stat>>
      • getPointer

        public long getPointer()
      • deletePointer

        public void deletePointer()
      • toString

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