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

5 files changed, 1 insertions, 459 deletions

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