blob: a16f60910ba550724820d7c06a4a2afb320117e9 (
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 {
unsigned long 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. */
unsigned long elapsedCPU() const;
/** Return the milliseconds elapsed since last set() wall time. */
unsigned long 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(unsigned long millis, bool wall_time = true);
/** Return the milliseconds elapsed since last set() wall/cpu time
depending on d_wall_time*/
unsigned long 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. */
unsigned long d_timeBudgetCumulative;
/** A user-imposed per-call time budget, in milliseconds. 0 = no limit. */
unsigned long d_timeBudgetPerCall;
/** A user-imposed cumulative resource budget. 0 = no limit. */
unsigned long d_resourceBudgetCumulative;
/** A user-imposed per-call resource budget. 0 = no limit. */
unsigned long d_resourceBudgetPerCall;
/** The number of milliseconds used. */
unsigned long d_cumulativeTimeUsed;
/** The amount of resource used. */
unsigned long d_cumulativeResourceUsed;
/** The ammount of resource used during this call. */
unsigned long d_thisCallResourceUsed;
/**
* The ammount of resource budget for this call (min between per call
* budget and left-over cumulative budget.
*/
unsigned long d_thisCallTimeBudget;
unsigned long d_thisCallResourceBudget;
bool d_isHardLimit;
bool d_on;
bool d_cpuTime;
unsigned long d_spendResourceCalls;
/** Counter indicating how often to check resource manager in loops */
static const unsigned long 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()); }
unsigned long getResourceUsage() const;
unsigned long getTimeUsage() const;
unsigned long getResourceRemaining() const;
unsigned long getTimeRemaining() const;
unsigned long getResourceBudgetForThisCall() {
return d_thisCallResourceBudget;
}
void spendResource() throw(UnsafeInterruptException);
void setHardLimit(bool value);
void setResourceLimit(unsigned long units, bool cumulative = false);
void setTimeLimit(unsigned long 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 unsigned long getFrequencyCount() { return s_resourceCount; }
};/* class ResourceManager */
}/* CVC4 namespace */
#endif /* __CVC4__RESOURCE_MANAGER_H */
|
