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.

1 files changed, 137 insertions, 9 deletions

diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 16cb34e04..25697b856 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -26,6 +26,9 @@
 #include "expr/node.h"
 #include "util/options.h"
 #include "util/result.h"
+#include "smt/modal_exception.h"
+
+#include <sys/time.h>
 
 namespace CVC4 {
 
@@ -36,6 +39,80 @@ namespace prop {
 class CnfStream;
 class SatSolver;
 
+class PropEngine;
+
+/**
+ * A helper class to keep track of a time budget and signal
+ * the PropEngine when the budget expires.
+ */
+class SatTimer {
+
+  PropEngine& d_propEngine;
+  unsigned long d_ms;
+  timeval d_limit;
+
+public:
+
+  /** Construct a SatTimer attached to the given PropEngine. */
+  SatTimer(PropEngine& propEngine) :
+    d_propEngine(propEngine),
+    d_ms(0) {
+  }
+
+  /** Is the timer currently active? */
+  bool on() const {
+    return d_ms != 0;
+  }
+
+  /** Set a millisecond timer (0==off). */
+  void set(unsigned long millis) {
+    d_ms = millis;
+    // keep track of when it was set, even if it's disabled (i.e. == 0)
+    Trace("limit") << "SatTimer::set(" << d_ms << ")" << std::endl;
+    gettimeofday(&d_limit, NULL);
+    Trace("limit") << "SatTimer::set(): it's " << d_limit.tv_sec << "," << d_limit.tv_usec << std::endl;
+    d_limit.tv_sec += millis / 1000;
+    d_limit.tv_usec += (millis % 1000) * 1000;
+    if(d_limit.tv_usec > 1000000) {
+      ++d_limit.tv_sec;
+      d_limit.tv_usec -= 1000000;
+    }
+    Trace("limit") << "SatTimer::set(): limit is at " << d_limit.tv_sec << "," << d_limit.tv_usec << std::endl;
+  }
+
+  /** Return the milliseconds elapsed since last set(). */
+  unsigned long elapsed() {
+    timeval tv;
+    gettimeofday(&tv, NULL);
+    Trace("limit") << "SatTimer::elapsed(): it's now " << tv.tv_sec << "," << tv.tv_usec << std::endl;
+    tv.tv_sec -= d_limit.tv_sec - d_ms / 1000;
+    tv.tv_usec -= d_limit.tv_usec - (d_ms % 1000) * 1000;
+    Trace("limit") << "SatTimer::elapsed(): elapsed time is " << tv.tv_sec << "," << tv.tv_usec << std::endl;
+    return tv.tv_sec * 1000 + tv.tv_usec / 1000;
+  }
+
+  bool expired() {
+    if(on()) {
+      timeval tv;
+      gettimeofday(&tv, NULL);
+      Trace("limit") << "SatTimer::expired(): current time is " << tv.tv_sec << "," << tv.tv_usec << std::endl;
+      Trace("limit") << "SatTimer::expired(): limit time is " << d_limit.tv_sec << "," << d_limit.tv_usec << std::endl;
+      if(d_limit.tv_sec < tv.tv_sec ||
+         (d_limit.tv_sec == tv.tv_sec && d_limit.tv_usec <= tv.tv_usec)) {
+        Trace("limit") << "SatTimer::expired(): OVER LIMIT!" << std::endl;
+        return true;
+      } else {
+        Trace("limit") << "SatTimer::expired(): within limit" << std::endl;
+      }
+    }
+    return false;
+  }
+
+  /** Check the current time and signal the PropEngine if over-time. */
+  void check();
+
+};/* class SatTimer */
+
 /**
  * PropEngine is the abstraction of a Sat Solver, providing methods for
  * solving the SAT problem and conversion to CNF (via the CnfStream).
@@ -43,7 +120,7 @@ class SatSolver;
 class PropEngine {
 
   /**
-   * Indicates that the sat solver is currently solving something and we should
+   * Indicates that the SAT solver is currently solving something and we should
    * not mess with it's internal state.
    */
   bool d_inCheckSat;
@@ -51,6 +128,7 @@ class PropEngine {
   /** The theory engine we will be using */
   TheoryEngine *d_theoryEngine;
 
+  /** The context */
   context::Context* d_context;
 
   /** The SAT solver proxy */
@@ -62,6 +140,13 @@ class PropEngine {
   /** The CNF converter in use */
   CnfStream* d_cnfStream;
 
+  /** A timer for SAT calls */
+  SatTimer d_satTimer;
+
+  /** Whether we were just interrupted (or not) */
+  bool d_interrupted;
+
+  /** Dump out the satisfying assignment (after SAT result) */
   void printSatisfyingAssignment();
 
 public:
@@ -86,27 +171,34 @@ public:
   void shutdown() { }
 
   /**
-   * Converts the given formula to CNF and assert the CNF to the sat solver.
+   * Converts the given formula to CNF and assert the CNF to the SAT solver.
    * The formula is asserted permanently for the current context.
    * @param node the formula to assert
    */
   void assertFormula(TNode node);
 
   /**
-   * Converts the given formula to CNF and assert the CNF to the sat solver.
-   * The formula can be removed by the sat solver after backtracking lower
+   * Converts the given formula to CNF and assert the CNF to the SAT solver.
+   * The formula can be removed by the SAT solver after backtracking lower
    * than the (SAT and SMT) level at which it was asserted.
    *
    * @param node the formula to assert
-   * @param negated whether the node should be considered to be negated at the top level (or not)
-   * @param removable whether this lemma can be quietly removed based on an activity heuristic (or not)
+   * @param negated whether the node should be considered to be negated
+   * at the top level (or not)
+   * @param removable whether this lemma can be quietly removed based
+   * on an activity heuristic (or not)
    */
   void assertLemma(TNode node, bool negated, bool removable);
 
   /**
    * Checks the current context for satisfiability.
+   *
+   * @param millis the time limit for this call in milliseconds
+   * (0==off); on output, it is set to the milliseconds used
+   * @param on input, resource the number of resource units permitted
+   * for this call (0==off); on output, it is set to the resource used
    */
-  Result checkSat();
+  Result checkSat(unsigned long& millis, unsigned long& resource);
 
   /**
    * Get the value of a boolean variable.
@@ -116,12 +208,19 @@ public:
    */
   Node getValue(TNode node);
 
-  /*
-   * Return true if node has an associated SAT literal
+  /**
+   * Return true if node has an associated SAT literal.
    */
   bool isSatLiteral(TNode node);
 
   /**
+   * Return true if node has an associated SAT literal that is
+   * currently translated (i.e., it's relevant to the current
+   * user push/pop level).
+   */
+  bool isTranslatedSatLiteral(TNode node);
+
+  /**
    * Check if the node has a value and return it if yes.
    */
   bool hasValue(TNode node, bool& value);
@@ -143,8 +242,37 @@ public:
    */
   void pop();
 
+  /**
+   * Check the current time budget.
+   */
+  void checkTime();
+
+  /**
+   * Interrupt a running solver (cause a timeout).
+   */
+  void interrupt() throw(ModalException);
+
+  /**
+   * "Spend" a "resource."  If the sum of these externally-counted
+   * resources and SAT-internal resources exceed the current limit,
+   * SAT should terminate.
+   */
+  void spendResource() throw();
+
 };/* class PropEngine */
 
+
+inline void SatTimer::check() {
+  if(expired()) {
+    Trace("limit") << "SatTimer::check(): interrupt!" << std::endl;
+    d_propEngine.interrupt();
+  }
+}
+
+inline void PropEngine::checkTime() {
+  d_satTimer.check();
+}
+
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */