Branch data     Line data    Source code

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