diff options
| -rw-r--r-- | apt-pkg/solver3.cc | 74 | ||||
| -rw-r--r-- | apt-pkg/solver3.h | 2 |
2 files changed, 24 insertions, 52 deletions
diff --git a/apt-pkg/solver3.cc b/apt-pkg/solver3.cc index 54f31a797..b7ad45f27 100644 --- a/apt-pkg/solver3.cc +++ b/apt-pkg/solver3.cc @@ -441,15 +441,6 @@ bool Solver::Propagate() return true; } -void Solver::Push(Var var, Work work) -{ - if (unlikely(debug >= 2)) - std::cerr << "Trying choice for " << work.toString(cache) << std::endl; - - trailLim.push_back(trail.size()); - trail.push_back(Trail{var, std::move(work)}); -} - void Solver::UndoOne() { auto trailItem = trail.back(); @@ -473,8 +464,7 @@ void Solver::UndoOne() if (unlikely(debug >= 4)) std::cerr << "Adding work item " << work->toString(cache) << std::endl; - if (not AddWork(std::move(*work))) - abort(); + must_succeed(AddWork(std::move(*work))); } trail.pop_back(); @@ -568,7 +558,7 @@ bool Solver::Solve() startTime = time(nullptr); while (true) { - while (not Propagate()) + while (_error->PendingError() || not Propagate()) { if (not Pop()) return false; @@ -577,59 +567,44 @@ bool Solver::Solve() if (work.empty()) break; - // *NOW* we can pop the item. + auto item = work.front(); std::pop_heap(work.begin(), work.end()); - + work.pop_back(); // This item has been replaced with a new one. Remove it. - if (work.back().erased) - { - work.pop_back(); + if (item.erased) continue; - } - auto item = std::move(work.back()); - work.pop_back(); - trail.push_back(Trail{Var(), item}); if (std::any_of(item.clause->solutions.begin(), item.clause->solutions.end(), [this](auto ver) { return value(ver) == LiftedBool::True; })) { if (unlikely(debug >= 2)) std::cerr << "ELIDED " << item.toString(cache) << std::endl; - continue; } - - if (unlikely(debug >= 1)) - std::cerr << item.toString(cache) << std::endl; - - bool foundSolution = false; - for (auto &sol : item.clause->solutions) + else if (auto candidate = std::find_if(item.clause->solutions.begin(), item.clause->solutions.end(), [this](auto ver) + { return value(ver) == LiftedBool::Undefined; }); + candidate != item.clause->solutions.end()) { - if (value(sol) == LiftedBool::False) - { - if (unlikely(debug >= 3)) - std::cerr << "(existing conflict: " << sol.toString(cache) << ")\n"; - continue; - } - if (item.size > 1 || item.clause->optional) - { - Push(sol, item); - } if (unlikely(debug >= 3)) - std::cerr << "(try it: " << sol.toString(cache) << ")\n"; - if (not Enqueue(sol, item.clause) && not Pop()) - return false; - foundSolution = true; - break; + std::cerr << item.toString(cache) << "\n" + << "(try it: " << candidate->toString(cache) << ")\n"; + must_succeed(Assume(*candidate, item.clause)); + } + else if (item.clause->optional) + { + if (unlikely(debug >= 1)) + std::cerr << item.toString(cache) << "\n"; } - if (not foundSolution && not item.clause->optional) + else { + if (unlikely(debug >= 1)) + std::cerr << item.toString(cache) << "\n"; // Enqueue produces the right error message for us here, given that reason has been assigned true already... assert(value(item.clause->reason) == LiftedBool::True); - bool res = Enqueue(~item.clause->reason, item.clause); - assert(not res); - if (not Pop()) - return false; + must_succeed(not Enqueue(~item.clause->reason, item.clause)); + assert(value(item.clause->reason) == LiftedBool::True); } + // Must push to trail after any Assume() above. + trail.push_back(Trail{Var(), item}); } return true; @@ -1323,8 +1298,7 @@ bool DependencySolver::FromDepCache(pkgDepCache &depcache) for (auto assumption : manualPackages) { if (not Assume(assumption, {}) || not Propagate()) - if (not Pop()) - abort(); + must_succeed(Pop()); } return true; diff --git a/apt-pkg/solver3.h b/apt-pkg/solver3.h index f66b3cf62..facba4d39 100644 --- a/apt-pkg/solver3.h +++ b/apt-pkg/solver3.h @@ -370,8 +370,6 @@ class Solver inline LiftedBool value(Lit lit) const; public: - // \brief Create a new decision level. - void Push(Var var, Work work); // \brief Revert to the previous decision level. [[nodiscard]] bool Pop(); // \brief Undo a single assignment / trail work item |