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, 13 insertions, 1 deletions

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) {