First refactoring of statistics classes (#6105)

This PR does a first round of refactoring on the statistics, in particular the Stat class and derived classes.
It significantly shrinks the class hierarchy, modernizes some code (e.g. use std::chrono instead of clock_gettime), removes unused features (e.g. nesting of statistics) and does some general cleanup and consolidation.

Subsequent PRs are planned to change the ownership model (right now every module owns the Stat object) which makes the whole register / unregister mechanism obsolete.

1 files changed, 278 insertions, 0 deletions

diff --git a/src/util/stats_base.h b/src/util/stats_base.h
new file mode 100644
index 000000000..c9ff2131f
--- /dev/null
+++ b/src/util/stats_base.h
@@ -0,0 +1,278 @@
+/*********************                                                        */
+/*! \file stats_base.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Gereon Kremer
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Base statistic classes
+ **
+ ** Base statistic classes
+ **/
+
+#include "cvc4_private_library.h"
+
+#ifndef CVC4__UTIL__STATS_BASE_H
+#define CVC4__UTIL__STATS_BASE_H
+
+#include <iomanip>
+#include <sstream>
+#include <string>
+
+#include "util/safe_print.h"
+#include "util/sexpr.h"
+#include "util/stats_utils.h"
+
+#ifdef CVC4_STATISTICS_ON
+#define CVC4_USE_STATISTICS true
+#else
+#define CVC4_USE_STATISTICS false
+#endif
+
+namespace CVC4 {
+
+/**
+ * The base class for all statistics.
+ *
+ * This base class keeps the name of the statistic and declares the (pure)
+ * virtual functions flushInformation() and safeFlushInformation().
+ * Derived classes must implement these function and pass their name to
+ * the base class constructor.
+ */
+class Stat
+{
+ public:
+  /**
+   * Construct a statistic with the given name.  Debug builds of CVC4
+   * will throw an assertion exception if the given name contains the
+   * statistic delimiter string.
+   */
+  Stat(const std::string& name);
+
+  /** Destruct a statistic.  This base-class version does nothing. */
+  virtual ~Stat() = default;
+
+  /**
+   * Flush the value of this statistic to an output stream.  Should
+   * finish the output with an end-of-line character.
+   */
+  virtual void flushInformation(std::ostream& out) const = 0;
+
+  /**
+   * Flush the value of this statistic to a file descriptor. Should finish the
+   * output with an end-of-line character. Should be safe to use in a signal
+   * handler.
+   */
+  virtual void safeFlushInformation(int fd) const = 0;
+
+  /** Get the name of this statistic. */
+  const std::string& getName() const { return d_name; }
+
+  /** Get the value of this statistic as a string. */
+  virtual SExpr getValue() const
+  {
+    std::stringstream ss;
+    flushInformation(ss);
+    return SExpr(ss.str());
+  }
+
+ protected:
+  /** The name of this statistic */
+  std::string d_name;
+}; /* class Stat */
+
+/**
+ * A data statistic that keeps a T and sets it with setData().
+ *
+ * Template class T must have an operator=() and a copy constructor.
+ */
+template <class T>
+class BackedStat : public Stat
+{
+ public:
+  /** Construct a backed statistic with the given name and initial value. */
+  BackedStat(const std::string& name, const T& init) : Stat(name), d_data(init)
+  {
+  }
+
+  /** Set the underlying data value to the given value. */
+  void set(const T& t)
+  {
+    if (CVC4_USE_STATISTICS)
+    {
+      d_data = t;
+    }
+  }
+
+  const T& get() const { return d_data; }
+
+  /** Flush the value of the statistic to the given output stream. */
+  virtual void flushInformation(std::ostream& out) const override
+  {
+    out << d_data;
+  }
+
+  virtual void safeFlushInformation(int fd) const override
+  {
+    safe_print<T>(fd, d_data);
+  }
+
+ protected:
+  /** The internally-kept statistic value */
+  T d_data;
+}; /* class BackedStat<T> */
+
+/**
+ * A data statistic that references a data cell of type T,
+ * implementing get() by referencing that memory cell, and
+ * setData() by reassigning the statistic to point to the new
+ * data cell.  The referenced data cell is kept as a const
+ * reference, meaning the referenced data is never actually
+ * modified by this class (it must be externally modified for
+ * a reference statistic to make sense).  A common use for
+ * this type of statistic is to output a statistic that is kept
+ * outside the statistics package (for example, one that's kept
+ * by a theory implementation for internal heuristic purposes,
+ * which is important to keep even if statistics are turned off).
+ *
+ * Template class T must have an assignment operator=().
+ */
+template <class T>
+class ReferenceStat : public Stat
+{
+ public:
+  /**
+   * Construct a reference stat with the given name and a reference
+   * to nullptr.
+   */
+  ReferenceStat(const std::string& name) : Stat(name) {}
+
+  /**
+   * Construct a reference stat with the given name and a reference to
+   * the given data.
+   */
+  ReferenceStat(const std::string& name, const T& data) : Stat(name)
+  {
+    set(data);
+  }
+
+  /** Set this reference statistic to refer to the given data cell. */
+  void set(const T& t)
+  {
+    if (CVC4_USE_STATISTICS)
+    {
+      d_data = &t;
+    }
+  }
+  const T& get() const { return *d_data; }
+
+  /** Flush the value of the statistic to the given output stream. */
+  virtual void flushInformation(std::ostream& out) const override
+  {
+    out << *d_data;
+  }
+
+  virtual void safeFlushInformation(int fd) const override
+  {
+    safe_print<T>(fd, *d_data);
+  }
+
+ private:
+  /** The referenced data cell */
+  const T* d_data = nullptr;
+}; /* class ReferenceStat<T> */
+
+/**
+ * A backed integer-valued (64-bit signed) statistic.
+ * This doesn't functionally differ from its base class BackedStat<int64_t>,
+ * except for adding convenience functions for dealing with integers.
+ */
+class IntStat : public BackedStat<int64_t>
+{
+ public:
+  /**
+   * Construct an integer-valued statistic with the given name and
+   * initial value.
+   */
+  IntStat(const std::string& name, int64_t init);
+
+  /** Increment the underlying integer statistic. */
+  IntStat& operator++();
+  /** Increment the underlying integer statistic. */
+  IntStat& operator++(int);
+
+  /** Increment the underlying integer statistic by the given amount. */
+  IntStat& operator+=(int64_t val);
+
+  /** Keep the maximum of the current statistic value and the given one. */
+  void maxAssign(int64_t val);
+
+  /** Keep the minimum of the current statistic value and the given one. */
+  void minAssign(int64_t val);
+
+  SExpr getValue() const override { return SExpr(Integer(d_data)); }
+
+}; /* class IntStat */
+
+/**
+ * The value for an AverageStat is the running average of (e1, e_2, ..., e_n),
+ *   (e1 + e_2 + ... + e_n)/n,
+ * where e_i is an entry added by an addEntry(e_i) call.
+ * The value is initially always 0.
+ * (This is to avoid making parsers confused.)
+ *
+ * A call to setData() will change the running average but not reset the
+ * running count, so should generally be avoided.  Call addEntry() to add
+ * an entry to the average calculation.
+ */
+class AverageStat : public BackedStat<double>
+{
+ public:
+  /** Construct an average statistic with the given name. */
+  AverageStat(const std::string& name);
+
+  /** Add an entry to the running-average calculation. */
+  AverageStat& operator<<(double e);
+
+  SExpr getValue() const override;
+
+ private:
+  /**
+   * The number of accumulations of the running average that we
+   * have seen so far.
+   */
+  uint32_t d_count = 0;
+  double d_sum = 0;
+}; /* class AverageStat */
+
+template <class T>
+class SizeStat : public Stat
+{
+ public:
+  SizeStat(const std::string& name, const T& sized) : Stat(name), d_sized(sized)
+  {
+  }
+  ~SizeStat() {}
+
+  /** Flush the value of the statistic to the given output stream. */
+  void flushInformation(std::ostream& out) const override
+  {
+    out << d_sized.size();
+  }
+
+  void safeFlushInformation(int fd) const override
+  {
+    safe_print(fd, d_sized.size());
+  }
+
+ private:
+  const T& d_sized;
+}; /* class SizeStat */
+
+}  // namespace CVC4
+
+#endif