Branch data     Line data    Source code

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