Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Gereon Kremer, Aina Niemetz, Matthew Sotoudeh
       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                 :            :  * Central statistics registry.
      14                 :            :  *
      15                 :            :  * The StatisticsRegistry that issues statistic proxy objects.
      16                 :            :  */
      17                 :            : 
      18                 :            : #include "util/statistics_registry.h"
      19                 :            : 
      20                 :            : #include "options/base_options.h"
      21                 :            : #include "util/statistics_public.h"
      22                 :            : 
      23                 :            : namespace cvc5::internal {
      24                 :            : 
      25                 :     144218 : StatisticsRegistry::StatisticsRegistry(bool internal,
      26                 :            :                                        bool all,
      27                 :     144218 :                                        bool registerPublic)
      28                 :     144218 :     : d_internal(internal), d_all(all)
      29                 :            : {
      30         [ +  + ]:     144218 :   if (registerPublic)
      31                 :            :   {
      32                 :     144217 :     registerPublicStatistics(*this);
      33                 :            :   }
      34                 :     144218 : }
      35                 :            : 
      36                 :     205559 : AverageStat StatisticsRegistry::registerAverage(const std::string& name,
      37                 :            :                                                 bool internal)
      38                 :            : {
      39                 :     205559 :   return registerStat<AverageStat>(name, internal);
      40                 :            : }
      41                 :   16433700 : IntStat StatisticsRegistry::registerInt(const std::string& name, bool internal)
      42                 :            : {
      43                 :   16433700 :   return registerStat<IntStat>(name, internal);
      44                 :            : }
      45                 :    6251320 : TimerStat StatisticsRegistry::registerTimer(const std::string& name,
      46                 :            :                                             bool internal)
      47                 :            : {
      48                 :    6251320 :   return registerStat<TimerStat>(name, internal);
      49                 :            : }
      50                 :            : 
      51                 :          0 : void StatisticsRegistry::storeSnapshot()
      52                 :            : {
      53                 :            :   if constexpr (configuration::isStatisticsBuild())
      54                 :            :   {
      55                 :          0 :     d_lastSnapshot = std::make_unique<Snapshot>();
      56         [ -  - ]:          0 :     for (const auto& s : d_stats)
      57                 :            :     {
      58 [ -  - ][ -  - ]:          0 :       if (!d_internal && s.second->d_internal) continue;
                 [ -  - ]
      59                 :          0 :       if (!d_all && s.second->isDefault()) continue;
      60                 :            :       d_lastSnapshot->emplace(
      61                 :          0 :           s.first,
      62                 :          0 :           s.second->getViewer());
      63                 :            :     }
      64                 :            :   }
      65                 :          0 : }
      66                 :            : 
      67                 :         10 : StatisticBaseValue* StatisticsRegistry::get(const std::string& name) const
      68                 :            : {
      69                 :            :   if constexpr (configuration::isStatisticsBuild())
      70                 :            :   {
      71                 :         10 :     auto it = d_stats.find(name);
      72         [ -  + ]:         10 :     if (it == d_stats.end()) return nullptr;
      73                 :         10 :     return it->second.get();
      74                 :            :   }
      75                 :            :   return nullptr;
      76                 :            : }
      77                 :            : 
      78                 :          0 : void StatisticsRegistry::print(std::ostream& os) const
      79                 :            : {
      80                 :            :   if constexpr (configuration::isStatisticsBuild())
      81                 :            :   {
      82         [ -  - ]:          0 :     for (const auto& s : d_stats)
      83                 :            :     {
      84 [ -  - ][ -  - ]:          0 :       if (!d_internal && s.second->d_internal) continue;
                 [ -  - ]
      85                 :          0 :       if (!d_all && s.second->isDefault()) continue;
      86                 :          0 :       os << s.first << " = " << *s.second << std::endl;
      87                 :            :     }
      88                 :            :   }
      89                 :          0 : }
      90                 :            : 
      91                 :         15 : void StatisticsRegistry::printSafe(int fd) const
      92                 :            : {
      93                 :            :   if constexpr (configuration::isStatisticsBuild())
      94                 :            :   {
      95         [ +  + ]:       1351 :     for (const auto& s : d_stats)
      96                 :            :     {
      97 [ +  - ][ +  + ]:       1336 :       if (!d_internal && s.second->d_internal) continue;
                 [ +  + ]
      98 [ +  - ][ +  + ]:        705 :       if (!d_all && s.second->isDefault()) continue;
                 [ +  + ]
      99                 :            : 
     100                 :         15 :       safe_print(fd, s.first);
     101                 :         15 :       safe_print(fd, " = ");
     102                 :         15 :       s.second->printSafe(fd);
     103                 :         15 :       safe_print(fd, "\n");
     104                 :            :     }
     105                 :            :   }
     106                 :         15 : }
     107                 :          0 : void StatisticsRegistry::printDiff(std::ostream& os) const
     108                 :            : {
     109                 :            :   if constexpr (configuration::isStatisticsBuild())
     110                 :            :   {
     111         [ -  - ]:          0 :     if (!d_lastSnapshot)
     112                 :            :     {
     113                 :            :       // we have no snapshot, print as usual
     114                 :          0 :       print(os);
     115                 :          0 :       return;
     116                 :            :     }
     117         [ -  - ]:          0 :     for (const auto& s : d_stats)
     118                 :            :     {
     119 [ -  - ][ -  - ]:          0 :       if (!d_internal && s.second->d_internal) continue;
                 [ -  - ]
     120                 :          0 :       if (!d_all && s.second->isDefault())
     121                 :            :       {
     122                 :          0 :         auto oldit = d_lastSnapshot->find(s.first);
     123                 :          0 :         if (oldit != d_lastSnapshot->end() && oldit->second != s.second->getViewer())
     124                 :            :         {
     125                 :            :           // present in the snapshot, now defaulted
     126                 :          0 :           os << s.first << " = " << *s.second << " (was ";
     127                 :          0 :           detail::print(os, oldit->second);
     128                 :          0 :           os << ")" << std::endl;
     129                 :            :         }
     130                 :            :       }
     131                 :            :       else
     132                 :            :       {
     133                 :          0 :         auto oldit = d_lastSnapshot->find(s.first);
     134         [ -  - ]:          0 :         if (oldit == d_lastSnapshot->end())
     135                 :            :         {
     136                 :            :           // not present in the snapshot
     137                 :          0 :           os << s.first << " = " << *s.second << " (was <default>)"
     138                 :          0 :              << std::endl;
     139                 :            :         }
     140         [ -  - ]:          0 :         else if (oldit->second != s.second->getViewer())
     141                 :            :         {
     142                 :            :           // present in the snapshot, print old value
     143                 :          0 :           os << s.first << " = " << *s.second << " (was ";
     144                 :          0 :           detail::print(os, oldit->second);
     145                 :          0 :           os << ")" << std::endl;
     146                 :            :         }
     147                 :            :       }
     148                 :            :     }
     149                 :            :   }
     150                 :            : }
     151                 :            : 
     152                 :          0 : std::ostream& operator<<(std::ostream& os, const StatisticsRegistry& sr)
     153                 :            : {
     154                 :          0 :   sr.print(os);
     155                 :          0 :   return os;
     156                 :            : }
     157                 :            : 
     158                 :            : }  // namespace cvc5::internal