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 data classes
      11                 :            :  *
      12                 :            :  * The statistic data classes that actually hold the data for the statistics.
      13                 :            :  *
      14                 :            :  * Conceptually, every statistic consists of a data object and a proxy object.
      15                 :            :  * The data objects (statistic values) are derived from `StatisticBaseValue`
      16                 :            :  * and live in the `StatisticsRegistry`.
      17                 :            :  * They are solely exported to the proxy objects, which should be the sole
      18                 :            :  * way to manipulate the data of a data object.
      19                 :            :  * The data objects themselves need to implement printing (normal and safe) and
      20                 :            :  * conversion to the API type `Stat`.
      21                 :            :  */
      22                 :            : 
      23                 :            : #include "util/statistics_value.h"
      24                 :            : 
      25                 :            : #include "util/ostream_util.h"
      26                 :            : 
      27                 :            : namespace cvc5::internal {
      28                 :            : 
      29                 :            : // standard helper, see https://en.cppreference.com/w/cpp/utility/variant/visit
      30                 :            : template <class... Ts>
      31                 :            : struct overloaded : Ts...
      32                 :            : {
      33                 :            :   using Ts::operator()...;
      34                 :            : };
      35                 :            : template <class... Ts>
      36                 :            : overloaded(Ts...) -> overloaded<Ts...>;
      37                 :            : 
      38                 :            : namespace detail {
      39                 :      13788 : std::ostream& print(std::ostream& out, const StatExportData& sed)
      40                 :            : {
      41                 :      13788 :   std::visit(overloaded{
      42                 :       8743 :                  [&out](int64_t v) { out << v; },
      43                 :            :                  [&out](uint64_t v) { out << v; },
      44                 :        108 :                  [&out](double v) { out << v; },
      45                 :       3167 :                  [&out](const std::string& v) { out << v; },
      46                 :       4100 :                  [&out](const std::map<std::string, uint64_t>& v) {
      47                 :       1770 :                    out << "{ ";
      48                 :       1770 :                    bool first = true;
      49         [ +  + ]:       2092 :                    for (const auto& e : v)
      50                 :            :                    {
      51         [ +  + ]:        322 :                      if (!first)
      52                 :        238 :                        out << ", ";
      53                 :            :                      else
      54                 :         84 :                        first = false;
      55                 :        322 :                      out << e.first << ": " << e.second;
      56                 :            :                    }
      57                 :       1770 :                    out << " }";
      58                 :       1770 :                  },
      59                 :            :              },
      60                 :            :              sed);
      61                 :      13788 :   return out;
      62                 :            : }
      63                 :            : }  // namespace detail
      64                 :            : 
      65                 :   30936474 : StatisticBaseValue::~StatisticBaseValue() {}
      66                 :            : 
      67                 :        132 : std::ostream& operator<<(std::ostream& out, const StatisticBaseValue& sbv)
      68                 :            : {
      69                 :        132 :   return detail::print(out, sbv.getViewer());
      70                 :            : }
      71                 :            : 
      72                 :       1141 : StatExportData StatisticAverageValue::getViewer() const { return get(); }
      73                 :            : 
      74                 :       1140 : bool StatisticAverageValue::isDefault() const { return d_count == 0; }
      75                 :            : 
      76                 :          0 : void StatisticAverageValue::printSafe(int fd) const
      77                 :            : {
      78                 :          0 :   safe_print<double>(fd, get());
      79                 :          0 : }
      80                 :            : 
      81                 :       1141 : double StatisticAverageValue::get() const { return d_sum / d_count; }
      82                 :            : 
      83                 :      33938 : StatExportData StatisticTimerValue::getViewer() const
      84                 :            : {
      85                 :      33938 :   return std::to_string(get()) + "ms";
      86                 :            : }
      87                 :            : 
      88                 :      33939 : bool StatisticTimerValue::isDefault() const
      89                 :            : {
      90 [ +  + ][ +  + ]:      33939 :   return !d_running && d_duration.count() == 0;
      91                 :            : }
      92                 :            : 
      93                 :         13 : void StatisticTimerValue::printSafe(int fd) const
      94                 :            : {
      95                 :         13 :   safe_print<uint64_t>(fd, get());
      96                 :         13 :   safe_print<std::string>(fd, "ms");
      97                 :         13 : }
      98                 :            : 
      99                 :            : /** Make sure that we include the time of a currently running timer */
     100                 :      33951 : uint64_t StatisticTimerValue::get() const
     101                 :            : {
     102                 :      33951 :   auto data = d_duration;
     103         [ +  + ]:      33951 :   if (d_running)
     104                 :            :   {
     105                 :        301 :     data += clock::now() - d_start;
     106                 :            :   }
     107                 :      33951 :   return static_cast<int64_t>(data / std::chrono::milliseconds(1));
     108                 :            : }
     109                 :            : 
     110                 :            : }  // namespace cvc5::internal