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.h | 14 ++++++++++++++ 1 file changed, 14 insertions(+) (limited to 'apt-pkg/solver3.h') 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)"; + } }; /** -- cgit v1.2.3-70-g09d2