Interruption, time-out, and deterministic time-out ("resource-out") features.

Details here: http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_October_14,_2011#Resource.2Ftime_limiting_API
This will need more work, but it's a start.

Also implemented TheoryEngine::properPropagation().

Other minor things.

2 files changed, 229 insertions, 8 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f80d9a135..ecd61c0b4 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -180,9 +180,25 @@ using namespace CVC4::smt;
 
 SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_context(em->getContext()),
+  d_userLevels(),
   d_userContext(new UserContext()),
   d_exprManager(em),
   d_nodeManager(d_exprManager->getNodeManager()),
+  d_theoryEngine(NULL),
+  d_propEngine(NULL),
+  d_definedFunctions(NULL),
+  d_assertionList(NULL),
+  d_assignments(NULL),
+  d_logic(""),
+  d_problemExtended(false),
+  d_queryMade(false),
+  d_timeBudgetCumulative(0),
+  d_timeBudgetPerCall(0),
+  d_resourceBudgetCumulative(0),
+  d_resourceBudgetPerCall(0),
+  d_cumulativeTimeUsed(0),
+  d_cumulativeResourceUsed(0),
+  d_status(),
   d_private(new smt::SmtEnginePrivate(*this)),
   d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
   d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"),
@@ -212,14 +228,22 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
 
   d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
 
-  d_assertionList = NULL;
   if(Options::current()->interactive) {
     d_assertionList = new(true) AssertionList(d_userContext);
   }
 
-  d_assignments = NULL;
-  d_problemExtended = false;
-  d_queryMade = false;
+  if(Options::current()->perCallResourceLimit != 0) {
+    setResourceLimit(Options::current()->perCallResourceLimit, false);
+  }
+  if(Options::current()->cumulativeResourceLimit != 0) {
+    setResourceLimit(Options::current()->cumulativeResourceLimit, true);
+  }
+  if(Options::current()->perCallMillisecondLimit != 0) {
+    setTimeLimit(Options::current()->perCallMillisecondLimit, false);
+  }
+  if(Options::current()->cumulativeMillisecondLimit != 0) {
+    setTimeLimit(Options::current()->cumulativeMillisecondLimit, true);
+  }
 }
 
 void SmtEngine::shutdown() {
@@ -719,12 +743,44 @@ void SmtEnginePrivate::simplifyAssertions()
 Result SmtEngine::check() {
   Trace("smt") << "SmtEngine::check()" << endl;
 
-  // make sure the prop layer has all assertions
-  Trace("smt") << "SmtEngine::check(): processing assertion" << endl;
+  // Make sure the prop layer has all of the assertions
+  Trace("smt") << "SmtEngine::check(): processing assertions" << endl;
   d_private->processAssertions();
 
+  unsigned long millis = 0;
+  if(d_timeBudgetCumulative != 0) {
+    millis = getTimeRemaining();
+    if(millis == 0) {
+      return Result(Result::VALIDITY_UNKNOWN, Result::TIMEOUT);
+    }
+  }
+  if(d_timeBudgetPerCall != 0 && (millis == 0 || d_timeBudgetPerCall < millis)) {
+    millis = d_timeBudgetPerCall;
+  }
+
+  unsigned long resource = 0;
+  if(d_resourceBudgetCumulative != 0) {
+    resource = getResourceRemaining();
+    if(resource == 0) {
+      return Result(Result::VALIDITY_UNKNOWN, Result::RESOURCEOUT);
+    }
+  }
+  if(d_resourceBudgetPerCall != 0 && (resource == 0 || d_resourceBudgetPerCall < resource)) {
+    resource = d_resourceBudgetPerCall;
+  }
+
   Trace("smt") << "SmtEngine::check(): running check" << endl;
-  return d_propEngine->checkSat();
+  Result result = d_propEngine->checkSat(millis, resource);
+
+  // PropEngine::checkSat() returns the actual amount used in these
+  // variables.
+  d_cumulativeTimeUsed += millis;
+  d_cumulativeResourceUsed += resource;
+
+  Trace("limit") << "SmtEngine::check(): cumulative millis " << d_cumulativeTimeUsed
+                 << ", conflicts " << d_cumulativeResourceUsed << std::endl;
+
+  return result;
 }
 
 Result SmtEngine::quickCheck() {
@@ -1082,6 +1138,9 @@ void SmtEngine::pop() {
   if(!Options::current()->incrementalSolving) {
     throw ModalException("Cannot pop when not solving incrementally (use --incremental)");
   }
+  if(d_userContext->getLevel() == 0) {
+    throw ModalException("Cannot pop beyond the first user frame");
+  }
   AlwaysAssert(d_userLevels.size() > 0 && d_userLevels.back() < d_userContext->getLevel());
   while (d_userLevels.back() < d_userContext->getLevel()) {
     internalPop();
@@ -1113,6 +1172,56 @@ void SmtEngine::internalPop() {
   }
 }
 
+void SmtEngine::interrupt() throw(ModalException) {
+  d_propEngine->interrupt();
+}
+
+void SmtEngine::setResourceLimit(unsigned long units, bool cumulative) {
+  if(cumulative) {
+    Trace("limit") << "SmtEngine: setting cumulative resource limit to " << units << std::endl;
+    d_resourceBudgetCumulative = (units == 0) ? 0 : (d_cumulativeResourceUsed + units);
+  } else {
+    Trace("limit") << "SmtEngine: setting per-call resource limit to " << units << std::endl;
+    d_resourceBudgetPerCall = units;
+  }
+}
+
+void SmtEngine::setTimeLimit(unsigned long millis, bool cumulative) {
+  if(cumulative) {
+    Trace("limit") << "SmtEngine: setting cumulative time limit to " << millis << " ms" << std::endl;
+    d_timeBudgetCumulative = (millis == 0) ? 0 : (d_cumulativeTimeUsed + millis);
+  } else {
+    Trace("limit") << "SmtEngine: setting per-call time limit to " << millis << " ms" << std::endl;
+    d_timeBudgetPerCall = millis;
+  }
+}
+
+unsigned long SmtEngine::getResourceUsage() const {
+  return d_cumulativeResourceUsed;
+}
+
+unsigned long SmtEngine::getTimeUsage() const {
+  return d_cumulativeTimeUsed;
+}
+
+unsigned long SmtEngine::getResourceRemaining() const throw(ModalException) {
+  if(d_resourceBudgetCumulative == 0) {
+    throw ModalException("No cumulative resource limit is currently set");
+  }
+
+  return d_resourceBudgetCumulative <= d_cumulativeResourceUsed ? 0 :
+    d_resourceBudgetCumulative - d_cumulativeResourceUsed;
+}
+
+unsigned long SmtEngine::getTimeRemaining() const throw(ModalException) {
+  if(d_timeBudgetCumulative == 0) {
+    throw ModalException("No cumulative time limit is currently set");
+  }
+
+  return d_timeBudgetCumulative <= d_cumulativeTimeUsed ? 0 :
+    d_timeBudgetCumulative - d_cumulativeTimeUsed;
+}
+
 StatisticsRegistry* SmtEngine::getStatisticsRegistry() const {
   return d_exprManager->d_nodeManager->getStatisticsRegistry();
 }
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index f5036bed7..f898ee76a 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -104,7 +104,7 @@ class CVC4_PUBLIC SmtEngine {
 
   /** Our expression manager */
   ExprManager* d_exprManager;
-  /** Out internal expression/node manager */
+  /** Our internal expression/node manager */
   NodeManager* d_nodeManager;
   /** The decision engine */
   TheoryEngine* d_theoryEngine;
@@ -143,6 +143,20 @@ class CVC4_PUBLIC SmtEngine {
    */
   bool d_queryMade;
 
+  /** A user-imposed cumulative time budget, in milliseconds.  0 = no limit. */
+  unsigned long d_timeBudgetCumulative;
+  /** A user-imposed per-call time budget, in milliseconds.  0 = no limit. */
+  unsigned long d_timeBudgetPerCall;
+  /** A user-imposed cumulative resource budget.  0 = no limit. */
+  unsigned long d_resourceBudgetCumulative;
+  /** A user-imposed per-call resource budget.  0 = no limit. */
+  unsigned long d_resourceBudgetPerCall;
+
+  /** The number of milliseconds used by this SmtEngine since its inception. */
+  unsigned long d_cumulativeTimeUsed;
+  /** The amount of resource used by this SmtEngine since its inception. */
+  unsigned long d_cumulativeResourceUsed;
+
   /**
    * Most recent result of last checkSat/query or (set-info :status).
    */
@@ -324,6 +338,104 @@ public:
   void pop();
 
   /**
+   * Interrupt a running query.  This can be called from another thread
+   * or from a signal handler.  Throws a ModalException if the SmtEngine
+   * isn't currently in a query.
+   */
+  void interrupt() throw(ModalException);
+
+  /**
+   * Set a resource limit for SmtEngine operations.  This is like a time
+   * limit, but it's deterministic so that reproducible results can be
+   * obtained.  However, please note that it may not be deterministic
+   * between different versions of CVC4, or even the same version on
+   * different platforms.
+   *
+   * A cumulative and non-cumulative (per-call) resource limit can be
+   * set at the same time.  A call to setResourceLimit() with
+   * cumulative==true replaces any cumulative resource limit currently
+   * in effect; a call with cumulative==false replaces any per-call
+   * resource limit currently in effect.  Time limits can be set in
+   * addition to resource limits; the SmtEngine obeys both.  That means
+   * that up to four independent limits can control the SmtEngine
+   * at the same time.
+   *
+   * When an SmtEngine is first created, it has no time or resource
+   * limits.
+   *
+   * Currently, these limits only cause the SmtEngine to stop what its
+   * doing when the limit expires (or very shortly thereafter); no
+   * heuristics are altered by the limits or the threat of them expiring.
+   * We reserve the right to change this in the future.
+   *
+   * @param units the resource limit, or 0 for no limit
+   * @param cumulative whether this resource limit is to be a cumulative
+   * resource limit for all remaining calls into the SmtEngine (true), or
+   * whether it's a per-call resource limit (false); the default is false
+   */
+  void setResourceLimit(unsigned long units, bool cumulative = false);
+
+  /**
+   * Set a time limit for SmtEngine operations.
+   *
+   * A cumulative and non-cumulative (per-call) time limit can be
+   * set at the same time.  A call to setTimeLimit() with
+   * cumulative==true replaces any cumulative time limit currently
+   * in effect; a call with cumulative==false replaces any per-call
+   * time limit currently in effect.  Resource limits can be set in
+   * addition to time limits; the SmtEngine obeys both.  That means
+   * that up to four independent limits can control the SmtEngine
+   * at the same time.
+   *
+   * Note that the cumulative timer only ticks away when one of the
+   * SmtEngine's workhorse functions (things like assertFormula(),
+   * query(), checkSat(), and simplify()) are running.  Between calls,
+   * the timer is still.
+   *
+   * When an SmtEngine is first created, it has no time or resource
+   * limits.
+   *
+   * Currently, these limits only cause the SmtEngine to stop what its
+   * doing when the limit expires (or very shortly thereafter); no
+   * heuristics are altered by the limits or the threat of them expiring.
+   * We reserve the right to change this in the future.
+   *
+   * @param millis the time limit in milliseconds, or 0 for no limit
+   * @param cumulative whether this time limit is to be a cumulative
+   * time limit for all remaining calls into the SmtEngine (true), or
+   * whether it's a per-call time limit (false); the default is false
+   */
+  void setTimeLimit(unsigned long millis, bool cumulative = false);
+
+  /**
+   * Get the current resource usage count for this SmtEngine.  This
+   * function can be used to ascertain reasonable values to pass as
+   * resource limits to setResourceLimit().
+   */
+  unsigned long getResourceUsage() const;
+
+  /**
+   * Get the current millisecond count for this SmtEngine.
+   */
+  unsigned long getTimeUsage() const;
+
+  /**
+   * Get the remaining resources that can be consumed by this SmtEngine
+   * according to the currently-set cumulative resource limit.  If there
+   * is not a cumulative resource limit set, this function throws a
+   * ModalException.
+   */
+  unsigned long getResourceRemaining() const throw(ModalException);
+
+  /**
+   * Get the remaining number of milliseconds that can be consumed by
+   * this SmtEngine according to the currently-set cumulative time limit.
+   * If there is not a cumulative resource limit set, this function
+   * throws a ModalException.
+   */
+  unsigned long getTimeRemaining() const throw(ModalException);
+
+  /**
    * Permit access to the underlying StatisticsRegistry.
    */
   StatisticsRegistry* getStatisticsRegistry() const;