Adding a new Listener utility class. Changing the ResourceManager to use Listeners for reporting hard and soft resource out() events.

4 files changed, 474 insertions, 0 deletions

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" <<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 */
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 <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 */
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"