Fix a resource limiting issue where interruption didn't occur promptly. Thanks Johannes Kanig for the report.

8 files changed, 25 insertions, 14 deletions

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 498b31ce5..71b8eb69d 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -97,8 +97,9 @@ void BVMinisatSatSolver::markUnremovable(SatLiteral lit){
   d_minisat->setFrozen(BVMinisat::var(toMinisatLit(lit)), true);
 }
 
-void BVMinisatSatSolver::spendResource(){
-  // do nothing for the BV solver
+bool BVMinisatSatSolver::spendResource(){
+  // Do nothing for the BV solver.
+  return false;
 }
 
 void BVMinisatSatSolver::interrupt(){
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 04f21e761..c7ee2e0b7 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -87,7 +87,7 @@ public:
 
   void markUnremovable(SatLiteral lit);
 
-  void spendResource();
+  bool spendResource();
 
   void interrupt();
   
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 5403b992e..e5e28bb0b 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -815,7 +815,8 @@ CRef Solver::propagate(TheoryCheckType type)
     if (type == CHECK_FINAL) {
       // Do the theory check
       theoryCheck(CVC4::theory::Theory::EFFORT_FULL);
-      // Pick up the theory propagated literals (there could be some, if new lemmas are added)
+      // Pick up the theory propagated literals (there could be some,
+      // if new lemmas are added)
       propagateTheory();
       // If there are lemmas (or conflicts) update them
       if (lemmas.size() > 0) {
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 2d70cfeef..6d9fd538f 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -423,7 +423,9 @@ protected:
     int      intro_level      (Var x) const; // User level at which this variable was created
     int      trail_index      (Var x) const; // Index in the trail
     double   progressEstimate ()      const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
+public:
     bool     withinBudget     ()      const;
+protected:
 
     // Static helpers:
     //
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index b50c1c09f..99341455c 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -182,8 +182,9 @@ SatValue MinisatSatSolver::solve() {
   return toSatLiteralValue(d_minisat->solve());
 }
 
-void MinisatSatSolver::spendResource() {
+bool MinisatSatSolver::spendResource() {
   d_minisat->spendResource();
+  return !d_minisat->withinBudget();
 }
 
 void MinisatSatSolver::interrupt() {
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index 3992f1adb..3d3cea356 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -62,7 +62,7 @@ public:
   SatValue solve();
   SatValue solve(long unsigned int&);
 
-  void spendResource();
+  bool spendResource();
   void interrupt();
 
   SatValue value(SatLiteral l);
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 1572dfa88..a998d4240 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -79,14 +79,14 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext
 
   Debug("prop") << "Constructing the PropEngine" << endl;
 
-  d_satSolver = SatSolverFactory::createDPLLMinisat(); 
+  d_satSolver = SatSolverFactory::createDPLLMinisat();
 
   d_registrar = new theory::TheoryRegistrar(d_theoryEngine);
   d_cnfStream = new CVC4::prop::TseitinCnfStream
     (d_satSolver, d_registrar,
      userContext,
-     // fullLitToNode Map = 
-     options::threads() > 1 || 
+     // fullLitToNode Map =
+     options::threads() > 1 ||
      options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY
      );
 
@@ -95,7 +95,7 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext
 
   d_decisionEngine->setSatSolver(d_satSolver);
   d_decisionEngine->setCnfStream(d_cnfStream);
-  PROOF (ProofManager::currentPM()->initCnfProof(d_cnfStream); ); 
+  PROOF (ProofManager::currentPM()->initCnfProof(d_cnfStream); );
 }
 
 PropEngine::~PropEngine() {
@@ -279,12 +279,15 @@ void PropEngine::interrupt() throw(ModalException) {
 
   d_interrupted = true;
   d_satSolver->interrupt();
-  d_theoryEngine->interrupt(); 
+  d_theoryEngine->interrupt();
   Debug("prop") << "interrupt()" << endl;
 }
 
 void PropEngine::spendResource() throw() {
-  d_satSolver->spendResource();
+  if(d_satSolver->spendResource()) {
+    d_satSolver->interrupt();
+    d_theoryEngine->interrupt();
+  }
   checkTime();
 }
 
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index e3b0f3449..adf6dfd07 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -62,8 +62,11 @@ public:
   /** Check the satisfiability of the added clauses */
   virtual SatValue solve(long unsigned int&) = 0;
 
-  /** Instruct the solver that it should bump its consumed resource count. */
-  virtual void spendResource() = 0;
+  /**
+   * Instruct the solver that it should bump its consumed resource count.
+   * Returns true if resources are exhausted.
+   */
+  virtual bool spendResource() = 0;
 
   /** Interrupt the solver */
   virtual void interrupt() = 0;