added support for interrupting TheoryBV

3 files changed, 24 insertions, 5 deletions

diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index e13775ab2..0dd208088 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -46,6 +46,10 @@ private:
       toSatClause(clause, satClause);
       d_notify->notify(satClause);
     }
+
+    void safePoint() {
+      d_notify->safePoint(); 
+    }
   };
 
   BVMinisat::SimpSolver* d_minisat;
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 293ddd657..978ac8d7b 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -27,9 +27,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 #include "util/output.h"
 #include "util/utility.h"
-
+#include "util/exception.h"
 #include "theory/bv/options.h"
-
+#include "theory/interrupted.h"
 using namespace BVMinisat;
 
 namespace CVC4 {
@@ -794,13 +794,25 @@ lbool Solver::search(int nof_conflicts, UIP uip)
 
         }else{
             // NO CONFLICT
-            if (decisionLevel() > assumptions.size() && nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){
+            bool isWithinBudget;
+            try {
+              isWithinBudget = withinBudget(); 
+            }
+            catch (const CVC4::theory::Interrupted& e) {
+              // do some clean-up and rethrow 
+              cancelUntil(assumptions.size()); 
+              throw e; 
+            }
+            
+            if (decisionLevel() > assumptions.size() && nof_conflicts >= 0 && conflictC >= nof_conflicts ||
+                !isWithinBudget) {
                 // Reached bound on number of conflicts:
                 Debug("bvminisat::search") << OUTPUT_TAG << " restarting " << std::endl;
                 progress_estimate = progressEstimate();
                 cancelUntil(assumptions.size());
-                return l_Undef; }
-
+                return l_Undef;
+            }
+ 
             // Simplify the set of problem clauses:
             if (decisionLevel() == 0 && !simplify()) {
                 Debug("bvminisat::search") << OUTPUT_TAG << " base level conflict, we're unsat" << std::endl;
diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index b50ab632e..53d92ac39 100644
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -52,6 +52,7 @@ public:
    */
   virtual void notify(vec<Lit>& learnt) = 0;
 
+  virtual void safePoint() = 0;
 };
 
 //=================================================================================================
@@ -410,6 +411,8 @@ inline void     Solver::interrupt(){ asynch_interrupt = true; }
 inline void     Solver::clearInterrupt(){ asynch_interrupt = false; }
 inline void     Solver::budgetOff(){ conflict_budget = propagation_budget = -1; }
 inline bool     Solver::withinBudget() const {
+    Assert (notify); 
+    notify->safePoint(); 
     return !asynch_interrupt &&
            (conflict_budget    < 0 || conflicts < (uint64_t)conflict_budget) &&
            (propagation_budget < 0 || propagations < (uint64_t)propagation_budget); }