/usr/include/cvc4/util/resource_manager.h is in libcvc4-dev 1.5-1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 | /********************* */
/*! \file resource_manager.h
** \verbatim
** Top contributors (to current version):
** Liana Hadarean, Tim King, Morgan Deters
** This file is part of the CVC4 project.
** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
**
** [[ Add lengthier description here ]]
** \todo document this file
**/
#include <cvc4/cvc4_public.h>
#ifndef __CVC4__RESOURCE_MANAGER_H
#define __CVC4__RESOURCE_MANAGER_H
#include <cstddef>
#include <sys/time.h>
#include <cvc4/base/exception.h>
#include <cvc4/base/listener.h>
#include <cvc4/util/unsafe_interrupt_exception.h>
namespace CVC4 {
/**
* A helper class to keep track of a time budget and signal
* the PropEngine when the budget expires.
*/
class CVC4_PUBLIC Timer {
uint64_t d_ms;
timeval d_wall_limit;
clock_t d_cpu_start_time;
clock_t d_cpu_limit;
bool d_wall_time;
/** Return the milliseconds elapsed since last set() cpu time. */
uint64_t elapsedCPU() const;
/** Return the milliseconds elapsed since last set() wall time. */
uint64_t elapsedWall() const;
public:
/** Construct a Timer. */
Timer()
: d_ms(0)
, d_cpu_start_time(0)
, d_cpu_limit(0)
, d_wall_time(true)
{}
/** Is the timer currently active? */
bool on() const {
return d_ms != 0;
}
/** Set a millisecond timer (0==off). */
void set(uint64_t millis, bool wall_time = true);
/** Return the milliseconds elapsed since last set() wall/cpu time
depending on d_wall_time*/
uint64_t elapsed() const;
bool expired() const;
};/* class Timer */
class CVC4_PUBLIC ResourceManager {
Timer d_cumulativeTimer;
Timer d_perCallTimer;
/** A user-imposed cumulative time budget, in milliseconds. 0 = no limit. */
uint64_t d_timeBudgetCumulative;
/** A user-imposed per-call time budget, in milliseconds. 0 = no limit. */
uint64_t d_timeBudgetPerCall;
/** A user-imposed cumulative resource budget. 0 = no limit. */
uint64_t d_resourceBudgetCumulative;
/** A user-imposed per-call resource budget. 0 = no limit. */
uint64_t d_resourceBudgetPerCall;
/** The number of milliseconds used. */
uint64_t d_cumulativeTimeUsed;
/** The amount of resource used. */
uint64_t d_cumulativeResourceUsed;
/** The ammount of resource used during this call. */
uint64_t d_thisCallResourceUsed;
/**
* The ammount of resource budget for this call (min between per call
* budget and left-over cumulative budget.
*/
uint64_t d_thisCallTimeBudget;
uint64_t d_thisCallResourceBudget;
bool d_isHardLimit;
bool d_on;
bool d_cpuTime;
uint64_t d_spendResourceCalls;
/** Counter indicating how often to check resource manager in loops */
static const uint64_t s_resourceCount;
/** Receives a notification on reaching a hard limit. */
ListenerCollection d_hardListeners;
/** Receives a notification on reaching a hard limit. */
ListenerCollection d_softListeners;
/**
* ResourceManagers cannot be copied as they are given an explicit
* list of Listeners to respond to.
*/
ResourceManager(const ResourceManager&) CVC4_UNDEFINED;
/**
* ResourceManagers cannot be assigned as they are given an explicit
* list of Listeners to respond to.
*/
ResourceManager& operator=(const ResourceManager&) CVC4_UNDEFINED;
public:
ResourceManager();
bool limitOn() const { return cumulativeLimitOn() || perCallLimitOn(); }
bool cumulativeLimitOn() const;
bool perCallLimitOn() const;
bool outOfResources() const;
bool outOfTime() const;
bool out() const { return d_on && (outOfResources() || outOfTime()); }
/**
* This returns a const uint64_t& to support being used as a ReferenceStat.
*/
const uint64_t& getResourceUsage() const;
uint64_t getTimeUsage() const;
uint64_t getResourceRemaining() const;
uint64_t getTimeRemaining() const;
uint64_t getResourceBudgetForThisCall() {
return d_thisCallResourceBudget;
}
void spendResource(unsigned ammount) throw(UnsafeInterruptException);
void setHardLimit(bool value);
void setResourceLimit(uint64_t units, bool cumulative = false);
void setTimeLimit(uint64_t millis, bool cumulative = false);
void useCPUTime(bool cpu);
void enable(bool on);
/**
* Resets perCall limits to mark the start of a new call,
* updates budget for current call and starts the timer
*/
void beginCall();
/**
* Marks the end of a SmtEngine check call, stops the per
* call timer, updates cumulative time used.
*/
void endCall();
static uint64_t getFrequencyCount() { return s_resourceCount; }
/**
* Registers a listener that is notified on a hard resource out.
*
* This Registration must be destroyed by the user before this
* ResourceManager.
*/
ListenerCollection::Registration* registerHardListener(Listener* listener);
/**
* Registers a listener that is notified on a soft resource out.
*
* This Registration must be destroyed by the user before this
* ResourceManager.
*/
ListenerCollection::Registration* registerSoftListener(Listener* listener);
};/* class ResourceManager */
}/* CVC4 namespace */
#endif /* __CVC4__RESOURCE_MANAGER_H */
|