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