From 429e6250b70ebd6e1f2bb31ddfebfb61bf10a3e5 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Fri, 1 Aug 2014 14:31:16 -0400 Subject: [PATCH] Better support for resource-limiting when there aren't any actual conflicts. --- src/prop/bvminisat/bvminisat.cpp | 4 ++++ src/prop/bvminisat/bvminisat.h | 2 ++ src/prop/minisat/core/Solver.cc | 5 ++++- src/prop/minisat/core/Solver.h | 6 ++++-- src/prop/minisat/minisat.cpp | 7 +++++-- src/prop/minisat/minisat.h | 1 + src/prop/sat_solver.h | 3 +++ test/unit/prop/cnf_stream_white.h | 3 +++ 8 files changed, 26 insertions(+), 5 deletions(-) diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp index 7322cd0fa..2121d7366 100644 --- 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 f9d0fbd6a..0101c5d62 100644 --- 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 610023b70..b0d710d66 100644 --- 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 30d72ac75..7831f211b 100644 --- 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 e4956ecc8..4a192d0d2 100644 --- 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 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 a919bbcc4..b37371d98 100644 --- 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 929b867c9..8e7e53474 100644 --- 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 665126059..679b68a2f 100644 --- 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() { } -- 2.30.2