1 files changed, 27 insertions, 2 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 932f11f74..0db71aba4 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -71,6 +71,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_propagatedLiterals(context),
   d_propagatedLiteralsIndex(context, 0),
   d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
+  d_interrupted(false),
   d_inPreregister(false),
   d_factsAsserted(context, false),
   d_preRegistrationVisitor(this, context),
@@ -113,6 +114,10 @@ TheoryEngine::~TheoryEngine() {
   StatisticsRegistry::unregisterStat(&d_combineTheoriesTime);
 }
 
+void TheoryEngine::interrupt() throw(ModalException) {
+  d_interrupted = true;
+}
+
 void TheoryEngine::preRegister(TNode preprocessed) {
 
   if(Dump.isOn("missed-t-propagations")) {
@@ -282,6 +287,9 @@ void TheoryEngine::check(Theory::Effort effort) {
 
   d_propEngine->checkTime();
 
+  // Reset the interrupt flag
+  d_interrupted = false; 
+
 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 #endif
@@ -293,7 +301,6 @@ void TheoryEngine::check(Theory::Effort effort) {
        } \
     }
 
-
   // Do the checking
   try {
 
@@ -455,6 +462,9 @@ void TheoryEngine::combineTheories() {
 }
 
 void TheoryEngine::propagate(Theory::Effort effort) {
+  // Reset the interrupt flag
+  d_interrupted = false; 
+
   // Definition of the statement that is to be run by every theory
 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
@@ -464,6 +474,9 @@ void TheoryEngine::propagate(Theory::Effort effort) {
     theoryOf(THEORY)->propagate(effort); \
   }
 
+  // Reset the interrupt flag
+  d_interrupted = false; 
+
   // Propagate for each theory using the statement above
   CVC4_FOR_EACH_THEORY;
 
@@ -592,6 +605,8 @@ TheoryModel* TheoryEngine::getModel() {
 }
 
 bool TheoryEngine::presolve() {
+  // Reset the interrupt flag
+  d_interrupted = false; 
 
   try {
     // Definition of the statement that is to be run by every theory
@@ -599,7 +614,7 @@ bool TheoryEngine::presolve() {
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
 #endif
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
-    if (theory::TheoryTraits<THEORY>::hasPresolve) { \
+    if (theory::TheoryTraits<THEORY>::hasPresolve) {    \
       theoryOf(THEORY)->presolve(); \
       if(d_inConflict) { \
         return true; \
@@ -616,6 +631,8 @@ bool TheoryEngine::presolve() {
 }/* TheoryEngine::presolve() */
 
 void TheoryEngine::postsolve() {
+  // Reset the interrupt flag
+  d_interrupted = false; 
 
   try {
     // Definition of the statement that is to be run by every theory
@@ -637,6 +654,9 @@ void TheoryEngine::postsolve() {
 
 
 void TheoryEngine::notifyRestart() {
+  // Reset the interrupt flag
+  d_interrupted = false; 
+
   // Definition of the statement that is to be run by every theory
 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
 #undef CVC4_FOR_EACH_THEORY_STATEMENT
@@ -651,6 +671,8 @@ void TheoryEngine::notifyRestart() {
 }
 
 void TheoryEngine::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
+  // Reset the interrupt flag
+  d_interrupted = false; 
 
   // Definition of the statement that is to be run by every theory
 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
@@ -683,6 +705,9 @@ void TheoryEngine::shutdown() {
 }
 
 theory::Theory::PPAssertStatus TheoryEngine::solve(TNode literal, SubstitutionMap& substitutionOut) {
+  // Reset the interrupt flag
+  d_interrupted = false; 
+
   TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
   Trace("theory::solve") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl;