Fix a resource limiting issue where interruption didn't occur promptly. Thanks Johan...

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 498b31ce58965de2acedc8ab3569734606bbd89a..71b8eb69de3e455189955aaec8b66d880a97461c 100644 (file)
--- 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 04f21e761b11e98aa465c92abf6ccdaa11cff73d..c7ee2e0b70838f11221d87cfd4691a82c05ed3a6 100644 (file)
--- 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 5403b992eb691109f663885207e488dea6666193..e5e28bb0b710c68e2c535b0f679082e108657f7d 100644 (file)
--- 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 2d70cfeef9a4b50b237333a33d74bbdb0ee90501..6d9fd538f59c5fb0dd2deaa1f2b905b15d0dc9ad 100644 (file)
--- 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 b50c1c09f6f3946e993529c87cfe1390b0933b05..99341455cce97a15b65adaf9c092abbd51bb3dcc 100644 (file)
--- 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 3992f1adbaee696549480f78ec805784fcee463b..3d3cea356a14263720868b3b2515383a3f31d839 100644 (file)
--- 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 1572dfa88d1569839e054bd5123b16dd203a7df5..a998d4240ce7e8af254d150dedf13b7aae35bf21 100644 (file)
--- 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 e3b0f34495b6f2631b6b1e5944d0fbb680cf9f06..adf6dfd073e03469cbe4326fe115a512e1db456e 100644 (file)
--- 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;

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index a4d7aaec12465cc770f89068bd42cdd6befb31a7..5bf285ae2f3ec392969e5ae0351a1b4f978e45ea 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -601,7 +601,7 @@ void QuantifiersEngine::addRequirePhase( Node lit, bool req ){
 
 bool QuantifiersEngine::addInstantiation( Node f, InstMatch& m, bool mkRep, bool modEq, bool modInst ){
   // For resource-limiting (also does a time check).
-  getOutputChannel().spendResource();
+  getOutputChannel().safePoint();
 
   std::vector< Node > terms;
   //make sure there are values for each variable we are instantiating