Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Gereon Kremer, Matthew Sotoudeh, Mathias Preiner
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
       8                 :            :  * in the top-level source directory and their institutional affiliations.
       9                 :            :  * All rights reserved.  See the file COPYING in the top-level source
      10                 :            :  * directory for licensing information.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * Statistic proxy objects
      14                 :            :  *
      15                 :            :  * Conceptually, every statistic consists of a data object and a proxy
      16                 :            :  * object. The proxy objects are issued by the `StatisticsRegistry` and
      17                 :            :  * maintained by the user. They only hold a pointer to a matching data
      18                 :            :  * object. The purpose of proxy objects is to implement methods to easily
      19                 :            :  * change the statistic data, but shield the regular user from the internals.
      20                 :            :  */
      21                 :            : 
      22                 :            : #include "cvc5_private_library.h"
      23                 :            : 
      24                 :            : #ifndef CVC5__UTIL__STATISTICS_STATS_H
      25                 :            : #define CVC5__UTIL__STATISTICS_STATS_H
      26                 :            : 
      27                 :            : #include <optional>
      28                 :            : 
      29                 :            : #include "base/configuration.h"
      30                 :            : 
      31                 :            : namespace cvc5::internal {
      32                 :            : 
      33                 :            : // forward declare all values to avoid inclusion
      34                 :            : struct StatisticAverageValue;
      35                 :            : template <typename T>
      36                 :            : struct StatisticBackedValue;
      37                 :            : template <typename T>
      38                 :            : struct StatisticHistogramValue;
      39                 :            : template <typename T>
      40                 :            : struct StatisticReferenceValue;
      41                 :            : template <typename T>
      42                 :            : struct StatisticSizeValue;
      43                 :            : struct StatisticTimerValue;
      44                 :            : 
      45                 :            : class StatisticsRegistry;
      46                 :            : 
      47                 :            : /**
      48                 :            :  * Collects the average of a series of double values.
      49                 :            :  * New values are added by
      50                 :            :  *   AverageStat stat;
      51                 :            :  *   stat << 1.0 << 2.0;
      52                 :            :  */
      53                 :            : class AverageStat
      54                 :            : {
      55                 :            :  public:
      56                 :            :   /** Allow access to private constructor */
      57                 :            :   friend class StatisticsRegistry;
      58                 :            :   /** Value stored for this statistic */
      59                 :            :   using stat_type = StatisticAverageValue;
      60                 :            :   /** Add the value `v` to the running average */
      61                 :            :   AverageStat& operator<<(double v);
      62                 :            : 
      63                 :            :  private:
      64                 :            :   /** Construct from a pointer to the internal data */
      65                 :     200799 :   AverageStat(stat_type* data) : d_data(data) {}
      66                 :            :   /** The actual data that lives in the registry */
      67                 :            :   stat_type* d_data;
      68                 :            : };
      69                 :            : 
      70                 :            : /**
      71                 :            :  * Collects a histogram over some type.
      72                 :            :  * The type needs to be (convertible to) integral and support streaming to
      73                 :            :  * an `std::ostream`.
      74                 :            :  * New values are added by
      75                 :            :  *    HistogramStat<Kind> stat;
      76                 :            :  *    stat << Kind::ADD << Kind::AND;
      77                 :            :  */
      78                 :            : template <typename Integral>
      79                 :            : class HistogramStat
      80                 :            : {
      81                 :            :  public:
      82                 :            :   /** Allow access to private constructor */
      83                 :            :   friend class StatisticsRegistry;
      84                 :            :   /** Value stored for this statistic */
      85                 :            :   using stat_type = StatisticHistogramValue<Integral>;
      86                 :            :   /** Add the value `val` to the histogram */
      87                 :  161271235 :   HistogramStat& operator<<(Integral val)
      88                 :            :   {
      89                 :            :     if constexpr (configuration::isStatisticsBuild())
      90                 :            :     {
      91                 :  161271235 :       d_data->add(val);
      92                 :            :     }
      93                 :  161271235 :     return *this;
      94                 :            :   }
      95                 :            :   /** Get the current value for key `val` */
      96                 :          0 :   uint64_t getValue(Integral val) { return d_data->getValue(val); }
      97                 :            : 
      98                 :            :  private:
      99                 :            :   /** Construct from a pointer to the internal data */
     100                 :    9901823 :   HistogramStat(stat_type* data) : d_data(data) {}
     101                 :            :   /** The actual data that lives in the registry */
     102                 :            :   stat_type* d_data;
     103                 :            : };
     104                 :            : 
     105                 :            : /**
     106                 :            :  * Stores the reference to some value that exists outside of this statistic.
     107                 :            :  * Despite being called `ReferenceStat`, the reference is held as a pointer
     108                 :            :  * and can thus be reset using `set`.
     109                 :            :  * Note that the referenced object must have a lifetime that is longer than
     110                 :            :  * the lifetime of the `ReferenceStat` object. Upon destruction of the
     111                 :            :  * `ReferenceStat` the current value of the referenced object is copied into
     112                 :            :  * the `StatisticsRegistry`.
     113                 :            :  *
     114                 :            :  * To convert to the API representation in `cvc5::Stat`, `T` can only be one
     115                 :            :  * of the types accepted by the `cvc5::Stat` constructors (or be implicitly
     116                 :            :  * converted to one of them).
     117                 :            :  */
     118                 :            : template <typename T>
     119                 :            : class ReferenceStat
     120                 :            : {
     121                 :            :  public:
     122                 :            :   /** Allow access to private constructor */
     123                 :            :   friend class StatisticsRegistry;
     124                 :            :   /** Value stored for this statistic */
     125                 :            :   using stat_type = StatisticReferenceValue<T>;
     126                 :            :   /** Reset the reference to point to `t`. */
     127                 :            :   template <typename TT>
     128                 :     682970 :   void set(const TT& t)
     129                 :            :   {
     130                 :            :     static_assert(std::is_same_v<T, TT>, "Incorrect type for ReferenceStat");
     131                 :            :     if constexpr (configuration::isStatisticsBuild())
     132                 :            :     {
     133                 :     682970 :       d_data->d_value = &t;
     134                 :            :     }
     135                 :     682970 :   }
     136                 :            :   /** Commit the value currently pointed to and release it. */
     137                 :     454545 :   void reset()
     138                 :            :   {
     139                 :            :     if constexpr (configuration::isStatisticsBuild())
     140                 :            :     {
     141                 :     454545 :       d_data->commit();
     142                 :     454545 :       d_data->d_value = nullptr;
     143                 :            :     }
     144                 :     454545 :   }
     145                 :            :   /** Copy the current value of the referenced object. */
     146                 :     673882 :   ~ReferenceStat()
     147                 :            :   {
     148                 :            :     if constexpr (configuration::isStatisticsBuild())
     149                 :            :     {
     150                 :     673882 :       d_data->commit();
     151                 :            :     }
     152                 :     673882 :   }
     153                 :            : 
     154                 :            :  private:
     155                 :            :   /** Construct from a pointer to the internal data */
     156                 :     682970 :   ReferenceStat(StatisticReferenceValue<T>* data) : d_data(data) {}
     157                 :            :   /** The actual data that lives in the registry */
     158                 :            :   StatisticReferenceValue<T>* d_data;
     159                 :            : };
     160                 :            : 
     161                 :            : /**
     162                 :            :  * Stores the size of some container that exists outside of this statistic.
     163                 :            :  * Note that the referenced container must have a lifetime that is longer than
     164                 :            :  * the lifetime of the `SizeStat` object. Upon destruction of the `SizeStat`
     165                 :            :  * the current size of the referenced container is copied into the
     166                 :            :  * `StatisticsRegistry`.
     167                 :            :  */
     168                 :            : template <typename T>
     169                 :            : class SizeStat
     170                 :            : {
     171                 :            :  public:
     172                 :            :   /** Allow access to private constructor */
     173                 :            :   friend class StatisticsRegistry;
     174                 :            :   /** Value stored for this statistic */
     175                 :            :   using stat_type = StatisticSizeValue<T>;
     176                 :            :   /** Reset the reference to point to `t`. */
     177                 :      50198 :   void set(const T& t)
     178                 :            :   {
     179                 :            :     if constexpr (configuration::isStatisticsBuild())
     180                 :            :     {
     181                 :      50198 :       d_data->d_value = &t;
     182                 :            :     }
     183                 :      50198 :   }
     184                 :            :   /** Copy the current size of the referenced container. */
     185                 :      49853 :   ~SizeStat()
     186                 :            :   {
     187                 :            :     if constexpr (configuration::isStatisticsBuild())
     188                 :            :     {
     189                 :      49853 :       d_data->commit();
     190                 :            :     }
     191                 :      49853 :   }
     192                 :            : 
     193                 :            :  private:
     194                 :            :   /** Construct from a pointer to the internal data */
     195                 :      50198 :   SizeStat(stat_type* data) : d_data(data) {}
     196                 :            :   /** The actual data that lives in the registry */
     197                 :            :   stat_type* d_data;
     198                 :            : };
     199                 :            : 
     200                 :            : class CodeTimer;
     201                 :            : /**
     202                 :            :  * Collects cumulative runtimes. The timer can be started and stopped
     203                 :            :  * arbitrarily like a stopwatch. The value of the statistic is the
     204                 :            :  * accumulated time over all (start,stop) pairs.
     205                 :            :  * While the runtimes are stored in nanosecond precision internally,
     206                 :            :  * the API exports runtimes as integral numbers in millisecond
     207                 :            :  * precision.
     208                 :            :  *
     209                 :            :  * Note that it is recommended to use it in an RAII fashion using the
     210                 :            :  * `CodeTimer` class.
     211                 :            :  */
     212                 :            : class TimerStat
     213                 :            : {
     214                 :            :  public:
     215                 :            :   /** Utility for RAII-style timing of code blocks */
     216                 :            :   using CodeTimer = cvc5::internal::CodeTimer;
     217                 :            :   /** Allow access to private constructor */
     218                 :            :   friend class StatisticsRegistry;
     219                 :            :   /** Value stored for this statistic */
     220                 :            :   using stat_type = StatisticTimerValue;
     221                 :            : 
     222                 :            :   /** Start the timer. Assumes it is not already running. */
     223                 :            :   void start();
     224                 :            :   /** Stop the timer. Assumes it is running. */
     225                 :            :   void stop();
     226                 :            :   /** Checks whether the timer is running. */
     227                 :            :   bool running() const;
     228                 :            : 
     229                 :            :  private:
     230                 :            :   /** Construct from a pointer to the internal data */
     231                 :    6292950 :   TimerStat(stat_type* data) : d_data(data) {}
     232                 :            :   /** The actual data that lives in the registry */
     233                 :            :   stat_type* d_data;
     234                 :            : };
     235                 :            : 
     236                 :            : /**
     237                 :            :  * Utility class to make it easier to call `stop` at the end of a code
     238                 :            :  * block. When constructed, it starts the timer. When destructed, it stops
     239                 :            :  * the timer.
     240                 :            :  *
     241                 :            :  * Allows for reentrant usage. If `allow_reentrant` is true, we check
     242                 :            :  * whether the timer is already running. If so, this particular instance
     243                 :            :  * of `CodeTimer` neither starts nor stops the actual timer, but leaves
     244                 :            :  * this to the first (or outermost) `CodeTimer`.
     245                 :            :  */
     246                 :            : class CodeTimer
     247                 :            : {
     248                 :            :  public:
     249                 :            :   /** Disallow copying */
     250                 :            :   CodeTimer(const CodeTimer& timer) = delete;
     251                 :            :   /** Disallow assignment */
     252                 :            :   CodeTimer& operator=(const CodeTimer& timer) = delete;
     253                 :            :   /**
     254                 :            :    * Start the timer.
     255                 :            :    * If `allow_reentrant` is true we check whether the timer is already
     256                 :            :    * running. If so, this particular instance of `CodeTimer` neither starts
     257                 :            :    * nor stops the actual timer, but leaves this to the first (or outermost)
     258                 :            :    * `CodeTimer`.
     259                 :            :    */
     260                 :            :   CodeTimer(TimerStat& timer, bool allow_reentrant = false);
     261                 :            :   /** Stop the timer */
     262                 :            :   ~CodeTimer();
     263                 :            : 
     264                 :            :  private:
     265                 :            :   /** Reference to the timer this utility works on */
     266                 :            :   TimerStat& d_timer;
     267                 :            :   /** Whether this timer is reentrant (i.e. does not do anything) */
     268                 :            :   bool d_reentrant;
     269                 :            : };
     270                 :            : 
     271                 :            : /**
     272                 :            :  * Stores a simple value that can be set manually using regular assignment
     273                 :            :  * or the `set` method.
     274                 :            :  *
     275                 :            :  * To convert to the API representation in `cvc5::Stat`, `T` can only be one
     276                 :            :  * of the types accepted by the `cvc5::Stat` constructors (or be implicitly
     277                 :            :  * converted to one of them).
     278                 :            :  */
     279                 :            : template <typename T>
     280                 :            : class ValueStat
     281                 :            : {
     282                 :            :  public:
     283                 :            :   /** Allow access to private constructor */
     284                 :            :   friend class StatisticsRegistry;
     285                 :            :   friend class IntStat;
     286                 :            :   /** Value stored for this statistic */
     287                 :            :   using stat_type = StatisticBackedValue<T>;
     288                 :            :   /** Set to `t` */
     289                 :      23966 :   void set(const T& t)
     290                 :            :   {
     291                 :            :     if constexpr (configuration::isStatisticsBuild())
     292                 :            :     {
     293                 :      23966 :       d_data->d_value = t;
     294                 :            :     }
     295                 :      23966 :   }
     296                 :            :   /** Set to `t` */
     297                 :            :   ValueStat<T>& operator=(const T& t)
     298                 :            :   {
     299                 :            :     if constexpr (configuration::isStatisticsBuild())
     300                 :            :     {
     301                 :            :       set(t);
     302                 :            :     }
     303                 :            :     return *this;
     304                 :            :   }
     305                 :     129524 :   T get() const
     306                 :            :   {
     307                 :            :     if constexpr (configuration::isStatisticsBuild())
     308                 :            :     {
     309                 :     129524 :       return d_data->d_value;
     310                 :            :     }
     311                 :            :     return T();
     312                 :            :   }
     313                 :            : 
     314                 :            :  private:
     315                 :            :   /** Construct from a pointer to the internal data */
     316                 :   16256318 :   ValueStat(StatisticBackedValue<T>* data) : d_data(data) {}
     317                 :            :   /** The actual data that lives in the registry */
     318                 :            :   StatisticBackedValue<T>* d_data;
     319                 :            : };
     320                 :            : 
     321                 :            : /**
     322                 :            :  * Stores an integer value as int64_t.
     323                 :            :  * Supports the most useful standard operators (assignment, pre- and
     324                 :            :  * post-increment, addition assignment) and some custom ones (maximum
     325                 :            :  * assignment, minimum assignment).
     326                 :            :  */
     327                 :            : class IntStat : public ValueStat<int64_t>
     328                 :            : {
     329                 :            :  public:
     330                 :            :   /** Allow access to private constructor */
     331                 :            :   friend class StatisticsRegistry;
     332                 :            :   /** Value stored for this statistic */
     333                 :            :   using stat_type = StatisticBackedValue<int64_t>;
     334                 :            :   /** Set to given value */
     335                 :            :   IntStat& operator=(int64_t val);
     336                 :            :   /** Pre-increment for the integer */
     337                 :            :   IntStat& operator++();
     338                 :            :   /** Post-increment for the integer */
     339                 :            :   IntStat& operator++(int);
     340                 :            :   /** Add `val` to the integer */
     341                 :            :   IntStat& operator+=(int64_t val);
     342                 :            :   /** Assign the maximum of the current value and `val` */
     343                 :            :   void maxAssign(int64_t val);
     344                 :            :   /** Assign the minimum of the current value and `val` */
     345                 :            :   void minAssign(int64_t val);
     346                 :            : 
     347                 :            :  private:
     348                 :            :   /** Construct from a pointer to the internal data */
     349                 :   16080600 :   IntStat(stat_type* data) : ValueStat(data) {}
     350                 :            : };
     351                 :            : 
     352                 :            : }  // namespace cvc5::internal
     353                 :            : 
     354                 :            : #endif