GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/util/resource_manager.h Lines: 2 2 100.0 %
Date: 2021-03-22 Branches: 4 6 66.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file resource_manager.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Gereon Kremer, Mathias Preiner, Liana Hadarean
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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.\endverbatim
11
 **
12
 ** \brief Provides mechanisms to limit resources.
13
 **
14
 ** This file provides the ResourceManager class. It can be used to impose
15
 ** (cumulative and per-call) resource limits on the solver, as well as per-call
16
 ** time limits.
17
 **/
18
19
#include "cvc4_public.h"
20
21
#ifndef CVC4__RESOURCE_MANAGER_H
22
#define CVC4__RESOURCE_MANAGER_H
23
24
#include <stdint.h>
25
#include <chrono>
26
#include <memory>
27
#include <vector>
28
29
namespace CVC4 {
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
9620
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
/**
70
 * This class manages resource limits (cumulative or per call) and (per call)
71
 * time limits. The available resources are listed in ResourceManager::Resource
72
 * and their individual costs are configured via command line options.
73
 */
74
class ResourceManager
75
{
76
 public:
77
  /** Types of resources. */
78
  enum class Resource
79
  {
80
    ArithPivotStep,
81
    ArithNlLemmaStep,
82
    BitblastStep,
83
    BvEagerAssertStep,
84
    BvPropagationStep,
85
    BvSatConflictsStep,
86
    BvSatPropagateStep,
87
    BvSatSimplifyStep,
88
    CnfStep,
89
    DecisionStep,
90
    LemmaStep,
91
    NewSkolemStep,
92
    ParseStep,
93
    PreprocessStep,
94
    QuantifierStep,
95
    RestartStep,
96
    RewriteStep,
97
    SatConflictStep,
98
    TheoryCheckStep,
99
  };
100
101
  /** Construst a resource manager. */
102
  ResourceManager(StatisticsRegistry& statistics_registry, Options& options);
103
  /** Default destructor. */
104
  ~ResourceManager();
105
  /** Can not be copied. */
106
  ResourceManager(const ResourceManager&) = delete;
107
  /** Can not be moved. */
108
  ResourceManager(ResourceManager&&) = delete;
109
  /** Can not be copied. */
110
  ResourceManager& operator=(const ResourceManager&) = delete;
111
  /** Can not be moved. */
112
  ResourceManager& operator=(ResourceManager&&) = delete;
113
114
  /** Checks whether any limit is active. */
115
  bool limitOn() const { return cumulativeLimitOn() || perCallLimitOn(); }
116
  /** Checks whether any cumulative limit is active. */
117
  bool cumulativeLimitOn() const;
118
  /** Checks whether any per-call limit is active. */
119
  bool perCallLimitOn() const;
120
121
  /** Checks whether resources have been exhausted. */
122
  bool outOfResources() const;
123
  /** Checks whether time has been exhausted. */
124
  bool outOfTime() const;
125
  /** Checks whether any limit has been exhausted. */
126
20239
  bool out() const { return d_on && (outOfResources() || outOfTime()); }
127
128
  /** Retrieves amount of resources used overall. */
129
  uint64_t getResourceUsage() const;
130
  /** Retrieves time used over all calls. */
131
  uint64_t getTimeUsage() const;
132
  /** Retrieves the remaining number of cumulative resources. */
133
  uint64_t getResourceRemaining() const;
134
135
  /** Retrieves resource budget for this call. */
136
  uint64_t getResourceBudgetForThisCall() { return d_thisCallResourceBudget; }
137
138
  /**
139
   * Spends a given resources. Throws an UnsafeInterruptException if there are
140
   * no remaining resources.
141
   */
142
  void spendResource(Resource r);
143
144
  /** Sets the resource limit. */
145
  void setResourceLimit(uint64_t units, bool cumulative = false);
146
  /** Sets the time limit. */
147
  void setTimeLimit(uint64_t millis);
148
  /** Sets whether resource limitation is enabled. */
149
  void enable(bool on);
150
151
  /**
152
   * Resets perCall limits to mark the start of a new call,
153
   * updates budget for current call and starts the timer
154
   */
155
  void beginCall();
156
157
  /**
158
   * Marks the end of a SmtEngine check call, stops the per
159
   * call timer.
160
   */
161
  void endCall();
162
163
  /**
164
   * Registers a listener that is notified on a resource out or (per-call)
165
   * timeout.
166
   */
167
  void registerListener(Listener* listener);
168
169
 private:
170
  /** The per-call wall clock timer. */
171
  WallClockTimer d_perCallTimer;
172
173
  /** A user-imposed per-call time budget, in milliseconds. 0 = no limit. */
174
  uint64_t d_timeBudgetPerCall;
175
  /** A user-imposed cumulative resource budget. 0 = no limit. */
176
  uint64_t d_resourceBudgetCumulative;
177
  /** A user-imposed per-call resource budget. 0 = no limit. */
178
  uint64_t d_resourceBudgetPerCall;
179
180
  /** The total number of milliseconds used. */
181
  uint64_t d_cumulativeTimeUsed;
182
  /** The total amount of resources used. */
183
  uint64_t d_cumulativeResourceUsed;
184
185
  /** The amount of resources used during this call. */
186
  uint64_t d_thisCallResourceUsed;
187
188
  /**
189
   * The resource budget for this call (min between per call
190
   * budget and left-over cumulative budget.)
191
   */
192
  uint64_t d_thisCallResourceBudget;
193
194
  /** A flag indicating whether resource limitation is active. */
195
  bool d_on;
196
197
  /** Receives a notification on reaching a limit. */
198
  std::vector<Listener*> d_listeners;
199
200
  void spendResource(unsigned amount);
201
202
  struct Statistics;
203
  std::unique_ptr<Statistics> d_statistics;
204
205
  Options& d_options;
206
207
}; /* class ResourceManager */
208
209
}  // namespace CVC4
210
211
#endif /* CVC4__RESOURCE_MANAGER_H */