Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/util/resource_manager.cpp	Lines:	75	142	52.8 %
Date:	2021-08-06	Branches:	40	200	20.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Gereon Kremer, Mathias Preiner, Liana Hadarean
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 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.
 * ****************************************************************************
 *
 * This file provides the ResourceManager class. It can be used to impose
 * (cumulative and per-call) resource limits on the solver, as well as per-call
 * time limits.
 */
#include "util/resource_manager.h"

#include <algorithm>
#include <ostream>

#include "base/check.h"
#include "base/listener.h"
#include "base/output.h"
#include "options/base_options.h"
#include "options/option_exception.h"
#include "options/options.h"
#include "util/statistics_registry.h"

using namespace std;

namespace cvc5 {

bool WallClockTimer::on() const
{
  // default-constructed time points are at the respective epoch
  return d_limit.time_since_epoch().count() != 0;
}
void WallClockTimer::set(uint64_t millis)
{
  if (millis == 0)
  {
    // reset / deactivate
    d_start = time_point();
    d_limit = time_point();
  }
  else
  {
    // set to now() + millis
    d_start = clock::now();
    d_limit = d_start + std::chrono::milliseconds(millis);
  }
}
uint64_t WallClockTimer::elapsed() const
{
  if (!on()) return 0;
  // now() - d_start casted to milliseconds
  return std::chrono::duration_cast<std::chrono::milliseconds>(clock::now()
                                                               - d_start)
      .count();
}
bool WallClockTimer::expired() const
{
  // whether d_limit is in the past
  if (!on()) return false;
  return d_limit <= clock::now();
}

/*---------------------------------------------------------------------------*/

const char* toString(Resource r)
{
  switch (r)
  {
    case Resource::ArithPivotStep: return "ArithPivotStep";
    case Resource::ArithNlLemmaStep: return "ArithNlLemmaStep";
    case Resource::BitblastStep: return "BitblastStep";
    case Resource::BvEagerAssertStep: return "BvEagerAssertStep";
    case Resource::BvPropagationStep: return "BvPropagationStep";
    case Resource::BvSatConflictsStep: return "BvSatConflictsStep";
    case Resource::BvSatPropagateStep: return "BvSatPropagateStep";
    case Resource::BvSatSimplifyStep: return "BvSatSimplifyStep";
    case Resource::CnfStep: return "CnfStep";
    case Resource::DecisionStep: return "DecisionStep";
    case Resource::LemmaStep: return "LemmaStep";
    case Resource::NewSkolemStep: return "NewSkolemStep";
    case Resource::ParseStep: return "ParseStep";
    case Resource::PreprocessStep: return "PreprocessStep";
    case Resource::QuantifierStep: return "QuantifierStep";
    case Resource::RestartStep: return "RestartStep";
    case Resource::RewriteStep: return "RewriteStep";
    case Resource::SatConflictStep: return "SatConflictStep";
    case Resource::TheoryCheckStep: return "TheoryCheckStep";
    default: return "?Resource?";
  }
}
std::ostream& operator<<(std::ostream& os, Resource r)
{
  return os << toString(r);
}

struct ResourceManager::Statistics
{
  ReferenceStat<uint64_t> d_resourceUnitsUsed;
  IntStat d_spendResourceCalls;
  HistogramStat<theory::InferenceId> d_inferenceIdSteps;
  HistogramStat<Resource> d_resourceSteps;
  Statistics(StatisticsRegistry& stats);
};

ResourceManager::Statistics::Statistics(StatisticsRegistry& stats)
    : d_resourceUnitsUsed(
        stats.registerReference<uint64_t>("resource::resourceUnitsUsed")),
      d_spendResourceCalls(stats.registerInt("resource::spendResourceCalls")),
      d_inferenceIdSteps(stats.registerHistogram<theory::InferenceId>(
          "resource::steps::inference-id")),
      d_resourceSteps(
          stats.registerHistogram<Resource>("resource::steps::resource"))
{
}

bool parseOption(const std::string& optarg, std::string& name, uint64_t& weight)
{
  auto pos = optarg.find('=');
  // Check if there is a '='
  if (pos == std::string::npos) return false;
  // The name is the part before '='
  name = optarg.substr(0, pos);
  // The weight is the part after '='
  std::string num = optarg.substr(pos + 1);
  std::size_t converted;
  weight = std::stoull(num, &converted);
  // Check everything after '=' was converted
  return converted == num.size();
}

template <typename T, typename Weights>
bool setWeight(const std::string& name, uint64_t weight, Weights& weights)
{
  using theory::toString;
  for (std::size_t i = 0; i < weights.size(); ++i)
  {
    if (name == toString(static_cast<T>(i)))
    {
      weights[i] = weight;
      return true;
    }
  }
  return false;
}

/*---------------------------------------------------------------------------*/

ResourceManager::ResourceManager(StatisticsRegistry& stats,
                                 const Options& options)
    : d_options(options),
      d_perCallTimer(),
      d_cumulativeTimeUsed(0),
      d_cumulativeResourceUsed(0),
      d_thisCallResourceUsed(0),
      d_statistics(new ResourceManager::Statistics(stats))
{
  d_statistics->d_resourceUnitsUsed.set(d_cumulativeResourceUsed);

  d_infidWeights.fill(1);
  d_resourceWeights.fill(1);
  for (const auto& opt : d_options.base.resourceWeightHolder)
  {
    std::string name;
    uint64_t weight;
    if (parseOption(opt, name, weight))
    {
      if (setWeight<theory::InferenceId>(name, weight, d_infidWeights))
        continue;
      if (setWeight<Resource>(name, weight, d_resourceWeights)) continue;
      throw OptionException("Did not recognize resource type " + name);
    }
  }
}

ResourceManager::~ResourceManager() {}

uint64_t ResourceManager::getResourceUsage() const
{
  return d_cumulativeResourceUsed;
}

uint64_t ResourceManager::getTimeUsage() const { return d_cumulativeTimeUsed; }

uint64_t ResourceManager::getResourceRemaining() const
{
  if (d_options.base.cumulativeResourceLimit <= d_cumulativeResourceUsed)
    return 0;
  return d_options.base.cumulativeResourceLimit - d_cumulativeResourceUsed;
}

void ResourceManager::spendResource(uint64_t amount)
{
  ++d_statistics->d_spendResourceCalls;
  d_cumulativeResourceUsed += amount;

  Debug("limit") << "ResourceManager::spendResource()" << std::endl;
  d_thisCallResourceUsed += amount;
  if (out())
  {
    Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl;
    Trace("limit") << "          on call "
                   << d_statistics->d_spendResourceCalls.get() << std::endl;
    if (outOfTime())
    {
      Trace("limit") << "ResourceManager::spendResource: elapsed time"
                     << d_perCallTimer.elapsed() << std::endl;
    }

    for (Listener* l : d_listeners)
    {
      l->notify();
    }
  }
}

void ResourceManager::spendResource(Resource r)
{
  std::size_t i = static_cast<std::size_t>(r);
  Assert(d_resourceWeights.size() > i);
  d_statistics->d_resourceSteps << r;
  spendResource(d_resourceWeights[i]);
}

void ResourceManager::spendResource(theory::InferenceId iid)
{
  std::size_t i = static_cast<std::size_t>(iid);
  Assert(d_infidWeights.size() > i);
  d_statistics->d_inferenceIdSteps << iid;
  spendResource(d_infidWeights[i]);
}

void ResourceManager::beginCall()
{
  d_perCallTimer.set(d_options.base.perCallMillisecondLimit);
  d_thisCallResourceUsed = 0;

  if (d_options.base.cumulativeResourceLimit > 0)
  {
    // Compute remaining cumulative resource budget
    d_thisCallResourceBudget =
        d_options.base.cumulativeResourceLimit - d_cumulativeResourceUsed;
  }
  if (d_options.base.perCallResourceLimit > 0)
  {
    // Check if per-call resource budget is even smaller
    if (d_options.base.perCallResourceLimit < d_thisCallResourceBudget)
    {
      d_thisCallResourceBudget = d_options.base.perCallResourceLimit;
    }
  }
}

void ResourceManager::endCall()
{
  d_cumulativeTimeUsed += d_perCallTimer.elapsed();
  d_perCallTimer.set(0);
  d_thisCallResourceUsed = 0;
}

bool ResourceManager::limitOn() const
{
  return (d_options.base.cumulativeResourceLimit > 0)
         || (d_options.base.perCallMillisecondLimit > 0)
         || (d_options.base.perCallResourceLimit > 0);
}

bool ResourceManager::outOfResources() const
{
  if (d_options.base.perCallResourceLimit > 0)
  {
    // Check if per-call resources are exhausted
    if (d_thisCallResourceUsed >= d_options.base.perCallResourceLimit)
    {
      return true;
    }
  }
  if (d_options.base.cumulativeResourceLimit > 0)
  {
    // Check if cumulative resources are exhausted
    if (d_cumulativeResourceUsed >= d_options.base.cumulativeResourceLimit)
    {
      return true;
    }
  }
  return false;
}

bool ResourceManager::outOfTime() const
{
  if (d_options.base.perCallMillisecondLimit == 0) return false;
  return d_perCallTimer.expired();
}

void ResourceManager::registerListener(Listener* listener)
{
  return d_listeners.push_back(listener);
}

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Gereon Kremer, Mathias Preiner, Liana Hadarean
4		*
5		* This file is part of the cvc5 project.
6		*
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.
11		* ****************************************************************************
12		*
13		* This file provides the ResourceManager class. It can be used to impose
14		* (cumulative and per-call) resource limits on the solver, as well as per-call
15		* time limits.
16		*/
17		#include "util/resource_manager.h"
18
19		#include <algorithm>
20		#include <ostream>
21
22		#include "base/check.h"
23		#include "base/listener.h"
24		#include "base/output.h"
25		#include "options/base_options.h"
26		#include "options/option_exception.h"
27		#include "options/options.h"
28		#include "util/statistics_registry.h"
29
30		using namespace std;
31
32		namespace cvc5 {
33
34	20995	bool WallClockTimer::on() const
35		{
36		// default-constructed time points are at the respective epoch
37	20995	return d_limit.time_since_epoch().count() != 0;
38		}
39	30406	void WallClockTimer::set(uint64_t millis)
40		{
41	30406	if (millis == 0)
42		{
43		// reset / deactivate
44	30395	d_start = time_point();
45	30395	d_limit = time_point();
46		}
47		else
48		{
49		// set to now() + millis
50	11	d_start = clock::now();
51	11	d_limit = d_start + std::chrono::milliseconds(millis);
52		}
53	30406	}
54	15188	uint64_t WallClockTimer::elapsed() const
55		{
56	15188	if (!on()) return 0;
57		// now() - d_start casted to milliseconds
58	44	return std::chrono::duration_cast<std::chrono::milliseconds>(clock::now()
59	33	- d_start)
60	11	.count();
61		}
62	5807	bool WallClockTimer::expired() const
63		{
64		// whether d_limit is in the past
65	5807	if (!on()) return false;
66	2307	return d_limit <= clock::now();
67		}
68
69		/---------------------------------------------------------------------------/
70
71		const char* toString(Resource r)
72		{
73		switch (r)
74		{
75		case Resource::ArithPivotStep: return "ArithPivotStep";
76		case Resource::ArithNlLemmaStep: return "ArithNlLemmaStep";
77		case Resource::BitblastStep: return "BitblastStep";
78		case Resource::BvEagerAssertStep: return "BvEagerAssertStep";
79		case Resource::BvPropagationStep: return "BvPropagationStep";
80		case Resource::BvSatConflictsStep: return "BvSatConflictsStep";
81		case Resource::BvSatPropagateStep: return "BvSatPropagateStep";
82		case Resource::BvSatSimplifyStep: return "BvSatSimplifyStep";
83		case Resource::CnfStep: return "CnfStep";
84		case Resource::DecisionStep: return "DecisionStep";
85		case Resource::LemmaStep: return "LemmaStep";
86		case Resource::NewSkolemStep: return "NewSkolemStep";
87		case Resource::ParseStep: return "ParseStep";
88		case Resource::PreprocessStep: return "PreprocessStep";
89		case Resource::QuantifierStep: return "QuantifierStep";
90		case Resource::RestartStep: return "RestartStep";
91		case Resource::RewriteStep: return "RewriteStep";
92		case Resource::SatConflictStep: return "SatConflictStep";
93		case Resource::TheoryCheckStep: return "TheoryCheckStep";
94		default: return "?Resource?";
95		}
96		}
97		std::ostream& operator<<(std::ostream& os, Resource r)
98		{
99		return os << toString(r);
100		}
101
102	10497	struct ResourceManager::Statistics
103		{
104		ReferenceStat<uint64_t> d_resourceUnitsUsed;
105		IntStat d_spendResourceCalls;
106		HistogramStat<theory::InferenceId> d_inferenceIdSteps;
107		HistogramStat<Resource> d_resourceSteps;
108		Statistics(StatisticsRegistry& stats);
109		};
110
111	10497	ResourceManager::Statistics::Statistics(StatisticsRegistry& stats)
112		: d_resourceUnitsUsed(
113		stats.registerReference<uint64_t>("resource::resourceUnitsUsed")),
114	20994	d_spendResourceCalls(stats.registerInt("resource::spendResourceCalls")),
115		d_inferenceIdSteps(stats.registerHistogram<theory::InferenceId>(
116	20994	"resource::steps::inference-id")),
117		d_resourceSteps(
118	41988	stats.registerHistogram<Resource>("resource::steps::resource"))
119		{
120	10497	}
121
122		bool parseOption(const std::string& optarg, std::string& name, uint64_t& weight)
123		{
124		auto pos = optarg.find('=');
125		// Check if there is a '='
126		if (pos == std::string::npos) return false;
127		// The name is the part before '='
128		name = optarg.substr(0, pos);
129		// The weight is the part after '='
130		std::string num = optarg.substr(pos + 1);
131		std::size_t converted;
132		weight = std::stoull(num, &converted);
133		// Check everything after '=' was converted
134		return converted == num.size();
135		}
136
137		template <typename T, typename Weights>
138		bool setWeight(const std::string& name, uint64_t weight, Weights& weights)
139		{
140		using theory::toString;
141		for (std::size_t i = 0; i < weights.size(); ++i)
142		{
143		if (name == toString(static_cast<T>(i)))
144		{
145		weights[i] = weight;
146		return true;
147		}
148		}
149		return false;
150		}
151
152		/---------------------------------------------------------------------------/
153
154	10497	ResourceManager::ResourceManager(StatisticsRegistry& stats,
155	10497	const Options& options)
156		: d_options(options),
157		d_perCallTimer(),
158		d_cumulativeTimeUsed(0),
159		d_cumulativeResourceUsed(0),
160		d_thisCallResourceUsed(0),
161	10497	d_statistics(new ResourceManager::Statistics(stats))
162		{
163	10497	d_statistics->d_resourceUnitsUsed.set(d_cumulativeResourceUsed);
164
165	10497	d_infidWeights.fill(1);
166	10497	d_resourceWeights.fill(1);
167	10497	for (const auto& opt : d_options.base.resourceWeightHolder)
168		{
169		std::string name;
170		uint64_t weight;
171		if (parseOption(opt, name, weight))
172		{
173		if (setWeight<theory::InferenceId>(name, weight, d_infidWeights))
174		continue;
175		if (setWeight<Resource>(name, weight, d_resourceWeights)) continue;
176		throw OptionException("Did not recognize resource type " + name);
177		}
178		}
179	10497	}
180
181	10497	ResourceManager::~ResourceManager() {}
182
183	15188	uint64_t ResourceManager::getResourceUsage() const
184		{
185	15188	return d_cumulativeResourceUsed;
186		}
187
188	15188	uint64_t ResourceManager::getTimeUsage() const { return d_cumulativeTimeUsed; }
189
190		uint64_t ResourceManager::getResourceRemaining() const
191		{
192		if (d_options.base.cumulativeResourceLimit <= d_cumulativeResourceUsed)
193		return 0;
194		return d_options.base.cumulativeResourceLimit - d_cumulativeResourceUsed;
195		}
196
197	85906466	void ResourceManager::spendResource(uint64_t amount)
198		{
199	85906466	++d_statistics->d_spendResourceCalls;
200	85906466	d_cumulativeResourceUsed += amount;
201
202	85906466	Debug("limit") << "ResourceManager::spendResource()" << std::endl;
203	85906466	d_thisCallResourceUsed += amount;
204	85906466	if (out())
205		{
206		Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl;
207		Trace("limit") << " on call "
208		<< d_statistics->d_spendResourceCalls.get() << std::endl;
209		if (outOfTime())
210		{
211		Trace("limit") << "ResourceManager::spendResource: elapsed time"
212		<< d_perCallTimer.elapsed() << std::endl;
213		}
214
215		for (Listener* l : d_listeners)
216		{
217		l->notify();
218		}
219		}
220	85906466	}
221
222	85128912	void ResourceManager::spendResource(Resource r)
223		{
224	85128912	std::size_t i = static_cast<std::size_t>(r);
225	85128912	Assert(d_resourceWeights.size() > i);
226	85128912	d_statistics->d_resourceSteps << r;
227	85128912	spendResource(d_resourceWeights[i]);
228	85128912	}
229
230	777554	void ResourceManager::spendResource(theory::InferenceId iid)
231		{
232	777554	std::size_t i = static_cast<std::size_t>(iid);
233	777554	Assert(d_infidWeights.size() > i);
234	777554	d_statistics->d_inferenceIdSteps << iid;
235	777554	spendResource(d_infidWeights[i]);
236	777554	}
237
238	15218	void ResourceManager::beginCall()
239		{
240	15218	d_perCallTimer.set(d_options.base.perCallMillisecondLimit);
241	15218	d_thisCallResourceUsed = 0;
242
243	15218	if (d_options.base.cumulativeResourceLimit > 0)
244		{
245		// Compute remaining cumulative resource budget
246		d_thisCallResourceBudget =
247		d_options.base.cumulativeResourceLimit - d_cumulativeResourceUsed;
248		}
249	15218	if (d_options.base.perCallResourceLimit > 0)
250		{
251		// Check if per-call resource budget is even smaller
252		if (d_options.base.perCallResourceLimit < d_thisCallResourceBudget)
253		{
254		d_thisCallResourceBudget = d_options.base.perCallResourceLimit;
255		}
256		}
257	15218	}
258
259	15188	void ResourceManager::endCall()
260		{
261	15188	d_cumulativeTimeUsed += d_perCallTimer.elapsed();
262	15188	d_perCallTimer.set(0);
263	15188	d_thisCallResourceUsed = 0;
264	15188	}
265
266		bool ResourceManager::limitOn() const
267		{
268		return (d_options.base.cumulativeResourceLimit > 0)
269		\|\| (d_options.base.perCallMillisecondLimit > 0)
270		\|\| (d_options.base.perCallResourceLimit > 0);
271		}
272
273	85921684	bool ResourceManager::outOfResources() const
274		{
275	85921684	if (d_options.base.perCallResourceLimit > 0)
276		{
277		// Check if per-call resources are exhausted
278		if (d_thisCallResourceUsed >= d_options.base.perCallResourceLimit)
279		{
280		return true;
281		}
282		}
283	85921684	if (d_options.base.cumulativeResourceLimit > 0)
284		{
285		// Check if cumulative resources are exhausted
286		if (d_cumulativeResourceUsed >= d_options.base.cumulativeResourceLimit)
287		{
288		return true;
289		}
290		}
291	85921684	return false;
292		}
293
294	85921684	bool ResourceManager::outOfTime() const
295		{
296	85921684	if (d_options.base.perCallMillisecondLimit == 0) return false;
297	5807	return d_perCallTimer.expired();
298		}
299
300	10497	void ResourceManager::registerListener(Listener* listener)
301		{
302	10497	return d_listeners.push_back(listener);
303		}
304
305	29322	} // namespace cvc5