cvc4_assert.h \
exception.cpp \
exception.h \
+ listener.cpp \
+ listener.h \
modal_exception.h \
output.cpp \
output.h
--- /dev/null
+/********************* */
+/*! \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 <list>
+
+#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 */
--- /dev/null
+/********************* */
+/*! \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 <list>
+
+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<Listener*> 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 */
%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"
%include "expr/datatype.i"
%include "expr/predicate.i"
%include "expr/record.i"
-%include "expr/resource_manager.i"
%include "proof/unsat_core.i"
// TIM:
pickle_data.h \
pickler.cpp \
pickler.h \
- resource_manager.cpp \
- resource_manager.h \
symbol_table.cpp \
symbol_table.h \
type.cpp \
type.i \
kind.i \
expr.i \
- resource_manager.i \
record.i \
predicate.i \
variable_type_map.i \
#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;
+++ /dev/null
-/********************* */
-/*! \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" <<std::endl;
- return elapsed;
-}
-
-uint64_t Timer::elapsed() const {
- if (d_wall_time)
- return elapsedWall();
- return elapsedCPU();
-}
-
-bool Timer::expired() const {
- if (!on()) return false;
-
- if (d_wall_time) {
- timeval tv;
- gettimeofday(&tv, NULL);
- Debug("limit") << "Timer::expired(): current wall time is " << tv.tv_sec << "," << tv.tv_usec << std::endl;
- Debug("limit") << "Timer::expired(): limit wall time is " << d_wall_limit.tv_sec << "," << d_wall_limit.tv_usec << std::endl;
- if(d_wall_limit.tv_sec < tv.tv_sec ||
- (d_wall_limit.tv_sec == tv.tv_sec && d_wall_limit.tv_usec <= tv.tv_usec)) {
- Debug("limit") << "Timer::expired(): OVER LIMIT!" << std::endl;
- return true;
- }
- Debug("limit") << "Timer::expired(): within limit" << std::endl;
- return false;
- }
-
- // cpu time
- double current = ((double)clock())/(CLOCKS_PER_SEC*0.001);
- Debug("limit") << "Timer::expired(): current cpu time is " << current << std::endl;
- Debug("limit") << "Timer::expired(): limit cpu time is " << d_cpu_limit << std::endl;
- if (current >= 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 */
+++ /dev/null
-/********************* */
-/*! \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 "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 */
+++ /dev/null
-%{
-#include "expr/resource_manager.h"
-%}
-
-%include "expr/resource_manager.h"
#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;
#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"
#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;
#include <vector>
#include "base/exception.h"
+#include "base/listener.h"
#include "base/modal_exception.h"
#include "base/output.h"
#include "context/cdhashset.h"
#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"
#include "util/configuration_private.h"
#include "util/hash.h"
#include "util/proof.h"
+#include "util/resource_manager.h"
using namespace std;
using namespace CVC4;
}
};/* 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
*/
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<Node> d_nonClausalLearnedLiterals;
SmtEnginePrivate(SmtEngine& smt) :
d_smt(smt),
d_resourceManager(NULL),
+ d_softResourceOutListener(NULL),
+ d_hardResourceOutListener(NULL),
d_nonClausalLearnedLiterals(),
d_realAssertionsEnd(0),
d_booleanTermConverter(NULL),
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;
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,
#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"
#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."
#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;
#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 {
#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;
#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"
#include "theory/theory_traits.h"
#include "theory/uf/equality_engine.h"
#include "theory/unconstrained_simplifier.h"
+#include "util/resource_manager.h"
using namespace std;
proof.h \
regexp.cpp \
regexp.h \
+ resource_manager.cpp \
+ resource_manager.h \
result.cpp \
result.h \
sexpr.cpp \
rational_gmp_imp.cpp \
rational_gmp_imp.h \
regexp.i \
+ resource_manager.i \
result.i \
sexpr.i \
statistics.i \
--- /dev/null
+/********************* */
+/*! \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" <<std::endl;
+ return elapsed;
+}
+
+uint64_t Timer::elapsed() const {
+ if (d_wall_time)
+ return elapsedWall();
+ return elapsedCPU();
+}
+
+bool Timer::expired() const {
+ if (!on()) return false;
+
+ if (d_wall_time) {
+ timeval tv;
+ gettimeofday(&tv, NULL);
+ Debug("limit") << "Timer::expired(): current wall time is " << tv.tv_sec << "," << tv.tv_usec << std::endl;
+ Debug("limit") << "Timer::expired(): limit wall time is " << d_wall_limit.tv_sec << "," << d_wall_limit.tv_usec << std::endl;
+ if(d_wall_limit.tv_sec < tv.tv_sec ||
+ (d_wall_limit.tv_sec == tv.tv_sec && d_wall_limit.tv_usec <= tv.tv_usec)) {
+ Debug("limit") << "Timer::expired(): OVER LIMIT!" << std::endl;
+ return true;
+ }
+ Debug("limit") << "Timer::expired(): within limit" << std::endl;
+ return false;
+ }
+
+ // cpu time
+ double current = ((double)clock())/(CLOCKS_PER_SEC*0.001);
+ Debug("limit") << "Timer::expired(): current cpu time is " << current << std::endl;
+ Debug("limit") << "Timer::expired(): limit cpu time is " << d_cpu_limit << std::endl;
+ if (current >= 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 */
--- /dev/null
+/********************* */
+/*! \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 "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 */
--- /dev/null
+%{
+#include "util/resource_manager.h"
+%}
+
+%include "util/resource_manager.h"
util/exception_black \
util/integer_black \
util/integer_white \
+ util/listener_black \
util/rational_black \
util/rational_white \
util/stats_black \
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;
}
--- /dev/null
+/********************* */
+/*! \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 <cxxtest/TestSuite.h>
+#include <sstream>
+
+#include "base/listener.h"
+
+using namespace CVC4;
+using namespace std;
+
+class ListenerBlack : public CxxTest::TestSuite {
+
+ std::multiset<std::string> d_events;
+
+ class EventListener : public Listener {
+ public:
+ EventListener(std::multiset<std::string>& events, std::string name)
+ : d_events(events), d_name(name) {}
+ ~EventListener(){}
+
+ virtual void notify() { d_events.insert(d_name); }
+
+ private:
+ std::multiset<std::string>& d_events;
+ std::string d_name;
+ };
+
+public:
+
+ static std::multiset<std::string> mkMultiset(std::string arr[], int len){
+ return std::multiset<std::string>(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<RegisterListener*> 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));
+ }
+
+};
projects / cvc5.git / commitdiff