From c1f69a64fd5070723ef425cc1255cde2a28966ad Mon Sep 17 00:00:00 2001 From: Julian Andres Klode Date: Thu, 1 Aug 2024 15:51:37 +0900 Subject: solver3: Introduce new Assume() and Enqueue() helpers and use them These are taken roughly from the MiniSAT paper. We still have a bit to go in actually encoding all clauses so the reasons are still variables, and Assume() isn't fully working yet. Adjust the existing Install()/Reject() code to use these functions, we already see additional lines in the log that we failed to log before, and this ensures more consistency. This is sort of still the wrong direction: Install()/Reject() do the propagation too; but that is tbd. --- apt-pkg/solver3.cc | 64 ++++++++++++++-------- apt-pkg/solver3.h | 14 +++++ ...est-bug-549968-install-depends-of-not-installed | 1 + .../integration/test-bug-604222-new-and-autoremove | 4 ++ ...960705-propagate-protected-to-satisfied-depends | 7 +++ .../integration/test-dpkg-i-apt-install-fix-broken | 2 + 6 files changed, 69 insertions(+), 23 deletions(-) diff --git a/apt-pkg/solver3.cc b/apt-pkg/solver3.cc index 5065b9a87..a21af12f9 100644 --- a/apt-pkg/solver3.cc +++ b/apt-pkg/solver3.cc @@ -304,6 +304,35 @@ bool APT::Solver::Obsolete(pkgCache::PkgIterator pkg) const pkgObsolete[pkg->ID] = 2; return true; } +bool APT::Solver::Assume(Var var, bool decision, Var reason) +{ + choices.push_back(solved.size()); + return Enqueue(var, decision, std::move(reason)); +} + +bool APT::Solver::Enqueue(Var var, bool decision, Var reason) +{ + auto &state = (*this)[var]; + auto decisionCast = decision ? Decision::MUST : Decision::MUSTNOT; + + if (state.decision != Decision::NONE) + { + if (state.decision != decisionCast) + return _error->Error("Conflict: %s -> %s%s but %s", WhyStr(reason).c_str(), decision ? "" : "not ", var.toString(cache).c_str(), WhyStr(var).c_str()); + return true; + } + + state.decision = decisionCast; + state.depth = depth(); + state.reason = reason; + + if (unlikely(debug >= 1)) + std::cerr << "[" << depth() << "] " << (decision ? "Install" : "Reject") << ":" << var.toString(cache) << " (" << WhyStr(state.reason) << ")\n"; + + solved.push_back(Solved{var, std::nullopt}); + + return true; +} bool APT::Solver::Install(pkgCache::PkgIterator Pkg, Var reason, Group group) { @@ -329,10 +358,8 @@ bool APT::Solver::Install(pkgCache::PkgIterator Pkg, Var reason, Group group) } // Note decision - if (unlikely(debug >= 1)) - std::cerr << "[" << depth() << "] Install:" << Pkg.FullName() << " (" << WhyStr(reason) << ")\n"; - (*this)[Pkg] = {reason, depth(), Decision::MUST}; - solved.push_back(Solved{Var(Pkg), std::nullopt}); + if (not Enqueue(Var(Pkg), true, reason)) + return false; // Insert the work item. Work workItem{Var(Pkg), depth(), group}; @@ -380,15 +407,10 @@ bool APT::Solver::Install(pkgCache::VerIterator Ver, Var reason, Group group) WhyStr(Var(otherVer)).c_str()); // Note decision - if (unlikely(debug >= 1)) - std::cerr << "[" << depth() << "] Install:" << Ver.ParentPkg().FullName() << "=" << Ver.VerStr() << " (" << WhyStr(reason) << ")\n"; - (*this)[Ver] = {reason, depth(), Decision::MUST}; - solved.push_back(Solved{Var(Ver), std::nullopt}); - if ((*this)[Ver.ParentPkg()].decision != Decision::MUST) - { - (*this)[Ver.ParentPkg()] = {Var(Ver), depth(), Decision::MUST}; - solved.push_back(Solved{Var(Ver.ParentPkg()), std::nullopt}); - } + if (not Enqueue(Var(Ver), true, reason)) + return false; + if (not Enqueue(Var(Ver.ParentPkg()), true, Var(Ver))) + return false; for (auto OV = Ver.ParentPkg().VersionList(); not OV.end(); ++OV) { @@ -423,10 +445,8 @@ bool APT::Solver::Reject(pkgCache::PkgIterator Pkg, Var reason, Group group) return _error->Error("Conflict: %s -> not %s but %s", WhyStr(reason).c_str(), Pkg.FullName().c_str(), WhyStr(Var(Pkg)).c_str()); // Reject the package and its versions. - if (unlikely(debug >= 1)) - std::cerr << "[" << depth() << "] Reject:" << Pkg.FullName() << " (" << WhyStr(reason) << ")\n"; - (*this)[Pkg] = {reason, depth(), Decision::MUSTNOT}; - solved.push_back(Solved{Var(Pkg), std::nullopt}); + if (not Enqueue(Var(Pkg), false, reason)) + return false; for (auto ver = Pkg.VersionList(); not ver.end(); ver++) if (not Reject(ver, Var(Pkg), group)) return false; @@ -452,10 +472,8 @@ bool APT::Solver::Reject(pkgCache::VerIterator Ver, Var reason, Group group) WhyStr(Var(Ver)).c_str()); // Mark the package as rejected and propagate up as needed. - if (unlikely(debug >= 1)) - std::cerr << "[" << depth() << "] Reject:" << Ver.ParentPkg().FullName() << "=" << Ver.VerStr() << " (" << WhyStr(reason) << ")\n"; - (*this)[Ver] = {reason, depth(), Decision::MUSTNOT}; - solved.push_back(Solved{Var(Ver), std::nullopt}); + if (not Enqueue(Var(Ver), false, reason)) + return false; if (auto pkg = Ver.ParentPkg(); (*this)[pkg].decision != Decision::MUSTNOT) { bool anyInstallable = false; @@ -478,8 +496,8 @@ bool APT::Solver::Reject(pkgCache::VerIterator Ver, Var reason, Group group) } else if ((*this)[Ver.ParentPkg()].decision != Decision::MUSTNOT) // Last installable invalidated { - (*this)[Ver.ParentPkg()] = {Var(Ver), depth(), Decision::MUSTNOT}; - solved.push_back(Solved{Var(Ver), std::nullopt}); + if (not Enqueue(Var(Ver.ParentPkg()), false, Var(Ver))) + return false; } } diff --git a/apt-pkg/solver3.h b/apt-pkg/solver3.h index b0ced904a..527e6fc22 100644 --- a/apt-pkg/solver3.h +++ b/apt-pkg/solver3.h @@ -176,6 +176,11 @@ class Solver // \brief Basic solver initializer. This cannot fail. Solver(pkgCache &Cache, pkgDepCache::Policy &Policy); + // Assume that the variable is decided as specified. + bool Assume(Var var, bool decision, Var reason); + // Enqueue a decision fact + bool Enqueue(Var var, bool decision, Var reason); + // \brief Mark the package for install. This is annoying as it incurs a decision bool Install(pkgCache::PkgIterator Pkg, Var reason, Group group); // \brief Install a version. @@ -241,6 +246,15 @@ struct APT::Solver::Var { return IsVersion == 0 && MapPtr == 0; } + + std::string toString(pkgCache &cache) const + { + if (auto P = Pkg(cache); not P.end()) + return P.FullName(); + if (auto V = Ver(cache); not V.end()) + return V.ParentPkg().FullName() + "=" + V.VerStr(); + return "(root)"; + } }; /** diff --git a/test/integration/test-bug-549968-install-depends-of-not-installed b/test/integration/test-bug-549968-install-depends-of-not-installed index f575f9940..76219290a 100755 --- a/test/integration/test-bug-549968-install-depends-of-not-installed +++ b/test/integration/test-bug-549968-install-depends-of-not-installed @@ -34,6 +34,7 @@ Building dependency tree... Package 'extracoolstuff' is not installed, so not removed Solving dependencies...Install coolstuff:i386 () [0] Install:coolstuff:i386=1.0 () +[0] Install:coolstuff:i386 (coolstuff:i386=1.0) Delete extracoolstuff:i386 [0] Reject:extracoolstuff:i386 () [0] Reject:extracoolstuff:i386=1.0 (not extracoolstuff:i386) diff --git a/test/integration/test-bug-604222-new-and-autoremove b/test/integration/test-bug-604222-new-and-autoremove index a53fcb76b..1090e8b93 100755 --- a/test/integration/test-bug-604222-new-and-autoremove +++ b/test/integration/test-bug-604222-new-and-autoremove @@ -98,10 +98,14 @@ CONFLICTING='Reading package lists... Building dependency tree... Solving dependencies...MANUAL dummy-archive:i386 [0] Install:dummy-archive:i386=0.invalid.0 () +[0] Install:dummy-archive:i386 (dummy-archive:i386=0.invalid.0) [0] Install:libavcodec52:i386=4:0.5.2-6 (dummy-archive:i386=0.invalid.0) +[0] Install:libavcodec52:i386 (dummy-archive:i386=0.invalid.0 -> libavcodec52:i386=4:0.5.2-6) [0] Reject:libvtk5-dev:i386=5.4.2-8 (dummy-archive:i386=0.invalid.0 -> libavcodec52:i386=4:0.5.2-6) +[0] Reject:libvtk5-dev:i386 (dummy-archive:i386=0.invalid.0 -> libavcodec52:i386=4:0.5.2-6 -> not libvtk5-dev:i386=5.4.2-8) Item (1@0) dummy-archive:i386=0.invalid.0 -> | libvtk5-dev:i386=5.4.2-8 | libopenal-dev:i386=1:1.12.854-2 [0] Install:libopenal-dev:i386=1:1.12.854-2 (dummy-archive:i386=0.invalid.0) +[0] Install:libopenal-dev:i386 (dummy-archive:i386=0.invalid.0 -> libopenal-dev:i386=1:1.12.854-2) The following additional packages will be installed: libavcodec52 libopenal-dev diff --git a/test/integration/test-bug-960705-propagate-protected-to-satisfied-depends b/test/integration/test-bug-960705-propagate-protected-to-satisfied-depends index 6ffb69bf5..e5a12986d 100755 --- a/test/integration/test-bug-960705-propagate-protected-to-satisfied-depends +++ b/test/integration/test-bug-960705-propagate-protected-to-satisfied-depends @@ -22,14 +22,21 @@ testsuccessequal "Reading package lists... Building dependency tree... Solving dependencies...Install foobar:amd64 () [0] Install:foobar:amd64=1 () +[0] Install:foobar:amd64 (foobar:amd64=1) [0] Install:requires-foo:amd64=1 (foobar:amd64=1) +[0] Install:requires-foo:amd64 (foobar:amd64=1 -> requires-foo:amd64=1) [0] Install:foo:amd64=1 (foobar:amd64=1 -> requires-foo:amd64=1) +[0] Install:foo:amd64 (foobar:amd64=1 -> requires-foo:amd64=1 -> foo:amd64=1) [0] Install:foo-depends:amd64=1 (foobar:amd64=1 -> requires-foo:amd64=1 -> foo:amd64=1) +[0] Install:foo-depends:amd64 (foobar:amd64=1 -> requires-foo:amd64=1 -> foo:amd64=1 -> foo-depends:amd64=1) Item (2@0) foobar:amd64=1 -> | conflicts-foo:amd64=1 | fine-foo:amd64=1 [1] Install:conflicts-foo:amd64=1 (foobar:amd64=1) +[1] Install:conflicts-foo:amd64 (foobar:amd64=1 -> conflicts-foo:amd64=1) [0] Reject:conflicts-foo:amd64=1 () +[0] Reject:conflicts-foo:amd64 (not conflicts-foo:amd64=1) Item (1@0) foobar:amd64=1 -> | conflicts-foo:amd64=1 | fine-foo:amd64=1 [0] Install:fine-foo:amd64=1 (foobar:amd64=1) +[0] Install:fine-foo:amd64 (foobar:amd64=1 -> fine-foo:amd64=1) The following additional packages will be installed: fine-foo foo foo-depends requires-foo diff --git a/test/integration/test-dpkg-i-apt-install-fix-broken b/test/integration/test-dpkg-i-apt-install-fix-broken index a4c3c66d9..21d8e298e 100755 --- a/test/integration/test-dpkg-i-apt-install-fix-broken +++ b/test/integration/test-dpkg-i-apt-install-fix-broken @@ -18,12 +18,14 @@ Correcting dependencies...Install autopkgtest-satdep:amd64 () [0] Install:autopkgtest-satdep:amd64 () [0] Install:autopkgtest-satdep:amd64=1 (autopkgtest-satdep:amd64) [0] Install:debhelper:amd64=1 (autopkgtest-satdep:amd64 -> autopkgtest-satdep:amd64=1) +[0] Install:debhelper:amd64 (autopkgtest-satdep:amd64 -> autopkgtest-satdep:amd64=1 -> debhelper:amd64=1) Done Solving dependencies...Install debhelper:amd64 (M) Install autopkgtest-satdep:amd64 () [0] Install:autopkgtest-satdep:amd64 () [0] Install:autopkgtest-satdep:amd64=1 (autopkgtest-satdep:amd64) [0] Install:debhelper:amd64=1 (autopkgtest-satdep:amd64 -> autopkgtest-satdep:amd64=1) +[0] Install:debhelper:amd64 (autopkgtest-satdep:amd64 -> autopkgtest-satdep:amd64=1 -> debhelper:amd64=1) The following additional packages will be installed: debhelper -- cgit v1.2.3-70-g09d2