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, 14 insertions, 0 deletions

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