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.

4 files changed, 59 insertions, 9 deletions

diff --git a/src/theory/bv/theory_bv_rewrite_rules_core.h b/src/theory/bv/theory_bv_rewrite_rules_core.h
index 941b9d0b4..851a6893c 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_core.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_core.h
@@ -277,7 +277,7 @@ bool RewriteRule<ReflexivityEq>::applies(Node node) {
 template<>
 Node RewriteRule<ReflexivityEq>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<ReflexivityEq>(" << node << ")" << std::endl;
-  return node[1].eqNode(node[0]);;
+  return node[1].eqNode(node[0]);
 }
 
 }
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index f5bf620bf..625abc580 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -105,6 +105,20 @@ public:
    */
   virtual void setIncomplete() throw(AssertionException) = 0;
 
+  /**
+   * "Spend" a "resource."  The meaning is specific to the context in
+   * which the theory is operating, and may even be ignored.  The
+   * intended meaning is that if the user has set a limit on the "units
+   * of resource" that can be expended in a search, and that limit is
+   * exceeded, then the search is terminated.  Note that the check for
+   * termination occurs in the main search loop, so while theories
+   * should call OutputChannel::spendResource() during particularly
+   * long-running operations, they cannot rely on resource() to break
+   * out of infinite or intractable computations.
+   */
+  virtual void spendResource() throw() {
+  }
+
 };/* class OutputChannel */
 
 }/* CVC4::theory namespace */
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 2d4672776..2cd3f4d72 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -100,6 +100,8 @@ void TheoryEngine::preRegister(TNode preprocessed) {
  */
 void TheoryEngine::check(Theory::Effort effort) {
 
+  d_propEngine->checkTime();
+
 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 #endif
@@ -263,20 +265,38 @@ bool TheoryEngine::properConflict(TNode conflict) const {
   bool value;
   if (conflict.getKind() == kind::AND) {
     for (unsigned i = 0; i < conflict.getNumChildren(); ++ i) {
-      if (!getPropEngine()->hasValue(conflict[i], value)) return false;
-      if (!value) return false;
+      if (! getPropEngine()->hasValue(conflict[i], value)) {
+        Debug("properConflict") << "Bad conflict is due to unassigned atom: "
+                                << conflict[i] << endl;
+        return false;
+      }
+      if (! value) {
+        Debug("properConflict") << "Bad conflict is due to false atom: "
+                                << conflict[i] << endl;
+        return false;
+      }
     }
   } else {
-    if (!getPropEngine()->hasValue(conflict, value)) return false;
-    return value;
+    if (! getPropEngine()->hasValue(conflict, value)) {
+      Debug("properConflict") << "Bad conflict is due to unassigned atom: "
+                              << conflict << endl;
+      return false;
+    }
+    if(! value) {
+      Debug("properConflict") << "Bad conflict is due to false atom: "
+                              << conflict << endl;
+      return false;
+    }
   }
   return true;
 }
 
 bool TheoryEngine::properPropagation(TNode lit) const {
-  Assert(!lit.isNull());
-#warning implement TheoryEngine::properPropagation()
-  return true;
+  if(!getPropEngine()->isTranslatedSatLiteral(lit)) {
+    return false;
+  }
+  bool b;
+  return !getPropEngine()->hasValue(lit, b);
 }
 
 bool TheoryEngine::properExplanation(TNode node, TNode expl) const {
@@ -471,6 +491,8 @@ void TheoryEngine::assertFact(TNode node)
 {
   Trace("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl;
 
+  d_propEngine->checkTime();
+
   // Get the atom
   TNode atom = node.getKind() == kind::NOT ? node[0] : node;
 
@@ -497,6 +519,8 @@ void TheoryEngine::assertFact(TNode node)
 void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
       
   Debug("theory") << "EngineOutputChannel::propagate(" << literal << ")" << std::endl;
+
+  d_propEngine->checkTime();
       
   if(Dump.isOn("t-propagations")) {
     Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid") << std::endl
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 915373074..be3068a45 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -209,6 +209,11 @@ class TheoryEngine {
     void setIncomplete() throw(AssertionException) {
       d_engine->setIncomplete(d_theory);
     }
+
+    void spendResource() throw() {
+      d_engine->spendResource();
+    }
+
   };/* class EngineOutputChannel */
 
   /**
@@ -223,7 +228,7 @@ class TheoryEngine {
 
   void conflict(TNode conflict) {
 
-    Assert(properConflict(conflict));
+    Assert(properConflict(conflict), "not a proper conflict: %s", conflict.toString().c_str());
 
     // Mark that we are in conflict
     d_inConflict = true;
@@ -257,6 +262,13 @@ class TheoryEngine {
   }
 
   /**
+   * "Spend" a resource during a search or preprocessing.
+   */
+  void spendResource() throw() {
+    d_propEngine->spendResource();
+  }
+
+  /**
    * Is the theory active.
    */
   bool isActive(theory::TheoryId theory) {