blob: 9c2812f0f13363d5bfdd043d0b813dda27c6a879 (
plain)
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
|
/********************* */
/*! \file resource_manager.h
** \verbatim
** Original author: Liana Hadarean
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 project.
** Copyright (c) 2009-2014 New York University and The University of Iowa
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
** \brief Manages and updates various resource and time limits
**
** Manages and updates various resource and time limits.
**/
#include "cvc4_public.h"
#ifndef __CVC4__RESOURCE_MANAGER_H
#define __CVC4__RESOURCE_MANAGER_H
#include <cstddef>
#include <sys/time.h>
#include "util/exception.h"
#include "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;
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()); }
uint64_t getResourceUsage() const;
uint64_t getTimeUsage() const;
uint64_t getResourceRemaining() const;
uint64_t getTimeRemaining() const;
uint64_t getResourceBudgetForThisCall() {
return d_thisCallResourceBudget;
}
void spendResource(uint64_t 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; }
friend class SmtEngine;
};/* class ResourceManager */
}/* CVC4 namespace */
#endif /* __CVC4__RESOURCE_MANAGER_H */
|
