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

diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp
index 386fb5aad..5d53bf100 100644
--- a/src/prop/sat.cpp
+++ b/src/prop/sat.cpp
@@ -83,6 +83,7 @@ TNode SatSolver::getNode(SatLiteral lit) {
 }
 
 void SatSolver::notifyRestart() {
+  d_propEngine->checkTime();
   d_theoryEngine->notifyRestart();
 }
 
@@ -108,6 +109,9 @@ void SatSolver::logDecision(SatLiteral lit) {
 #endif /* CVC4_REPLAY */
 }
 
+void SatSolver::checkTime() {
+  d_propEngine->checkTime();
+}
 
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */