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                 :            :  * This file provides the ResourceManager class. It can be used to impose
      11                 :            :  * (cumulative and per-call) resource limits on the solver, as well as per-call
      12                 :            :  * time limits.
      13                 :            :  */
      14                 :            : #include "util/resource_manager.h"
      15                 :            : 
      16                 :            : #include <algorithm>
      17                 :            : #include <ostream>
      18                 :            : 
      19                 :            : #include "base/check.h"
      20                 :            : #include "base/listener.h"
      21                 :            : #include "base/output.h"
      22                 :            : #include "options/base_options.h"
      23                 :            : #include "options/option_exception.h"
      24                 :            : #include "options/options.h"
      25                 :            : #include "util/statistics_registry.h"
      26                 :            : 
      27                 :            : using namespace std;
      28                 :            : 
      29                 :            : namespace cvc5::internal {
      30                 :            : 
      31                 :    1044845 : bool WallClockTimer::on() const
      32                 :            : {
      33                 :            :   // default-constructed time points are at the respective epoch
      34                 :    1044845 :   return d_limit.time_since_epoch().count() != 0;
      35                 :            : }
      36                 :     181055 : void WallClockTimer::set(uint64_t millis)
      37                 :            : {
      38         [ +  + ]:     181055 :   if (millis == 0)
      39                 :            :   {
      40                 :            :     // reset / deactivate
      41                 :     178429 :     d_start = time_point();
      42                 :     178429 :     d_limit = time_point();
      43                 :            :   }
      44                 :            :   else
      45                 :            :   {
      46                 :            :     // set to now() + millis
      47                 :       2626 :     d_start = clock::now();
      48                 :       2626 :     d_limit = d_start + std::chrono::milliseconds(millis);
      49                 :            :   }
      50                 :     181055 : }
      51                 :     127785 : uint64_t WallClockTimer::elapsed() const
      52                 :            : {
      53         [ +  + ]:     127785 :   if (!on()) return 0;
      54                 :            :   // now() - d_start casted to milliseconds
      55                 :       2631 :   return std::chrono::duration_cast<std::chrono::milliseconds>(clock::now()
      56                 :       2631 :                                                                - d_start)
      57                 :       2631 :       .count();
      58                 :            : }
      59                 :     917060 : bool WallClockTimer::expired() const
      60                 :            : {
      61                 :            :   // whether d_limit is in the past
      62         [ +  + ]:     917060 :   if (!on()) return false;
      63                 :     898644 :   return d_limit <= clock::now();
      64                 :            : }
      65                 :            : 
      66                 :            : /*---------------------------------------------------------------------------*/
      67                 :            : 
      68                 :       1760 : const char* toString(Resource r)
      69                 :            : {
      70 [ +  - ][ -  - ]:       1760 :   switch (r)
         [ +  + ][ +  + ]
         [ -  - ][ +  - ]
         [ -  + ][ +  - ]
         [ +  + ][ -  - ]
      71                 :            :   {
      72                 :         12 :     case Resource::ArithPivotStep: return "ArithPivotStep";
      73                 :          0 :     case Resource::ArithNlCoveringStep: return "ArithNlCoveringStep";
      74                 :          0 :     case Resource::ArithNlLemmaStep: return "ArithNlLemmaStep";
      75                 :          0 :     case Resource::BitblastStep: return "BitblastStep";
      76                 :        285 :     case Resource::BvSatStep: return "BvSatStep";
      77                 :         13 :     case Resource::CnfStep: return "CnfStep";
      78                 :        285 :     case Resource::DecisionStep: return "DecisionStep";
      79                 :         12 :     case Resource::LemmaStep: return "LemmaStep";
      80                 :          0 :     case Resource::NewSkolemStep: return "NewSkolemStep";
      81                 :          0 :     case Resource::ParseStep: return "ParseStep";
      82                 :        285 :     case Resource::PreprocessStep: return "PreprocessStep";
      83                 :          0 :     case Resource::QuantifierStep: return "QuantifierStep";
      84                 :          0 :     case Resource::RestartStep: return "RestartStep";
      85                 :         13 :     case Resource::RewriteStep: return "RewriteStep";
      86                 :        285 :     case Resource::SatConflictStep: return "SatConflictStep";
      87                 :          0 :     case Resource::SygusCheckStep: return "SygusCheckStep";
      88                 :        285 :     case Resource::TheoryCheckStep: return "TheoryCheckStep";
      89                 :        285 :     case Resource::TheoryFullCheckStep: return "TheoryFullCheckStep";
      90                 :          0 :     case Resource::FindSynthStep: return "FindSynthStep";
      91                 :          0 :     default: return "?Resource?";
      92                 :            :   }
      93                 :            : }
      94                 :       1760 : std::ostream& operator<<(std::ostream& os, Resource r)
      95                 :            : {
      96                 :       1760 :   return os << toString(r);
      97                 :            : }
      98                 :            : 
      99                 :            : struct ResourceManager::Statistics
     100                 :            : {
     101                 :            :   ReferenceStat<uint64_t> d_resourceUnitsUsed;
     102                 :            :   IntStat d_spendResourceCalls;
     103                 :            :   HistogramStat<theory::InferenceId> d_inferenceIdSteps;
     104                 :            :   HistogramStat<Resource> d_resourceSteps;
     105                 :            :   Statistics(StatisticsRegistry& stats);
     106                 :            : };
     107                 :            : 
     108                 :      75842 : ResourceManager::Statistics::Statistics(StatisticsRegistry& stats)
     109                 :      75842 :     : d_resourceUnitsUsed(
     110                 :            :           stats.registerReference<uint64_t>("resource::resourceUnitsUsed")),
     111                 :      75842 :       d_spendResourceCalls(stats.registerInt("resource::spendResourceCalls")),
     112                 :      75842 :       d_inferenceIdSteps(stats.registerHistogram<theory::InferenceId>(
     113                 :            :           "resource::steps::inference-id")),
     114                 :            :       d_resourceSteps(
     115                 :      75842 :           stats.registerHistogram<Resource>("resource::steps::resource"))
     116                 :            : {
     117                 :      75842 : }
     118                 :            : 
     119                 :          0 : bool parseOption(const std::string& optarg, std::string& name, uint64_t& weight)
     120                 :            : {
     121                 :          0 :   auto pos = optarg.find('=');
     122                 :            :   // Check if there is a '='
     123         [ -  - ]:          0 :   if (pos == std::string::npos) return false;
     124                 :            :   // The name is the part before '='
     125                 :          0 :   name = optarg.substr(0, pos);
     126                 :            :   // The weight is the part after '='
     127                 :          0 :   std::string num = optarg.substr(pos + 1);
     128                 :            :   std::size_t converted;
     129                 :          0 :   weight = std::stoull(num, &converted);
     130                 :            :   // Check everything after '=' was converted
     131                 :          0 :   return converted == num.size();
     132                 :          0 : }
     133                 :            : 
     134                 :            : template <typename T, typename Weights>
     135                 :          0 : bool setWeight(const std::string& name, uint64_t weight, Weights& weights)
     136                 :            : {
     137                 :            :   using theory::toString;
     138         [ -  - ]:          0 :   for (std::size_t i = 0; i < weights.size(); ++i)
     139                 :            :   {
     140         [ -  - ]:          0 :     if (name == toString(static_cast<T>(i)))
     141                 :            :     {
     142                 :          0 :       weights[i] = weight;
     143                 :          0 :       return true;
     144                 :            :     }
     145                 :            :   }
     146                 :          0 :   return false;
     147                 :            : }
     148                 :            : 
     149                 :            : /*---------------------------------------------------------------------------*/
     150                 :            : 
     151                 :      75842 : ResourceManager::ResourceManager(StatisticsRegistry& stats,
     152                 :      75842 :                                  const Options& options)
     153                 :      75842 :     : d_options(options),
     154                 :      75842 :       d_enabled(true),
     155                 :      75842 :       d_perCallTimer(),
     156                 :      75842 :       d_cumulativeTimeUsed(0),
     157                 :      75842 :       d_cumulativeResourceUsed(0),
     158                 :      75842 :       d_thisCallResourceUsed(0),
     159                 :      75842 :       d_thisCallResourceBudget(0),
     160                 :      75842 :       d_statistics(new ResourceManager::Statistics(stats))
     161                 :            : {
     162                 :      75842 :   d_statistics->d_resourceUnitsUsed.set(d_cumulativeResourceUsed);
     163                 :            : 
     164                 :      75842 :   d_infidWeights.fill(1);
     165                 :      75842 :   d_resourceWeights.fill(1);
     166         [ -  + ]:      75842 :   for (const auto& opt : d_options.base.resourceWeightHolder)
     167                 :            :   {
     168                 :          0 :     std::string name;
     169                 :            :     uint64_t weight;
     170         [ -  - ]:          0 :     if (parseOption(opt, name, weight))
     171                 :            :     {
     172         [ -  - ]:          0 :       if (setWeight<theory::InferenceId>(name, weight, d_infidWeights))
     173                 :          0 :         continue;
     174         [ -  - ]:          0 :       if (setWeight<Resource>(name, weight, d_resourceWeights)) continue;
     175                 :          0 :       throw OptionException("Did not recognize resource type " + name);
     176                 :            :     }
     177         [ -  - ]:          0 :   }
     178                 :      75842 : }
     179                 :            : 
     180                 :      70803 : ResourceManager::~ResourceManager() {}
     181                 :            : 
     182                 :          0 : uint64_t ResourceManager::getResourceUsage() const
     183                 :            : {
     184                 :          0 :   return d_cumulativeResourceUsed;
     185                 :            : }
     186                 :            : 
     187                 :          0 : uint64_t ResourceManager::getTimeUsage() const { return d_cumulativeTimeUsed; }
     188                 :            : 
     189                 :       7106 : uint64_t ResourceManager::getRemainingTime() const
     190                 :            : {
     191                 :       7106 :   return d_options.base.perCallMillisecondLimit - d_perCallTimer.elapsed();
     192                 :            : }
     193                 :            : 
     194                 :          0 : uint64_t ResourceManager::getResourceRemaining() const
     195                 :            : {
     196         [ -  - ]:          0 :   if (d_options.base.cumulativeResourceLimit <= d_cumulativeResourceUsed)
     197                 :          0 :     return 0;
     198                 :          0 :   return d_options.base.cumulativeResourceLimit - d_cumulativeResourceUsed;
     199                 :            : }
     200                 :            : 
     201                 :  140702697 : void ResourceManager::spendResource(uint64_t amount)
     202                 :            : {
     203                 :  140702697 :   ++d_statistics->d_spendResourceCalls;
     204                 :  140702697 :   d_cumulativeResourceUsed += amount;
     205                 :            : 
     206         [ +  - ]:  140702697 :   Trace("limit") << "ResourceManager::spendResource()" << std::endl;
     207                 :  140702697 :   d_thisCallResourceUsed += amount;
     208         [ +  + ]:  140702697 :   if (out())
     209                 :            :   {
     210         [ +  - ]:     121004 :     Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl;
     211         [ +  - ]:     242008 :     Trace("limit") << "          on call "
     212                 :     121004 :                    << d_statistics->d_spendResourceCalls.get() << std::endl;
     213         [ +  + ]:     121004 :     if (outOfTime())
     214                 :            :     {
     215         [ +  - ]:     241340 :       Trace("limit") << "ResourceManager::spendResource: elapsed time"
     216                 :     120670 :                      << d_perCallTimer.elapsed() << std::endl;
     217                 :            :     }
     218                 :            : 
     219         [ +  + ]:     242008 :     for (Listener* l : d_listeners)
     220                 :            :     {
     221                 :     121004 :       l->notify();
     222                 :            :     }
     223                 :            :   }
     224                 :  140702697 : }
     225                 :            : 
     226                 :  139153434 : void ResourceManager::spendResource(Resource r)
     227                 :            : {
     228                 :  139153434 :   std::size_t i = static_cast<std::size_t>(r);
     229 [ -  + ][ -  + ]:  139153434 :   Assert(d_resourceWeights.size() > i);
                 [ -  - ]
     230                 :  139153434 :   d_statistics->d_resourceSteps << r;
     231                 :  139153434 :   spendResource(d_resourceWeights[i]);
     232                 :  139153434 : }
     233                 :            : 
     234                 :          0 : uint64_t ResourceManager::getResource(Resource r) const
     235                 :            : {
     236                 :          0 :   return d_statistics->d_resourceSteps.getValue(r);
     237                 :            : }
     238                 :            : 
     239                 :    1549263 : void ResourceManager::spendResource(theory::InferenceId iid)
     240                 :            : {
     241                 :    1549263 :   std::size_t i = static_cast<std::size_t>(iid);
     242 [ -  + ][ -  + ]:    1549263 :   Assert(d_infidWeights.size() > i);
                 [ -  - ]
     243                 :    1549263 :   d_statistics->d_inferenceIdSteps << iid;
     244                 :    1549263 :   spendResource(d_infidWeights[i]);
     245                 :    1549263 : }
     246                 :            : 
     247                 :      60376 : void ResourceManager::beginCall()
     248                 :            : {
     249                 :            :   // refresh here if not already done so
     250                 :      60376 :   refresh();
     251                 :            :   // begin call
     252                 :      60376 :   d_perCallTimer.set(d_options.base.perCallMillisecondLimit);
     253                 :      60376 :   d_thisCallResourceUsed = 0;
     254                 :            : 
     255         [ -  + ]:      60376 :   if (d_options.base.cumulativeResourceLimit > 0)
     256                 :            :   {
     257                 :            :     // Compute remaining cumulative resource budget
     258                 :          0 :     d_thisCallResourceBudget =
     259                 :          0 :         d_options.base.cumulativeResourceLimit - d_cumulativeResourceUsed;
     260                 :            :   }
     261         [ +  + ]:      60376 :   if (d_options.base.perCallResourceLimit > 0)
     262                 :            :   {
     263                 :            :     // Check if per-call resource budget is even smaller
     264         [ -  + ]:          2 :     if (d_options.base.perCallResourceLimit < d_thisCallResourceBudget)
     265                 :            :     {
     266                 :          0 :       d_thisCallResourceBudget = d_options.base.perCallResourceLimit;
     267                 :            :     }
     268                 :            :   }
     269                 :      60376 : }
     270                 :            : 
     271                 :     120679 : void ResourceManager::refresh()
     272                 :            : {
     273                 :     120679 :   d_cumulativeTimeUsed += d_perCallTimer.elapsed();
     274                 :     120679 :   d_perCallTimer.set(0);
     275                 :     120679 :   d_thisCallResourceUsed = 0;
     276                 :     120679 : }
     277                 :            : 
     278                 :         10 : bool ResourceManager::limitOn() const
     279                 :            : {
     280                 :         10 :   return (d_options.base.cumulativeResourceLimit > 0)
     281         [ +  - ]:         10 :          || (d_options.base.perCallMillisecondLimit > 0)
     282 [ +  - ][ -  + ]:         20 :          || (d_options.base.perCallResourceLimit > 0);
     283                 :            : }
     284                 :            : 
     285                 :  195528320 : bool ResourceManager::outOfResources() const
     286                 :            : {
     287         [ +  + ]:  195528320 :   if (!d_enabled)
     288                 :            :   {
     289                 :    1079066 :     return false;
     290                 :            :   }
     291         [ +  + ]:  194449254 :   if (d_options.base.perCallResourceLimit > 0)
     292                 :            :   {
     293                 :            :     // Check if per-call resources are exhausted
     294         [ +  + ]:        538 :     if (d_thisCallResourceUsed >= d_options.base.perCallResourceLimit)
     295                 :            :     {
     296                 :        338 :       return true;
     297                 :            :     }
     298                 :            :   }
     299         [ -  + ]:  194448916 :   if (d_options.base.cumulativeResourceLimit > 0)
     300                 :            :   {
     301                 :            :     // Check if cumulative resources are exhausted
     302         [ -  - ]:          0 :     if (d_cumulativeResourceUsed >= d_options.base.cumulativeResourceLimit)
     303                 :            :     {
     304                 :          0 :       return true;
     305                 :            :     }
     306                 :            :   }
     307                 :  194448916 :   return false;
     308                 :            : }
     309                 :            : 
     310                 :  195650612 : bool ResourceManager::outOfTime() const
     311                 :            : {
     312         [ +  + ]:  195650612 :   if (!d_enabled)
     313                 :            :   {
     314                 :    1079066 :     return false;
     315                 :            :   }
     316         [ +  + ]:  194571546 :   if (d_options.base.perCallMillisecondLimit == 0) return false;
     317                 :     917060 :   return d_perCallTimer.expired();
     318                 :            : }
     319                 :            : 
     320                 :      75822 : void ResourceManager::registerListener(Listener* listener)
     321                 :            : {
     322                 :      75822 :   return d_listeners.push_back(listener);
     323                 :            : }
     324                 :            : 
     325                 :            : }  // namespace cvc5::internal