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                 :            : 
      15                 :            : #include "cvc5_public.h"
      16                 :            : 
      17                 :            : #ifndef CVC5__RESOURCE_MANAGER_H
      18                 :            : #define CVC5__RESOURCE_MANAGER_H
      19                 :            : 
      20                 :            : #include <stdint.h>
      21                 :            : 
      22                 :            : #include <array>
      23                 :            : #include <chrono>
      24                 :            : #include <memory>
      25                 :            : #include <vector>
      26                 :            : 
      27                 :            : #include "theory/inference_id.h"
      28                 :            : 
      29                 :            : namespace cvc5::internal {
      30                 :            : 
      31                 :            : class Listener;
      32                 :            : class Options;
      33                 :            : class StatisticsRegistry;
      34                 :            : 
      35                 :            : /**
      36                 :            :  * This class implements a easy to use wall clock timer based on std::chrono.
      37                 :            :  */
      38                 :            : class WallClockTimer
      39                 :            : {
      40                 :            :   /**
      41                 :            :    * The underlying clock that is used.
      42                 :            :    * std::chrono::system_clock represents wall clock time.
      43                 :            :    */
      44                 :            :   using clock = std::chrono::system_clock;
      45                 :            :   /** A time point of the clock we use. */
      46                 :            :   using time_point = std::chrono::time_point<clock>;
      47                 :            : 
      48                 :            :  public:
      49                 :            :   /** Checks whether this timer is active. */
      50                 :            :   bool on() const;
      51                 :            :   /**
      52                 :            :    * Activates this timer with a timeout in milliseconds.
      53                 :            :    * If millis is zero, the timer is deactivated.
      54                 :            :    */
      55                 :            :   void set(uint64_t millis);
      56                 :            :   /** Returns the number of elapsed milliseconds since the last call to set().
      57                 :            :    */
      58                 :            :   uint64_t elapsed() const;
      59                 :            :   /** Checks whether the current timeout has expired. */
      60                 :            :   bool expired() const;
      61                 :            : 
      62                 :            :  private:
      63                 :            :   /** The start of this timer. */
      64                 :            :   time_point d_start;
      65                 :            :   /** The point in time when this timer expires. */
      66                 :            :   time_point d_limit;
      67                 :            : };
      68                 :            : 
      69                 :            : /** Types of resources. */
      70                 :            : enum class Resource
      71                 :            : {
      72                 :            :   ArithPivotStep,
      73                 :            :   ArithNlCoveringStep,
      74                 :            :   ArithNlLemmaStep,
      75                 :            :   BitblastStep,
      76                 :            :   BvSatStep,
      77                 :            :   CnfStep,
      78                 :            :   DecisionStep,
      79                 :            :   LemmaStep,
      80                 :            :   NewSkolemStep,
      81                 :            :   ParseStep,
      82                 :            :   PreprocessStep,
      83                 :            :   QuantifierStep,
      84                 :            :   RestartStep,
      85                 :            :   RewriteStep,
      86                 :            :   SatConflictStep,
      87                 :            :   SygusCheckStep,
      88                 :            :   TheoryCheckStep,
      89                 :            :   TheoryFullCheckStep,
      90                 :            :   FindSynthStep,
      91                 :            :   Unknown
      92                 :            : };
      93                 :            : 
      94                 :            : const char* toString(Resource r);
      95                 :            : std::ostream& operator<<(std::ostream& os, Resource r);
      96                 :            : 
      97                 :            : namespace resman_detail {
      98                 :            : /** The upper bound of values from the theory::InferenceId enum */
      99                 :            : constexpr std::size_t InferenceIdMax =
     100                 :            :     static_cast<std::size_t>(theory::InferenceId::UNKNOWN);
     101                 :            : /** The upper bound of values from the Resource enum */
     102                 :            : constexpr std::size_t ResourceMax = static_cast<std::size_t>(Resource::Unknown);
     103                 :            : };  // namespace resman_detail
     104                 :            : 
     105                 :            : /**
     106                 :            :  * This class manages resource limits (cumulative or per call) and (per call)
     107                 :            :  * time limits. The available resources are listed in Resource and their
     108                 :            :  * individual costs are configured via command line options.
     109                 :            :  */
     110                 :            : class ResourceManager
     111                 :            : {
     112                 :            :  public:
     113                 :            :   /** Construct a resource manager. */
     114                 :            :   ResourceManager(StatisticsRegistry& statistics_registry,
     115                 :            :                   const Options& options);
     116                 :            :   /** Default destructor. */
     117                 :            :   ~ResourceManager();
     118                 :            :   /** Can not be copied. */
     119                 :            :   ResourceManager(const ResourceManager&) = delete;
     120                 :            :   /** Can not be moved. */
     121                 :            :   ResourceManager(ResourceManager&&) = delete;
     122                 :            :   /** Can not be copied. */
     123                 :            :   ResourceManager& operator=(const ResourceManager&) = delete;
     124                 :            :   /** Can not be moved. */
     125                 :            :   ResourceManager& operator=(ResourceManager&&) = delete;
     126                 :            : 
     127                 :     121806 :   void setEnabled(bool enabled) { d_enabled = enabled; }
     128                 :            : 
     129                 :            :   /** Checks whether any limit is active. */
     130                 :            :   bool limitOn() const;
     131                 :            : 
     132                 :            :   /** Checks whether resources have been exhausted. */
     133                 :            :   bool outOfResources() const;
     134                 :            :   /** Checks whether time has been exhausted. */
     135                 :            :   bool outOfTime() const;
     136                 :            :   /** Checks whether any limit has been exhausted. */
     137 [ +  + ][ +  + ]:  191926413 :   bool out() const { return outOfResources() || outOfTime(); }
     138                 :            : 
     139                 :            :   /** Retrieves amount of resources used overall. */
     140                 :            :   uint64_t getResourceUsage() const;
     141                 :            :   /** Retrieves time used over all calls. */
     142                 :            :   uint64_t getTimeUsage() const;
     143                 :            :   /** Retrieves the remaining time until the time limit is reached. */
     144                 :            :   uint64_t getRemainingTime() const;
     145                 :            :   /** Retrieves the remaining number of cumulative resources. */
     146                 :            :   uint64_t getResourceRemaining() const;
     147                 :            : 
     148                 :            :   /**
     149                 :            :    * Spends a given resource. Calls the listener to interrupt the solver if
     150                 :            :    * there are no remaining resources.
     151                 :            :    */
     152                 :            :   void spendResource(Resource r);
     153                 :            :   /**
     154                 :            :    * Gets the number of resources spent for r so far.
     155                 :            :    */
     156                 :            :   uint64_t getResource(Resource r) const;
     157                 :            :   /**
     158                 :            :    * Spends a given resource. Calls the listener to interrupt the solver if
     159                 :            :    * there are no remaining resources.
     160                 :            :    */
     161                 :            :   void spendResource(theory::InferenceId iid);
     162                 :            : 
     163                 :            :   /**
     164                 :            :    * Resets perCall limits to mark the start of a new call,
     165                 :            :    * updates budget for current call and starts the timer
     166                 :            :    */
     167                 :            :   void beginCall();
     168                 :            : 
     169                 :            :   /**
     170                 :            :    * Marks the end of a SolverEngine check call, stops the per
     171                 :            :    * call timer.
     172                 :            :    */
     173                 :            :   void refresh();
     174                 :            : 
     175                 :            :   /**
     176                 :            :    * Registers a listener that is notified on a resource out or (per-call)
     177                 :            :    * timeout.
     178                 :            :    */
     179                 :            :   void registerListener(Listener* listener);
     180                 :            : 
     181                 :            :  private:
     182                 :            :   const Options& d_options;
     183                 :            : 
     184                 :            :   /**
     185                 :            :    * If the resource manager is not enabled, then the checks whether we are out
     186                 :            :    * of resources are disabled. Resources are still spent, however.
     187                 :            :    */
     188                 :            :   bool d_enabled;
     189                 :            : 
     190                 :            :   /** The per-call wall clock timer. */
     191                 :            :   WallClockTimer d_perCallTimer;
     192                 :            : 
     193                 :            :   /** The total number of milliseconds used. */
     194                 :            :   uint64_t d_cumulativeTimeUsed;
     195                 :            :   /** The total amount of resources used. */
     196                 :            :   uint64_t d_cumulativeResourceUsed;
     197                 :            : 
     198                 :            :   /** The amount of resources used during this call. */
     199                 :            :   uint64_t d_thisCallResourceUsed;
     200                 :            : 
     201                 :            :   /**
     202                 :            :    * The resource budget for this call (min between per call
     203                 :            :    * budget and left-over cumulative budget.)
     204                 :            :    */
     205                 :            :   uint64_t d_thisCallResourceBudget;
     206                 :            : 
     207                 :            :   /** Receives a notification on reaching a limit. */
     208                 :            :   std::vector<Listener*> d_listeners;
     209                 :            : 
     210                 :            :   void spendResource(uint64_t amount);
     211                 :            : 
     212                 :            :   /** Weights for InferenceId resources */
     213                 :            :   std::array<uint64_t, resman_detail::InferenceIdMax + 1> d_infidWeights;
     214                 :            :   /** Weights for Resource resources */
     215                 :            :   std::array<uint64_t, resman_detail::ResourceMax + 1> d_resourceWeights;
     216                 :            : 
     217                 :            :   struct Statistics;
     218                 :            :   /** The statistics object */
     219                 :            :   std::unique_ptr<Statistics> d_statistics;
     220                 :            : }; /* class ResourceManager */
     221                 :            : 
     222                 :            : }  // namespace cvc5::internal
     223                 :            : 
     224                 :            : #endif /* CVC5__RESOURCE_MANAGER_H */