Better support for resource-limiting when there aren't any actual conflicts.

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 7322cd0faa547f9827b61f5106d9194f3ca6bc95..2121d73667826f7017a580ce428c6f970cccd41f 100644 (file)
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -97,6 +97,10 @@ void BVMinisatSatSolver::markUnremovable(SatLiteral lit){
   d_minisat->setFrozen(BVMinisat::var(toMinisatLit(lit)), true);
 }
 
+void BVMinisatSatSolver::spendResource(){
+  // do nothing for the BV solver
+}
+
 void BVMinisatSatSolver::interrupt(){
   d_minisat->interrupt();
 }

diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index f9d0fbd6a50f748b235acaaedd3e9b6b27bde0d8..0101c5d6270952b071b759534c5f8628c692c241 100644 (file)
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -87,6 +87,8 @@ public:
 
   void markUnremovable(SatLiteral lit);
 
+  void spendResource();
+
   void interrupt();
   
   SatValue solve();

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 610023b70387e480c4b86cffff50c7479d33d30e..b0d710d6601161be82b12f1f62bdccce6d86d280 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -106,7 +106,7 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context,
 
     // Statistics: (formerly in 'SolverStats')
     //
-  , solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0)
+  , solves(0), starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0), resources_consumed(0)
   , dec_vars(0), clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)
 
   , ok                 (true)
@@ -1588,6 +1588,9 @@ CRef Solver::updateLemmas() {
 
   Debug("minisat::lemmas") << "Solver::updateLemmas() begin" << std::endl;
 
+  // Avoid adding lemmas indefinitely without resource-out
+  spendResource();
+
   CRef conflict = CRef_Undef;
 
   // Decision level to backtrack to

diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 30d72ac751a82e8175a719b52900b4e43a85d19e..7831f211b9edcab54bf10ad0c7572c8cd382034e 100644 (file)
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -215,6 +215,7 @@ public:
     void    budgetOff();
     void    interrupt();          // Trigger a (potentially asynchronous) interruption of the solver.
     void    clearInterrupt();     // Clear interrupt indicator flag.
+    void    spendResource();
 
     // Memory managment:
     //
@@ -252,7 +253,7 @@ public:
 
     // Statistics: (read-only member variable)
     //
-    uint64_t solves, starts, decisions, rnd_decisions, propagations, conflicts;
+    uint64_t solves, starts, decisions, rnd_decisions, propagations, conflicts, resources_consumed;
     uint64_t dec_vars, clauses_literals, learnts_literals, max_literals, tot_literals;
 
 protected:
@@ -526,8 +527,9 @@ inline void     Solver::clearInterrupt(){ asynch_interrupt = false; }
 inline void     Solver::budgetOff(){ conflict_budget = propagation_budget = -1; }
 inline bool     Solver::withinBudget() const {
     return !asynch_interrupt &&
-           (conflict_budget    < 0 || conflicts < (uint64_t)conflict_budget) &&
+           (conflict_budget    < 0 || conflicts + resources_consumed < (uint64_t)conflict_budget) &&
            (propagation_budget < 0 || propagations < (uint64_t)propagation_budget); }
+inline void     Solver::spendResource() { ++resources_consumed; }
 
 // FIXME: after the introduction of asynchronous interrruptions the solve-versions that return a
 // pure bool do not give a safe interface. Either interrupts must be possible to turn off here, or

diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index e4956ecc82067a13059b92cbd7a892f7ba13e68d..4a192d0d2f52ca6a7469b9926199cc7e95b68531 100644 (file)
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -168,10 +168,10 @@ SatValue MinisatSatSolver::solve(unsigned long& resource) {
     d_minisat->setConfBudget(resource);
   }
   Minisat::vec<Minisat::Lit> empty;
-  unsigned long conflictsBefore = d_minisat->conflicts;
+  unsigned long conflictsBefore = d_minisat->conflicts + d_minisat->resources_consumed;
   SatValue result = toSatLiteralValue(d_minisat->solveLimited(empty));
   d_minisat->clearInterrupt();
-  resource = d_minisat->conflicts - conflictsBefore;
+  resource = d_minisat->conflicts + d_minisat->resources_consumed - conflictsBefore;
   Trace("limit") << "SatSolver::solve(): it took " << resource << " conflicts" << std::endl;
   return result;
 }
@@ -182,6 +182,9 @@ SatValue MinisatSatSolver::solve() {
   return toSatLiteralValue(d_minisat->solve());
 }
 
+void MinisatSatSolver::spendResource() {
+  d_minisat->spendResource();
+}
 
 void MinisatSatSolver::interrupt() {
   d_minisat->interrupt();

diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index a919bbcc4597f252ac9b23a92fefb215c4c3e466..b37371d98eb2eb028eafeb5beb14d04212fe638f 100644 (file)
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -62,6 +62,7 @@ public:
   SatValue solve();
   SatValue solve(long unsigned int&);
 
+  void spendResource();
   void interrupt();
 
   SatValue value(SatLiteral l);

diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 929b867c9701fc38c02df6bfc19e69583f37b47f..8e7e53474a2c16d7a2ef26b3efb866b73365fd55 100644 (file)
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -61,6 +61,9 @@ 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;
+
   /** Interrupt the solver */
   virtual void interrupt() = 0;
 

diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
index 6651260599fa2c4c34ce6ec2e6deec11e261049e..679b68a2f380060a37f2bfab00d076fb008fd81e 100644 (file)
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -93,6 +93,9 @@ public:
   void renewVar(SatLiteral lit, int level = -1) {
   }
 
+  void spendResource() {
+  }
+
   void interrupt() {
   }