From: Tim King Date: Sat, 9 Jan 2016 02:19:30 +0000 (-0800) Subject: Adding a new Listener utility class. Changing the ResourceManager to use Listeners... X-Git-Tag: cvc5-1.0.0~6112 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3a973bd4fb586707a20d5e73146b79ff9fd6a77a;p=cvc5.git Adding a new Listener utility class. Changing the ResourceManager to use Listeners for reporting hard and soft resource out() events. --- diff --git a/src/base/Makefile.am b/src/base/Makefile.am index ed41db8ed..f2fe3f306 100644 --- a/src/base/Makefile.am +++ b/src/base/Makefile.am @@ -19,6 +19,8 @@ libbase_la_SOURCES = \ cvc4_assert.h \ exception.cpp \ exception.h \ + listener.cpp \ + listener.h \ modal_exception.h \ output.cpp \ output.h diff --git a/src/base/listener.cpp b/src/base/listener.cpp new file mode 100644 index 000000000..62bec5990 --- /dev/null +++ b/src/base/listener.cpp @@ -0,0 +1,66 @@ +/********************* */ +/*! \file managed_listener.h + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Output utility classes and functions + ** + ** Output utility classes and functions. + **/ + +#include "base/listener.h" + +#include + +#include "base/cvc4_assert.h" + +namespace CVC4 { + +Listener::Listener(){} +Listener::~Listener(){} + +ListenerCollection::ListenerCollection() : d_listeners() {} +ListenerCollection::~ListenerCollection() { Assert(empty()); } + +ListenerCollection::iterator ListenerCollection::addListener(Listener* listener) +{ + return d_listeners.insert(d_listeners.end(), listener); +} + +void ListenerCollection::removeListener(iterator position) { + d_listeners.erase(position); +} + +void ListenerCollection::notify() { + for(iterator i = d_listeners.begin(), iend = d_listeners.end(); i != iend; + ++i) + { + Listener* listener = *i; + listener->notify(); + } +} + +bool ListenerCollection::empty() const { return d_listeners.empty(); } + + +RegisterListener::RegisterListener(ListenerCollection* collection, + Listener* listener) + : d_listener(listener) + , d_position() + , d_collection(collection) +{ + d_position = d_collection->addListener(d_listener); +} + +RegisterListener::~RegisterListener() { + d_collection->removeListener(d_position); + delete d_listener; +} + +}/* CVC4 namespace */ diff --git a/src/base/listener.h b/src/base/listener.h new file mode 100644 index 000000000..d6828818c --- /dev/null +++ b/src/base/listener.h @@ -0,0 +1,99 @@ +/********************* */ +/*! \file listener.h + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2016 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Utility classes for listeners and collections of listeners. + ** + ** Utilities for the development of a Listener interface class. This class + ** provides a single notification that must be overwritten. This file also + ** provides a utility class for a collection of listeners and an RAII style + ** RegisterListener class for managing the relationship between Listeners + ** and the manager. + **/ + +#include "cvc4_public.h" + +#ifndef __CVC4__LISTENER_H +#define __CVC4__LISTENER_H + +#include + +namespace CVC4 { + +/** + * Listener interface class. + * + * The interface provides a notify() function. + */ +class CVC4_PUBLIC Listener { +public: + Listener(); + virtual ~Listener(); + + /** Note that notify may throw arbitrary exceptions. */ + virtual void notify() = 0; +}; + +/** + * ListenerCollection is a list of Listener instances. + * One can add and remove Listeners. + * + * ListenerCollection does not own the memory of the Listeners. + * As a sanity check, it asserted that all of its listeners + * have been removed. + */ +class CVC4_PUBLIC ListenerCollection { +public: + typedef std::list ListenerList; + typedef ListenerList::iterator iterator; + + ListenerCollection(); + + ~ListenerCollection(); + + iterator addListener(Listener* listener); + + void removeListener(iterator position); + + void notify(); + + bool empty() const; + +private: + ListenerList d_listeners; +}; + +/** + * RegisterListener is an RAII utility function for using Listener + * with ListenerCollection. + * + * On construction, the RegisterListener takes a ListenerCollection, collection, + * and a Listener*, listener. It takes over the memory for listener. It then + * add listener to collection. On destruction it removes listener and calls + * delete on listener. + * + * Because of this usage, a RegisterListener must be destroyed before + * collection. + */ +class CVC4_PUBLIC RegisterListener { +public: + RegisterListener(ListenerCollection* collection, Listener* listener); + ~RegisterListener(); + +private: + Listener* d_listener; + ListenerCollection::iterator d_position; + ListenerCollection* d_collection; +}; + + +}/* CVC4 namespace */ + +#endif /* __CVC4__LISTENER_H */ diff --git a/src/cvc4.i b/src/cvc4.i index b5ce4a5fa..4b954489c 100644 --- a/src/cvc4.i +++ b/src/cvc4.i @@ -322,6 +322,7 @@ std::set CVC4::JavaInputStreamAdapter::s_adapters; %include "util/hash.i" %include "util/proof.i" %include "util/regexp.i" +%include "util/resource_manager.i" %include "util/result.i" %include "util/sexpr.i" %include "util/statistics.i" @@ -336,7 +337,6 @@ std::set CVC4::JavaInputStreamAdapter::s_adapters; %include "expr/datatype.i" %include "expr/predicate.i" %include "expr/record.i" -%include "expr/resource_manager.i" %include "proof/unsat_core.i" // TIM: diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 4648ed3af..b3fb13253 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -39,8 +39,6 @@ libexpr_la_SOURCES = \ pickle_data.h \ pickler.cpp \ pickler.h \ - resource_manager.cpp \ - resource_manager.h \ symbol_table.cpp \ symbol_table.h \ type.cpp \ @@ -92,7 +90,6 @@ EXTRA_DIST = \ type.i \ kind.i \ expr.i \ - resource_manager.i \ record.i \ predicate.i \ variable_type_map.i \ diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 4cb75bfc7..13960b717 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -29,9 +29,8 @@ #include "expr/type_checker.h" #include "options/options.h" #include "options/smt_options.h" -#include "expr/resource_manager.h" #include "util/statistics_registry.h" - +#include "util/resource_manager.h" using namespace std; using namespace CVC4::expr; diff --git a/src/expr/resource_manager.cpp b/src/expr/resource_manager.cpp deleted file mode 100644 index f36200282..000000000 --- a/src/expr/resource_manager.cpp +++ /dev/null @@ -1,291 +0,0 @@ -/********************* */ -/*! \file resource_manager.cpp -** \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 "expr/resource_manager.h" - -#include "base/output.h" -#include "options/smt_options.h" -#include "smt/smt_engine_scope.h" -#include "theory/rewriter.h" - -#warning "TODO: Break the dependence of the ResourceManager on the theory" -#warning "rewriter and scope. Move this file back into util/ afterwards." - -using namespace std; - -namespace CVC4 { - -void Timer::set(uint64_t millis, bool wallTime) { - d_ms = millis; - Trace("limit") << "Timer::set(" << d_ms << ")" << std::endl; - // keep track of when it was set, even if it's disabled (i.e. == 0) - d_wall_time = wallTime; - if (d_wall_time) { - // Wall time - gettimeofday(&d_wall_limit, NULL); - Trace("limit") << "Timer::set(): it's " << d_wall_limit.tv_sec << "," << d_wall_limit.tv_usec << std::endl; - d_wall_limit.tv_sec += millis / 1000; - d_wall_limit.tv_usec += (millis % 1000) * 1000; - if(d_wall_limit.tv_usec > 1000000) { - ++d_wall_limit.tv_sec; - d_wall_limit.tv_usec -= 1000000; - } - Trace("limit") << "Timer::set(): limit is at " << d_wall_limit.tv_sec << "," << d_wall_limit.tv_usec << std::endl; - } else { - // CPU time - d_cpu_start_time = ((double)clock())/(CLOCKS_PER_SEC *0.001); - d_cpu_limit = d_cpu_start_time + d_ms; - } -} - -/** Return the milliseconds elapsed since last set(). */ -uint64_t Timer::elapsedWall() const { - Assert (d_wall_time); - timeval tv; - gettimeofday(&tv, NULL); - Trace("limit") << "Timer::elapsedWallTime(): it's now " << tv.tv_sec << "," << tv.tv_usec << std::endl; - tv.tv_sec -= d_wall_limit.tv_sec - d_ms / 1000; - tv.tv_usec -= d_wall_limit.tv_usec - (d_ms % 1000) * 1000; - Trace("limit") << "Timer::elapsedWallTime(): elapsed time is " << tv.tv_sec << "," << tv.tv_usec << std::endl; - return tv.tv_sec * 1000 + tv.tv_usec / 1000; -} - -uint64_t Timer::elapsedCPU() const { - Assert (!d_wall_time); - clock_t elapsed = ((double)clock())/(CLOCKS_PER_SEC *0.001)- d_cpu_start_time; - Trace("limit") << "Timer::elapsedCPUTime(): elapsed time is " << elapsed << " ms" <= d_cpu_limit) { - Debug("limit") << "Timer::expired(): OVER LIMIT!" << current << std::endl; - return true; - } - return false; -} - -const uint64_t ResourceManager::s_resourceCount = 1000; - -ResourceManager::ResourceManager() - : d_cumulativeTimer() - , d_perCallTimer() - , d_timeBudgetCumulative(0) - , d_timeBudgetPerCall(0) - , d_resourceBudgetCumulative(0) - , d_resourceBudgetPerCall(0) - , d_cumulativeTimeUsed(0) - , d_cumulativeResourceUsed(0) - , d_thisCallResourceUsed(0) - , d_thisCallTimeBudget(0) - , d_thisCallResourceBudget(0) - , d_isHardLimit() - , d_on(false) - , d_cpuTime(false) - , d_spendResourceCalls(0) -{} - - -void ResourceManager::setResourceLimit(uint64_t units, bool cumulative) { - d_on = true; - if(cumulative) { - Trace("limit") << "ResourceManager: setting cumulative resource limit to " << units << endl; - d_resourceBudgetCumulative = (units == 0) ? 0 : (d_cumulativeResourceUsed + units); - d_thisCallResourceBudget = d_resourceBudgetCumulative; - } else { - Trace("limit") << "ResourceManager: setting per-call resource limit to " << units << endl; - d_resourceBudgetPerCall = units; - } -} - -void ResourceManager::setTimeLimit(uint64_t millis, bool cumulative) { - d_on = true; - if(cumulative) { - Trace("limit") << "ResourceManager: setting cumulative time limit to " << millis << " ms" << endl; - d_timeBudgetCumulative = (millis == 0) ? 0 : (d_cumulativeTimeUsed + millis); - d_cumulativeTimer.set(millis, !d_cpuTime); - } else { - Trace("limit") << "ResourceManager: setting per-call time limit to " << millis << " ms" << endl; - d_timeBudgetPerCall = millis; - // perCall timer will be set in beginCall - } - -} - -uint64_t ResourceManager::getResourceUsage() const { - return d_cumulativeResourceUsed; -} - -uint64_t ResourceManager::getTimeUsage() const { - if (d_timeBudgetCumulative) { - return d_cumulativeTimer.elapsed(); - } - return d_cumulativeTimeUsed; -} - -uint64_t ResourceManager::getResourceRemaining() const { - if (d_thisCallResourceBudget <= d_thisCallResourceUsed) - return 0; - return d_thisCallResourceBudget - d_thisCallResourceUsed; -} - -uint64_t ResourceManager::getTimeRemaining() const { - uint64_t time_passed = d_cumulativeTimer.elapsed(); - if (time_passed >= d_thisCallTimeBudget) - return 0; - return d_thisCallTimeBudget - time_passed; -} - -void ResourceManager::spendResource(unsigned ammount) throw (UnsafeInterruptException) { - ++d_spendResourceCalls; - d_cumulativeResourceUsed += ammount; - if (!d_on) return; - - Debug("limit") << "ResourceManager::spendResource()" << std::endl; - d_thisCallResourceUsed += ammount; - if(out()) { - Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl; - Trace("limit") << " on call " << d_spendResourceCalls << std::endl; - if (outOfTime()) { - Trace("limit") << "ResourceManager::spendResource: elapsed time" << d_cumulativeTimer.elapsed() << std::endl; - } - - if (d_isHardLimit) { - if (smt::smtEngineInScope()) { - theory::Rewriter::clearCaches(); - } - throw UnsafeInterruptException(); - } - - // interrupt it next time resources are checked - if (smt::smtEngineInScope()) { - smt::currentSmtEngine()->interrupt(); - } - } -} - -void ResourceManager::beginCall() { - - d_perCallTimer.set(d_timeBudgetPerCall, !d_cpuTime); - d_thisCallResourceUsed = 0; - if (!d_on) return; - - if (cumulativeLimitOn()) { - if (d_resourceBudgetCumulative) { - d_thisCallResourceBudget = d_resourceBudgetCumulative <= d_cumulativeResourceUsed ? 0 : - d_resourceBudgetCumulative - d_cumulativeResourceUsed; - } - - if (d_timeBudgetCumulative) { - - AlwaysAssert(d_cumulativeTimer.on()); - // timer was on since the option was set - d_cumulativeTimeUsed = d_cumulativeTimer.elapsed(); - d_thisCallTimeBudget = d_timeBudgetCumulative <= d_cumulativeTimeUsed? 0 : - d_timeBudgetCumulative - d_cumulativeTimeUsed; - d_cumulativeTimer.set(d_thisCallTimeBudget, d_cpuTime); - } - // we are out of resources so we shouldn't update the - // budget for this call to the per call budget - if (d_thisCallTimeBudget == 0 || - d_thisCallResourceUsed == 0) - return; - } - - if (perCallLimitOn()) { - // take min of what's left and per-call budget - if (d_resourceBudgetPerCall) { - d_thisCallResourceBudget = d_thisCallResourceBudget < d_resourceBudgetPerCall && d_thisCallResourceBudget != 0 ? d_thisCallResourceBudget : d_resourceBudgetPerCall; - } - - if (d_timeBudgetPerCall) { - d_thisCallTimeBudget = d_thisCallTimeBudget < d_timeBudgetPerCall && d_thisCallTimeBudget != 0 ? d_thisCallTimeBudget : d_timeBudgetPerCall; - } - } -} - -void ResourceManager::endCall() { - uint64_t usedInCall = d_perCallTimer.elapsed(); - d_perCallTimer.set(0); - d_cumulativeTimeUsed += usedInCall; -} - -bool ResourceManager::cumulativeLimitOn() const { - return d_timeBudgetCumulative || d_resourceBudgetCumulative; -} - -bool ResourceManager::perCallLimitOn() const { - return d_timeBudgetPerCall || d_resourceBudgetPerCall; -} - -bool ResourceManager::outOfResources() const { - // resource limiting not enabled - if (d_resourceBudgetPerCall == 0 && - d_resourceBudgetCumulative == 0) - return false; - - return getResourceRemaining() == 0; -} - -bool ResourceManager::outOfTime() const { - if (d_timeBudgetPerCall == 0 && - d_timeBudgetCumulative == 0) - return false; - - return d_cumulativeTimer.expired() || d_perCallTimer.expired(); -} - -void ResourceManager::useCPUTime(bool cpu) { - Trace("limit") << "ResourceManager::useCPUTime("<< cpu <<")\n"; - d_cpuTime = cpu; -} - -void ResourceManager::setHardLimit(bool value) { - Trace("limit") << "ResourceManager::setHardLimit("<< value <<")\n"; - d_isHardLimit = value; -} - -void ResourceManager::enable(bool on) { - Trace("limit") << "ResourceManager::enable("<< on <<")\n"; - d_on = on; -} - -} /* namespace CVC4 */ diff --git a/src/expr/resource_manager.h b/src/expr/resource_manager.h deleted file mode 100644 index c4ad35564..000000000 --- a/src/expr/resource_manager.h +++ /dev/null @@ -1,158 +0,0 @@ -/********************* */ -/*! \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 -#include - -#include "base/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(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; } - friend class SmtEngine; -};/* class ResourceManager */ - -}/* CVC4 namespace */ - -#endif /* __CVC4__RESOURCE_MANAGER_H */ diff --git a/src/expr/resource_manager.i b/src/expr/resource_manager.i deleted file mode 100644 index 77edbd8c3..000000000 --- a/src/expr/resource_manager.i +++ /dev/null @@ -1,5 +0,0 @@ -%{ -#include "expr/resource_manager.h" -%} - -%include "expr/resource_manager.h" diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 120f63987..adbeaabd3 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -28,13 +28,13 @@ #include "expr/expr.h" #include "expr/expr_iomanip.h" #include "expr/kind.h" -#include "expr/resource_manager.h" #include "expr/type.h" #include "options/options.h" #include "options/smt_options.h" #include "parser/input.h" #include "parser/parser_exception.h" #include "smt_util/command.h" +#include "util/resource_manager.h" using namespace std; using namespace CVC4::kind; diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 630825103..9767ac7c7 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -24,7 +24,6 @@ #include "base/output.h" #include "decision/decision_engine.h" #include "expr/expr.h" -#include "expr/resource_manager.h" #include "options/base_options.h" #include "options/decision_options.h" #include "options/main_options.h" @@ -40,6 +39,7 @@ #include "smt_util/command.h" #include "theory/theory_engine.h" #include "theory/theory_registrar.h" +#include "util/resource_manager.h" #include "util/result.h" using namespace std; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 1999930d1..1962c6433 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -27,6 +27,7 @@ #include #include "base/exception.h" +#include "base/listener.h" #include "base/modal_exception.h" #include "base/output.h" #include "context/cdhashset.h" @@ -40,7 +41,6 @@ #include "expr/node.h" #include "expr/node_builder.h" #include "expr/node_self_iterator.h" -#include "expr/resource_manager.h" #include "options/arith_options.h" #include "options/arrays_options.h" #include "options/base_options.h" @@ -99,6 +99,7 @@ #include "util/configuration_private.h" #include "util/hash.h" #include "util/proof.h" +#include "util/resource_manager.h" using namespace std; using namespace CVC4; @@ -296,6 +297,32 @@ struct SmtEngineStatistics { } };/* struct SmtEngineStatistics */ + +class SoftResourceOutListener : public Listener { + public: + SoftResourceOutListener(SmtEngine& smt) : d_smt(&smt) {} + virtual void notify() { + SmtScope scope(d_smt); + Assert(smt::smtEngineInScope()); + d_smt->interrupt(); + } + private: + SmtEngine* d_smt; +}; /* class SoftResourceOutListener */ + + +class HardResourceOutListener : public Listener { + public: + HardResourceOutListener(SmtEngine& smt) : d_smt(&smt) {} + virtual void notify() { + SmtScope scope(d_smt); + theory::Rewriter::clearCaches(); + } + private: + SmtEngine* d_smt; +}; /* class HardResourceOutListener */ + + /** * This is an inelegant solution, but for the present, it will work. * The point of this is to separate the public and private portions of @@ -318,6 +345,16 @@ class SmtEnginePrivate : public NodeManagerListener { */ ResourceManager* d_resourceManager; + /** + * Listener for the when a soft resource out occurs. + */ + RegisterListener* d_softResourceOutListener; + + /** + * Listener for the when a hard resource out occurs. + */ + RegisterListener* d_hardResourceOutListener; + /** Learned literals */ vector d_nonClausalLearnedLiterals; @@ -465,6 +502,8 @@ public: SmtEnginePrivate(SmtEngine& smt) : d_smt(smt), d_resourceManager(NULL), + d_softResourceOutListener(NULL), + d_hardResourceOutListener(NULL), d_nonClausalLearnedLiterals(), d_realAssertionsEnd(0), d_booleanTermConverter(NULL), @@ -485,9 +524,23 @@ public: d_smt.d_nodeManager->subscribeEvents(this); d_true = NodeManager::currentNM()->mkConst(true); d_resourceManager = NodeManager::currentResourceManager(); + + d_softResourceOutListener = new RegisterListener( + d_resourceManager->getSoftListeners(), + new SoftResourceOutListener(d_smt)); + + d_hardResourceOutListener = new RegisterListener( + d_resourceManager->getHardListeners(), + new HardResourceOutListener(d_smt)); + } ~SmtEnginePrivate() throw() { + delete d_hardResourceOutListener; + d_hardResourceOutListener = NULL; + delete d_softResourceOutListener; + d_softResourceOutListener = NULL; + if(d_propagatorNeedsFinish) { d_propagator.finish(); d_propagatorNeedsFinish = false; @@ -733,7 +786,8 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_private = new smt::SmtEnginePrivate(*this); d_statisticsRegistry = new StatisticsRegistry(); d_stats = new SmtEngineStatistics(); - d_stats->d_resourceUnitsUsed.setData(d_private->getResourceManager()->d_cumulativeResourceUsed); + d_stats->d_resourceUnitsUsed.setData( + d_private->getResourceManager()->getResourceUsage()); // We have mutual dependency here, so we add the prop engine to the theory // engine later (it is non-essential there) d_theoryEngine = new TheoryEngine(d_context, d_userContext, diff --git a/src/smt/smt_options_handler.cpp b/src/smt/smt_options_handler.cpp index 147a53368..758ffaec8 100644 --- a/src/smt/smt_options_handler.cpp +++ b/src/smt/smt_options_handler.cpp @@ -28,7 +28,6 @@ #include "expr/expr_iomanip.h" #include "expr/metakind.h" #include "expr/node_manager.h" -#include "expr/resource_manager.h" #include "lib/strtok_r.h" #include "options/arith_heuristic_pivot_rule.h" #include "options/arith_propagation_mode.h" @@ -59,6 +58,7 @@ #include "theory/logic_info.h" #include "util/configuration.h" #include "util/configuration_private.h" +#include "util/resource_manager.h" #warning "TODO: Make SmtOptionsHandler non-public and refactor driver unified." diff --git a/src/theory/bv/bitblaster_template.h b/src/theory/bv/bitblaster_template.h index 7b071b9e9..ec76bb4f6 100644 --- a/src/theory/bv/bitblaster_template.h +++ b/src/theory/bv/bitblaster_template.h @@ -25,11 +25,11 @@ #include "bitblast_strategies_template.h" #include "context/cdhashmap.h" #include "expr/node.h" -#include "expr/resource_manager.h" #include "prop/sat_solver.h" #include "smt/smt_globals.h" #include "theory/theory_registrar.h" #include "theory/valuation.h" +#include "util/resource_manager.h" class Abc_Obj_t_; typedef Abc_Obj_t_ Abc_Obj_t; diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h index 2113ea66e..2491aef3a 100644 --- a/src/theory/output_channel.h +++ b/src/theory/output_channel.h @@ -20,9 +20,9 @@ #define __CVC4__THEORY__OUTPUT_CHANNEL_H #include "base/cvc4_assert.h" -#include "expr/resource_manager.h" #include "smt/logic_exception.h" #include "theory/interrupted.h" +#include "util/resource_manager.h" namespace CVC4 { namespace theory { diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp index 697736ebf..c98429dd2 100644 --- a/src/theory/rewriter.cpp +++ b/src/theory/rewriter.cpp @@ -17,12 +17,11 @@ #include "theory/rewriter.h" -#include "expr/resource_manager.h" #include "theory/theory.h" #include "smt/smt_engine_scope.h" #include "smt/smt_statistics_registry.h" #include "theory/rewriter_tables.h" - +#include "util/resource_manager.h" using namespace std; diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index bcc16c63a..25eac2ed4 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -23,7 +23,6 @@ #include "expr/attribute.h" #include "expr/node.h" #include "expr/node_builder.h" -#include "expr/resource_manager.h" #include "options/bv_options.h" #include "options/options.h" #include "options/quantifiers_options.h" @@ -46,6 +45,7 @@ #include "theory/theory_traits.h" #include "theory/uf/equality_engine.h" #include "theory/unconstrained_simplifier.h" +#include "util/resource_manager.h" using namespace std; diff --git a/src/util/Makefile.am b/src/util/Makefile.am index e1c593243..e95faea56 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -43,6 +43,8 @@ libutil_la_SOURCES = \ proof.h \ regexp.cpp \ regexp.h \ + resource_manager.cpp \ + resource_manager.h \ result.cpp \ result.h \ sexpr.cpp \ @@ -97,6 +99,7 @@ EXTRA_DIST = \ rational_gmp_imp.cpp \ rational_gmp_imp.h \ regexp.i \ + resource_manager.i \ result.i \ sexpr.i \ statistics.i \ diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp new file mode 100644 index 000000000..d426ab03e --- /dev/null +++ b/src/util/resource_manager.cpp @@ -0,0 +1,292 @@ +/********************* */ +/*! \file resource_manager.cpp +** \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 "util/resource_manager.h" + +#include "base/cvc4_assert.h" +#include "base/output.h" + +using namespace std; + +namespace CVC4 { + +void Timer::set(uint64_t millis, bool wallTime) { + d_ms = millis; + Trace("limit") << "Timer::set(" << d_ms << ")" << std::endl; + // keep track of when it was set, even if it's disabled (i.e. == 0) + d_wall_time = wallTime; + if (d_wall_time) { + // Wall time + gettimeofday(&d_wall_limit, NULL); + Trace("limit") << "Timer::set(): it's " << d_wall_limit.tv_sec << "," << d_wall_limit.tv_usec << std::endl; + d_wall_limit.tv_sec += millis / 1000; + d_wall_limit.tv_usec += (millis % 1000) * 1000; + if(d_wall_limit.tv_usec > 1000000) { + ++d_wall_limit.tv_sec; + d_wall_limit.tv_usec -= 1000000; + } + Trace("limit") << "Timer::set(): limit is at " << d_wall_limit.tv_sec << "," << d_wall_limit.tv_usec << std::endl; + } else { + // CPU time + d_cpu_start_time = ((double)clock())/(CLOCKS_PER_SEC *0.001); + d_cpu_limit = d_cpu_start_time + d_ms; + } +} + +/** Return the milliseconds elapsed since last set(). */ +uint64_t Timer::elapsedWall() const { + Assert (d_wall_time); + timeval tv; + gettimeofday(&tv, NULL); + Trace("limit") << "Timer::elapsedWallTime(): it's now " << tv.tv_sec << "," << tv.tv_usec << std::endl; + tv.tv_sec -= d_wall_limit.tv_sec - d_ms / 1000; + tv.tv_usec -= d_wall_limit.tv_usec - (d_ms % 1000) * 1000; + Trace("limit") << "Timer::elapsedWallTime(): elapsed time is " << tv.tv_sec << "," << tv.tv_usec << std::endl; + return tv.tv_sec * 1000 + tv.tv_usec / 1000; +} + +uint64_t Timer::elapsedCPU() const { + Assert (!d_wall_time); + clock_t elapsed = ((double)clock())/(CLOCKS_PER_SEC *0.001)- d_cpu_start_time; + Trace("limit") << "Timer::elapsedCPUTime(): elapsed time is " << elapsed << " ms" <= d_cpu_limit) { + Debug("limit") << "Timer::expired(): OVER LIMIT!" << current << std::endl; + return true; + } + return false; +} + +const uint64_t ResourceManager::s_resourceCount = 1000; + +ResourceManager::ResourceManager() + : d_cumulativeTimer() + , d_perCallTimer() + , d_timeBudgetCumulative(0) + , d_timeBudgetPerCall(0) + , d_resourceBudgetCumulative(0) + , d_resourceBudgetPerCall(0) + , d_cumulativeTimeUsed(0) + , d_cumulativeResourceUsed(0) + , d_thisCallResourceUsed(0) + , d_thisCallTimeBudget(0) + , d_thisCallResourceBudget(0) + , d_isHardLimit() + , d_on(false) + , d_cpuTime(false) + , d_spendResourceCalls(0) + , d_hardListeners() + , d_softListeners() +{} + + +void ResourceManager::setResourceLimit(uint64_t units, bool cumulative) { + d_on = true; + if(cumulative) { + Trace("limit") << "ResourceManager: setting cumulative resource limit to " << units << endl; + d_resourceBudgetCumulative = (units == 0) ? 0 : (d_cumulativeResourceUsed + units); + d_thisCallResourceBudget = d_resourceBudgetCumulative; + } else { + Trace("limit") << "ResourceManager: setting per-call resource limit to " << units << endl; + d_resourceBudgetPerCall = units; + } +} + +void ResourceManager::setTimeLimit(uint64_t millis, bool cumulative) { + d_on = true; + if(cumulative) { + Trace("limit") << "ResourceManager: setting cumulative time limit to " << millis << " ms" << endl; + d_timeBudgetCumulative = (millis == 0) ? 0 : (d_cumulativeTimeUsed + millis); + d_cumulativeTimer.set(millis, !d_cpuTime); + } else { + Trace("limit") << "ResourceManager: setting per-call time limit to " << millis << " ms" << endl; + d_timeBudgetPerCall = millis; + // perCall timer will be set in beginCall + } + +} + +const uint64_t& ResourceManager::getResourceUsage() const { + return d_cumulativeResourceUsed; +} + +uint64_t ResourceManager::getTimeUsage() const { + if (d_timeBudgetCumulative) { + return d_cumulativeTimer.elapsed(); + } + return d_cumulativeTimeUsed; +} + +uint64_t ResourceManager::getResourceRemaining() const { + if (d_thisCallResourceBudget <= d_thisCallResourceUsed) + return 0; + return d_thisCallResourceBudget - d_thisCallResourceUsed; +} + +uint64_t ResourceManager::getTimeRemaining() const { + uint64_t time_passed = d_cumulativeTimer.elapsed(); + if (time_passed >= d_thisCallTimeBudget) + return 0; + return d_thisCallTimeBudget - time_passed; +} + +void ResourceManager::spendResource(unsigned ammount) throw (UnsafeInterruptException) { + ++d_spendResourceCalls; + d_cumulativeResourceUsed += ammount; + if (!d_on) return; + + Debug("limit") << "ResourceManager::spendResource()" << std::endl; + d_thisCallResourceUsed += ammount; + if(out()) { + Trace("limit") << "ResourceManager::spendResource: interrupt!" << std::endl; + Trace("limit") << " on call " << d_spendResourceCalls << std::endl; + if (outOfTime()) { + Trace("limit") << "ResourceManager::spendResource: elapsed time" << d_cumulativeTimer.elapsed() << std::endl; + } + + if (d_isHardLimit) { + d_hardListeners.notify(); + throw UnsafeInterruptException(); + } else { + d_softListeners.notify(); + } + + } +} + +void ResourceManager::beginCall() { + + d_perCallTimer.set(d_timeBudgetPerCall, !d_cpuTime); + d_thisCallResourceUsed = 0; + if (!d_on) return; + + if (cumulativeLimitOn()) { + if (d_resourceBudgetCumulative) { + d_thisCallResourceBudget = d_resourceBudgetCumulative <= d_cumulativeResourceUsed ? 0 : + d_resourceBudgetCumulative - d_cumulativeResourceUsed; + } + + if (d_timeBudgetCumulative) { + + AlwaysAssert(d_cumulativeTimer.on()); + // timer was on since the option was set + d_cumulativeTimeUsed = d_cumulativeTimer.elapsed(); + d_thisCallTimeBudget = d_timeBudgetCumulative <= d_cumulativeTimeUsed? 0 : + d_timeBudgetCumulative - d_cumulativeTimeUsed; + d_cumulativeTimer.set(d_thisCallTimeBudget, d_cpuTime); + } + // we are out of resources so we shouldn't update the + // budget for this call to the per call budget + if (d_thisCallTimeBudget == 0 || + d_thisCallResourceUsed == 0) + return; + } + + if (perCallLimitOn()) { + // take min of what's left and per-call budget + if (d_resourceBudgetPerCall) { + d_thisCallResourceBudget = d_thisCallResourceBudget < d_resourceBudgetPerCall && d_thisCallResourceBudget != 0 ? d_thisCallResourceBudget : d_resourceBudgetPerCall; + } + + if (d_timeBudgetPerCall) { + d_thisCallTimeBudget = d_thisCallTimeBudget < d_timeBudgetPerCall && d_thisCallTimeBudget != 0 ? d_thisCallTimeBudget : d_timeBudgetPerCall; + } + } +} + +void ResourceManager::endCall() { + uint64_t usedInCall = d_perCallTimer.elapsed(); + d_perCallTimer.set(0); + d_cumulativeTimeUsed += usedInCall; +} + +bool ResourceManager::cumulativeLimitOn() const { + return d_timeBudgetCumulative || d_resourceBudgetCumulative; +} + +bool ResourceManager::perCallLimitOn() const { + return d_timeBudgetPerCall || d_resourceBudgetPerCall; +} + +bool ResourceManager::outOfResources() const { + // resource limiting not enabled + if (d_resourceBudgetPerCall == 0 && + d_resourceBudgetCumulative == 0) + return false; + + return getResourceRemaining() == 0; +} + +bool ResourceManager::outOfTime() const { + if (d_timeBudgetPerCall == 0 && + d_timeBudgetCumulative == 0) + return false; + + return d_cumulativeTimer.expired() || d_perCallTimer.expired(); +} + +void ResourceManager::useCPUTime(bool cpu) { + Trace("limit") << "ResourceManager::useCPUTime("<< cpu <<")\n"; + d_cpuTime = cpu; +} + +void ResourceManager::setHardLimit(bool value) { + Trace("limit") << "ResourceManager::setHardLimit("<< value <<")\n"; + d_isHardLimit = value; +} + +void ResourceManager::enable(bool on) { + Trace("limit") << "ResourceManager::enable("<< on <<")\n"; + d_on = on; +} + +ListenerCollection* ResourceManager::getHardListeners() { + return &d_hardListeners; +} + +ListenerCollection* ResourceManager::getSoftListeners() { + return &d_softListeners; +} + +} /* namespace CVC4 */ diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h new file mode 100644 index 000000000..2c54011a5 --- /dev/null +++ b/src/util/resource_manager.h @@ -0,0 +1,174 @@ +/********************* */ +/*! \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 +#include + +#include "base/exception.h" +#include "base/listener.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; + + /** Receives a notification on reaching a hard limit. */ + ListenerCollection d_hardListeners; + + /** Receives a notification on reaching a hard limit. */ + ListenerCollection d_softListeners; + +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; } + + /** Collection of listeners that are notified on a hard resource out. */ + ListenerCollection* getHardListeners(); + + /** Collection of listeners that are notified on a soft resource out. */ + ListenerCollection* getSoftListeners(); +};/* class ResourceManager */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__RESOURCE_MANAGER_H */ diff --git a/src/util/resource_manager.i b/src/util/resource_manager.i new file mode 100644 index 000000000..0f55c2bce --- /dev/null +++ b/src/util/resource_manager.i @@ -0,0 +1,5 @@ +%{ +#include "util/resource_manager.h" +%} + +%include "util/resource_manager.h" diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 36203725f..9d934a6e0 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -48,6 +48,7 @@ UNIT_TESTS += \ util/exception_black \ util/integer_black \ util/integer_white \ + util/listener_black \ util/rational_black \ util/rational_white \ util/stats_black \ diff --git a/test/unit/theory/theory_black.h b/test/unit/theory/theory_black.h index bafd572c3..fe8bebdbf 100644 --- a/test/unit/theory/theory_black.h +++ b/test/unit/theory/theory_black.h @@ -49,11 +49,14 @@ public: void setUp() { d_em = new ExprManager(); d_smt = new SmtEngine(d_em); - d_nm = NodeManager::fromExprManager(d_em); d_scope = new SmtScope(d_smt); + + d_nm = NodeManager::fromExprManager(d_em); } void tearDown() { + delete d_scope; + delete d_smt; delete d_em; } diff --git a/test/unit/util/listener_black.h b/test/unit/util/listener_black.h new file mode 100644 index 000000000..cd3a08d4e --- /dev/null +++ b/test/unit/util/listener_black.h @@ -0,0 +1,156 @@ +/********************* */ +/*! \file output_black.h + ** \verbatim + ** Original author: Morgan Deters + ** 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 Black box testing of CVC4 output classes. + ** + ** Black box testing of CVC4 output classes. + **/ + +#include +#include + +#include "base/listener.h" + +using namespace CVC4; +using namespace std; + +class ListenerBlack : public CxxTest::TestSuite { + + std::multiset d_events; + + class EventListener : public Listener { + public: + EventListener(std::multiset& events, std::string name) + : d_events(events), d_name(name) {} + ~EventListener(){} + + virtual void notify() { d_events.insert(d_name); } + + private: + std::multiset& d_events; + std::string d_name; + }; + +public: + + static std::multiset mkMultiset(std::string arr[], int len){ + return std::multiset(arr, arr + len); + } + + void setUp() { + d_events.clear(); + } + + void tearDown() { + d_events.clear(); + } + + void testEmptyCollection() { + // Makes an new collection and tests that it is empty. + ListenerCollection* collection = new ListenerCollection; + TS_ASSERT(collection->empty()); + TS_ASSERT_THROWS_NOTHING( delete collection ); + } + + void testSingletonCollection() { + ListenerCollection collection; + std::string expected[1] = {"a"}; + { + RegisterListener a(&collection, new EventListener(d_events, "a")); + collection.notify(); + TS_ASSERT(not collection.empty()); + } + TS_ASSERT(collection.empty()); + TS_ASSERT_EQUALS(d_events, mkMultiset(expected, 1)); + } + + void testSingleRegisterTearDown() { + // Tests that collection succeeds at destruction after + // registering a single event. + ListenerCollection* collection = new ListenerCollection; + { + RegisterListener a(collection, new EventListener(d_events, "a")); + TS_ASSERT(not collection->empty()); + // The destructor for a now runs. + } + TS_ASSERT(collection->empty()); + TS_ASSERT_THROWS_NOTHING( delete collection ); + } + + void testMultipleCollection() { + ListenerCollection* collection = new ListenerCollection; + { + RegisterListener c(collection, new EventListener(d_events, "c")); + collection->notify(); + // d_events == {"c"} + RegisterListener b(collection, new EventListener(d_events, "b")); + RegisterListener a(collection, new EventListener(d_events, "a")); + collection->notify(); + // d_events == {"a", "b", "c", "c"} + TS_ASSERT(not collection->empty()); + } + TS_ASSERT(collection->empty()); + std::string expected[4] = {"a", "b", "c", "c"}; + TS_ASSERT_EQUALS(d_events, mkMultiset(expected, 4)); + } + + void testRegisterMiddleTearDown() { + // Tests that collection succeeds at destruction after + // registering several events. + ListenerCollection* collection = new ListenerCollection; + { + RegisterListener a(collection, new EventListener(d_events, "a")); + RegisterListener* b = + new RegisterListener(collection, new EventListener(d_events, "b")); + RegisterListener c(collection, new EventListener(d_events, "c")); + + collection->notify(); + delete b; + collection->notify(); + // The destructor for a and c now run. + TS_ASSERT(not collection->empty()); + } + TS_ASSERT(collection->empty()); + TS_ASSERT_THROWS_NOTHING( delete collection ); + } + + + + void testRegisterMultiple() { + // This tests adds and notify multiple times. + ListenerCollection collection; + + std::vector listeners; + for(int i = 0; i < 4 ; ++i){ + stringstream ss; ss << i; + Listener* listener = new EventListener(d_events, ss.str()); + listeners.push_back(new RegisterListener(&collection, listener)); + collection.notify(); + } + + TS_ASSERT(not collection.empty()); + for(int i=0; i < listeners.size(); ++i){ + RegisterListener* at_i = listeners[i]; + delete at_i; + } + listeners.clear(); + TS_ASSERT(collection.empty()); + + std::string expected[10] = + {"0", "0", "0", "0", "1", "1", "1", "2", "2", "3"}; + TS_ASSERT_EQUALS(d_events, mkMultiset(expected, 10)); + + // No more events occur. + collection.notify(); + TS_ASSERT_EQUALS(d_events, mkMultiset(expected, 10)); + } + +};