diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-06 22:57:57 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-06 22:57:57 -0400 |
commit | 744792614fdd8da94eecd5b0cad7c3cb19b3d91c (patch) | |
tree | beaf843bb917f99bc9c1742eafe41be6aab71a08 /src/prop/minisat | |
parent | ecc45b22ce41b6cde8e42a4c1baca4a0cd7c3ea3 (diff) |
Fix a resource limiting issue where interruption didn't occur promptly. Thanks Johannes Kanig for the report.
Diffstat (limited to 'src/prop/minisat')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 3 | ||||
-rw-r--r-- | src/prop/minisat/core/Solver.h | 2 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 3 | ||||
-rw-r--r-- | src/prop/minisat/minisat.h | 2 |
4 files changed, 7 insertions, 3 deletions
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); |