Branch data     Line data    Source code

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