diff options
Diffstat (limited to 'apt-pkg/solver3.h')
| -rw-r--r-- | apt-pkg/solver3.h | 596 |
1 files changed, 335 insertions, 261 deletions
diff --git a/apt-pkg/solver3.h b/apt-pkg/solver3.h index 45b55d962..4a2b4ac8d 100644 --- a/apt-pkg/solver3.h +++ b/apt-pkg/solver3.h @@ -22,7 +22,7 @@ template <typename T> struct always_false : std::false_type {}; -namespace APT +namespace APT::Solver { /** @@ -59,6 +59,10 @@ class ContiguousCacheMap V &operator[](const K *key) { return data_[key->ID]; } const V &operator[](const K *key) const { return data_[key->ID]; } ~ContiguousCacheMap() { delete[] data_; } + + // Delete copy constructors for memory safety (rule of 3) + ContiguousCacheMap(const ContiguousCacheMap &) = delete; + ContiguousCacheMap &operator=(const ContiguousCacheMap &) = delete; }; /** @@ -67,6 +71,203 @@ class ContiguousCacheMap template <typename K, typename V> using FastContiguousCacheMap = ContiguousCacheMap<K, V, true>; +struct Lit; + +// \brief Groups of works, these are ordered. +// +// Later items will be skipped if they are optional, or we will when backtracking, +// try a different choice for them. +enum class Group : uint8_t +{ + HoldOrDelete, + + // Satisfying dependencies on entirely new packages first is a good idea because + // it may contain replacement packages like libfoo1t64 whereas we later will see + // Depends: libfoo1 where libfoo1t64 Provides libfoo1 and we'd have to choose. + SatisfyNew, + Satisfy, + // On a similar note as for SatisfyNew, if the dependency contains obsolete packages + // try it last. + SatisfyObsolete, + + // Select a version of a package chosen for install. + SelectVersion, + + // My intuition tells me that we should try to schedule upgrades first, then + // any non-obsolete installed packages, and only finally obsolete ones, such + // that newer packages guide resolution of dependencies for older ones, they + // may have more stringent dependencies, like a (>> 2) whereas an obsolete + // package may have a (>> 1), for example. + UpgradeManual, + InstallManual, + ObsoleteManual, + + // Automatically installed packages must come last in the group, this allows + // us to see if they were installed as a dependency of a manually installed package, + // allowing a simple implementation of an autoremoval code. + UpgradeAuto, + KeepAuto, + ObsoleteAuto, + + // Satisfy optional dependencies that were previously satisfied but won't otherwise be installed + SatisfySuggests, +}; + +// \brief This essentially describes the install state in RFC2119 terms. +enum class LiftedBool : uint8_t +{ + // \brief We have not made a choice about the package yet + Undefined, + // \brief We need to install this package + True, + // \brief We cannot install this package (need conflicts with it) + False, +}; + +/** + * \brief Tagged union holding either a package, version, or nothing; representing the reason for installing something. + * + * We want to keep track of the reason why things are being installed such that + * we can have sensible debugging abilities; and we want to generically refer to + * both packages and versions as variables, hence this class was added. + * + */ +struct Var +{ + uint32_t value; + + explicit constexpr Var(uint32_t value = 0) : value{value} {} + explicit Var(pkgCache::PkgIterator const &Pkg) : value(uint32_t(Pkg.MapPointer()) << 1) {} + explicit Var(pkgCache::VerIterator const &Ver) : value(uint32_t(Ver.MapPointer()) << 1 | 1) {} + + inline constexpr bool isVersion() const { return value & 1; } + inline constexpr uint32_t mapPtr() const { return value >> 1; } + + // \brief Return the package, if any, otherwise 0. + map_pointer<pkgCache::Package> Pkg() const + { + return isVersion() ? 0 : map_pointer<pkgCache::Package>{mapPtr()}; + } + // \brief Return the version, if any, otherwise 0. + map_pointer<pkgCache::Version> Ver() const + { + return isVersion() ? map_pointer<pkgCache::Version>{mapPtr()} : 0; + } + // \brief Return the package iterator if storing a package, or an empty one + pkgCache::PkgIterator Pkg(pkgCache &cache) const + { + return isVersion() ? pkgCache::PkgIterator() : pkgCache::PkgIterator(cache, cache.PkgP + Pkg()); + } + // \brief Return the version iterator if storing a package, or an empty end. + pkgCache::VerIterator Ver(pkgCache &cache) const + { + return isVersion() ? pkgCache::VerIterator(cache, cache.VerP + Ver()) : pkgCache::VerIterator(); + } + // \brief Return a package, cast from version if needed + pkgCache::PkgIterator CastPkg(pkgCache &cache) const + { + return isVersion() ? Ver(cache).ParentPkg() : Pkg(cache); + } + // \brief Check if there is no reason. + constexpr bool empty() const { return value == 0; } + constexpr bool operator!=(Var const other) const noexcept { return value != other.value; } + constexpr bool operator==(Var const other) const noexcept { return value == other.value; } + + /// \brief Negate + constexpr Lit operator~() const; + + 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)"; + } +}; + +/** + * \brief A literal is a variable with a sign. + * + * A literal 'A' means 'install A' whereas a literal '-A' means 'do not install A'. + */ +struct Lit +{ + private: + friend struct std::hash<Lit>; + // Private constructor from a number, to be used with operator~ + explicit constexpr Lit(int32_t value) : value{value} {} + int32_t value; + + public: + // SAFETY: value must be 31 bit, one bit is needed for the sign. + constexpr Lit(Var var) : value{static_cast<int32_t>(var.value)} {} + + // Accessors + constexpr Var var() const { return Var(std::abs(value)); } + constexpr bool sign() const { return value < 0; } + constexpr Lit operator~() const { return Lit(-value); } + + // Properties + constexpr bool empty() const { return value == 0; } + constexpr bool operator!=(Lit const other) const noexcept { return value != other.value; } + constexpr bool operator==(Lit const other) const noexcept { return value == other.value; } + + std::string toString(pkgCache &cache) const { return (sign() ? "not " : "") + var().toString(cache); } +}; + +/** + * \brief A single clause + * + * A clause is a normalized, expanded dependency, translated into an implication + * in terms of Var objects, that is, `reason -> solutions[0] | ... | solutions[n]` + */ +struct Clause +{ + // \brief Underyling dependency + pkgCache::Dependency *dep = nullptr; + // \brief Var for the work + Var reason; + // \brief The group we are in + Group group; + // \brief Possible solutions to this task, ordered in order of preference. + std::vector<Var> solutions{}; + // \brief An optional clause does not need to be satisfied + bool optional; + + // \brief A negative clause negates the solutions, that is X->A|B you get X->!(A|B), aka X->!A&!B + bool negative; + + // \brief An optional clause may be eager + bool eager; + + // Clauses merged with this clause + std::forward_list<Clause> merged; + + inline Clause(Var reason, Group group, bool optional = false, bool negative = false) : reason(reason), group(group), optional(optional), negative(negative), eager(not optional) {} + + std::string toString(pkgCache &cache, bool pretty = false, bool showMerged = true) const; +}; + +constexpr Lit Solver::Var::operator~() const +{ + return ~Lit(*this); +} + +inline LiftedBool operator~(LiftedBool value) +{ + switch (value) + { + case LiftedBool::Undefined: + return LiftedBool::Undefined; + case LiftedBool::True: + return LiftedBool::False; + case LiftedBool::False: + return LiftedBool::True; + } + abort(); +} + /* * \brief APT 3.0 solver * @@ -79,71 +280,24 @@ using FastContiguousCacheMap = ContiguousCacheMap<K, V, true>; */ class Solver { - enum class Decision : uint16_t; - enum class Hint : uint16_t; - struct Var; - struct CompareProviders3; + protected: struct State; - struct Clause; struct Work; - struct Solved; - friend struct std::hash<APT::Solver::Var>; + struct Trail; - // \brief Groups of works, these are ordered. - // - // Later items will be skipped if they are optional, or we will when backtracking, - // try a different choice for them. - enum class Group : uint8_t - { - HoldOrDelete, - - // Satisfying dependencies on entirely new packages first is a good idea because - // it may contain replacement packages like libfoo1t64 whereas we later will see - // Depends: libfoo1 where libfoo1t64 Provides libfoo1 and we'd have to choose. - SatisfyNew, - Satisfy, - // On a similar note as for SatisfyNew, if the dependency contains obsolete packages - // try it last. - SatisfyObsolete, - - // Select a version of a package chosen for install. - SelectVersion, - - // My intuition tells me that we should try to schedule upgrades first, then - // any non-obsolete installed packages, and only finally obsolete ones, such - // that newer packages guide resolution of dependencies for older ones, they - // may have more stringent dependencies, like a (>> 2) whereas an obsolete - // package may have a (>> 1), for example. - UpgradeManual, - InstallManual, - ObsoleteManual, - - // Automatically installed packages must come last in the group, this allows - // us to see if they were installed as a dependency of a manually installed package, - // allowing a simple implementation of an autoremoval code. - UpgradeAuto, - KeepAuto, - ObsoleteAuto, - - // Satisfy optional dependencies that were previously satisfied but won't otherwise be installed - SatisfySuggests, - }; - - // \brief Type to record depth at. This may very well be a 16-bit - // unsigned integer, then change Solver::State::Decision to be a + // \brief Type to record decision level at. This may very well be a 16-bit + // unsigned integer, then change Solver::State::LiftedBool to be a // uint16_t class enum as well to get a more compact space. - using depth_type = unsigned int; + using level_type = unsigned int; // Documentation template <typename T> using heap = std::vector<T>; - static_assert(sizeof(depth_type) >= sizeof(map_id_t)); + static_assert(sizeof(level_type) >= sizeof(map_id_t)); // Cache is needed to construct Iterators from Version objects we see pkgCache &cache; - // Policy is needed for determining candidate version. - pkgDepCache::Policy &policy; // Root state std::unique_ptr<State> rootState; // States for packages @@ -174,304 +328,211 @@ class Solver inline State &operator[](Var r); inline const State &operator[](Var r) const; - mutable FastContiguousCacheMap<pkgCache::Package, char> pkgObsolete; - // \brief Check if package is obsolete. - // \param AllowManual controls whether manual packages can be obsolete - bool Obsolete(pkgCache::PkgIterator pkg, bool AllowManual=false) const; - bool ObsoletedByNewerSourceVersion(pkgCache::VerIterator cand) const; - - mutable FastContiguousCacheMap<pkgCache::Version, short> priorities; - short GetPriority(pkgCache::VerIterator ver) const - { - if (priorities[ver] == 0) - priorities[ver] = policy.GetPriority(ver); - return priorities[ver]; - } - - mutable ContiguousCacheMap<pkgCache::Package, pkgCache::VerIterator> candidates; - pkgCache::VerIterator GetCandidateVer(pkgCache::PkgIterator pkg) const - { - if (candidates[pkg].end()) - candidates[pkg] = policy.GetCandidateVer(pkg); - return candidates[pkg]; - } - // \brief Heap of the remaining work. // - // We are using an std::vector with std::make_heap(), std::push_heap(), - // and std::pop_heap() rather than a priority_queue because we need to - // be able to iterate over the queued work and see if a choice would - // invalidate any work. + // In contrast to MiniSAT which picks undecided literals and decides them, + // we keep track of unsolved active clauses in a priority queue. This allows + // us to for example, solve Depends before Recommends (see Group). heap<Work> work; - // \brief Backlog of solved work. - // - // Solved work may become invalidated when backtracking, so store it - // here to revisit it later. This is similar to what MiniSAT calls the - // trail; one distinction is that we have both literals and our work - // queue to be concerned about - std::vector<Solved> solved; + /// \brief Trail of assignments done, and clauses solved. + /// + /// Record past assignments and solved clauses such that we can revert them when + /// backtracking. + std::vector<Trail> trail; + + /// \brief Separator indices for different decision levels in trail + std::vector<level_type> trailLim{}; // \brief Propagation queue std::queue<Var> propQ; - // \brief Discover variables - std::queue<Var> discoverQ; - - // \brief Current decision level. - // - // This is an index into the solved vector. - std::vector<depth_type> choices{}; // \brief The time we called Solve() time_t startTime{}; - EDSP::Request::Flags requestFlags; /// Various configuration options std::string version{_config->Find("APT::Solver", "3.0")}; // \brief Debug level int debug{_config->FindI("Debug::APT::Solver")}; - // \brief If set, we try to keep automatically installed packages installed. - bool KeepAuto{version == "3.0" || not _config->FindB("APT::Get::AutomaticRemove")}; - // \brief Determines if we are in upgrade mode. - bool IsUpgrade{_config->FindB("APT::Solver::Upgrade", requestFlags &EDSP::Request::UPGRADE_ALL)}; - // \brief If set, removals are allowed. - bool AllowRemove{_config->FindB("APT::Solver::Remove", not(requestFlags & EDSP::Request::FORBID_REMOVE))}; - // \brief If set, removal of manual packages is allowed. - bool AllowRemoveManual{AllowRemove && _config->FindB("APT::Solver::RemoveManual", true)}; - // \brief If set, installs are allowed. - bool AllowInstall{_config->FindB("APT::Solver::Install", not(requestFlags & EDSP::Request::FORBID_NEW_INSTALL))}; - // \brief If set, we use strict pinning. - bool StrictPinning{_config->FindB("APT::Solver::Strict-Pinning", true)}; - // \brief If set, we install missing recommends and pick new best packages. - bool FixPolicyBroken{_config->FindB("APT::Get::Fix-Policy-Broken")}; - // \brief If set, we use strict pinning. - bool DeferVersionSelection{_config->FindB("APT::Solver::Defer-Version-Selection", true)}; // \brief If set, we use strict pinning. int Timeout{_config->FindI("APT::Solver::Timeout", 10)}; - // \brief Keep recommends installed - bool KeepRecommends{_config->FindB("APT::AutoRemove::RecommendsImportant", true)}; - // \brief Keep suggests installed - bool KeepSuggests{_config->FindB("APT::AutoRemove::SuggestsImportant", true)}; - // \brief Discover a variable, translating the underlying dependencies to the SAT presentation // // This does a breadth-first search of the entire dependency tree of var, // utilizing the discoverQ above. - void Discover(Var var); - // \brief Link a clause into the watchers - const Clause *RegisterClause(Clause &&clause); - // \brief Enqueue dependencies shared by all versions of the package. - void RegisterCommonDependencies(pkgCache::PkgIterator Pkg); - - // \brief Translate an or group into a clause object - [[nodiscard]] Clause TranslateOrGroup(pkgCache::DepIterator start, pkgCache::DepIterator end, Var reason); + virtual void Discover(Var var) = 0; // \brief Propagate all pending propagations [[nodiscard]] bool Propagate(); - // \brief Return the current depth (choices.size() with casting) - depth_type depth() + // \brief Return the current level (.size() with casting) + level_type decisionLevel() { - return static_cast<depth_type>(choices.size()); + return static_cast<level_type>(trailLim.size()); } inline Var bestReason(Clause const *clause, Var var) const; + 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 / solved work item + // \brief Undo a single assignment / trail work item void UndoOne(); // \brief Add work to our work queue. [[nodiscard]] bool AddWork(Work &&work); // \brief Basic solver initializer. This cannot fail. - Solver(pkgCache &Cache, pkgDepCache::Policy &Policy, EDSP::Request::Flags requestFlags); - ~Solver(); - - // Assume that the variable is decided as specified. - [[nodiscard]] bool Assume(Var var, bool decision, const Clause *reason = nullptr); - // Enqueue a decision fact - [[nodiscard]] bool Enqueue(Var var, bool decision, const Clause *reason = nullptr); + Solver(pkgCache &Cache); + virtual ~Solver(); - // \brief Apply the selections from the dep cache to the solver - [[nodiscard]] bool FromDepCache(pkgDepCache &depcache); - // \brief Apply the solver result to the depCache - [[nodiscard]] bool ToDepCache(pkgDepCache &depcache) const; + // Assume a literal + [[nodiscard]] bool Assume(Lit lit, const Clause *reason = nullptr); + // Enqueue a fact + [[nodiscard]] bool Enqueue(Lit lit, const Clause *reason = nullptr); // \brief Solve the dependencies [[nodiscard]] bool Solve(); // Print dependency chain - std::string WhyStr(Var reason) const; + virtual std::string WhyStr(Var reason) const; /** * \brief Print a long reason string * - * Print a reason as to why `rclause` implies `decision` for the variable `var`. + * Print a reason as to why `rclause` implies `assignment` for the variable `var`. * * \param var The variable to print the reason for - * \param decision The assumed decision to print the reason for (may be different from actual decision if rclause is specified) + * \param assignment The assumed assignment to print the reason for (may be different from actual assignment if rclause is specified) * \param rclause The clause that caused this variable to be marked (or would be marked) * \param prefix A prefix, for indentation purposes, as this is recursive * \param seen A set of seen objects such that the output does not repeat itself (not for safety, it is acyclic) */ - std::string LongWhyStr(Var var, bool decision, const Clause *rclause, std::string prefix, std::unordered_set<Var> &seen) const; - - // \brief Temporary internal API with external linkage for the `apt why` and `apt why-not` commands. - APT_PUBLIC static std::string InternalCliWhy(pkgDepCache &depcache, pkgCache::PkgIterator Pkg, bool decision); + virtual std::string LongWhyStr(Var var, bool assignment, const Clause *rclause, std::string prefix, std::unordered_set<Var> &seen) const; }; -}; // namespace APT - -/** - * \brief Tagged union holding either a package, version, or nothing; representing the reason for installing something. +/* + * \brief APT 3.0 solver * - * We want to keep track of the reason why things are being installed such that - * we can have sensible debugging abilities; and we want to generically refer to - * both packages and versions as variables, hence this class was added. + * This is a simple solver focused on understandability and sensible results, it + * will not generally find all solutions to the problem but will try to find the best + * ones. * + * It is a brute force solver with heuristics, conflicts learning, and 2**32 levels + * of backtracking. */ -struct APT::Solver::Var +class DependencySolver : public Solver { - uint32_t value; + friend class CompareProviders3; - explicit constexpr Var(uint32_t value = 0) : value{value} {} - explicit Var(pkgCache::PkgIterator const &Pkg) : value(uint32_t(Pkg.MapPointer()) << 1) {} - explicit Var(pkgCache::VerIterator const &Ver) : value(uint32_t(Ver.MapPointer()) << 1 | 1) {} + // Policy is needed for determining candidate version. + pkgDepCache::Policy &policy; + // Request flags determine the behavior of the options below, make sure it comes first. + EDSP::Request::Flags requestFlags; - inline constexpr bool isVersion() const { return value & 1; } - inline constexpr uint32_t mapPtr() const { return value >> 1; } + // Configuration options for the dependency solver + bool KeepAuto{version == "3.0" || not _config->FindB("APT::Get::AutomaticRemove")}; + bool IsUpgrade{_config->FindB("APT::Solver::Upgrade", requestFlags &EDSP::Request::UPGRADE_ALL)}; + bool AllowRemove{_config->FindB("APT::Solver::Remove", not(requestFlags & EDSP::Request::FORBID_REMOVE))}; + bool AllowRemoveManual{AllowRemove && _config->FindB("APT::Solver::RemoveManual", true)}; + bool AllowInstall{_config->FindB("APT::Solver::Install", not(requestFlags & EDSP::Request::FORBID_NEW_INSTALL))}; + bool StrictPinning{_config->FindB("APT::Solver::Strict-Pinning", true)}; + bool FixPolicyBroken{_config->FindB("APT::Get::Fix-Policy-Broken")}; + bool DeferVersionSelection{_config->FindB("APT::Solver::Defer-Version-Selection", true)}; + bool KeepRecommends{_config->FindB("APT::AutoRemove::RecommendsImportant", true)}; + bool KeepSuggests{_config->FindB("APT::AutoRemove::SuggestsImportant", true)}; - // \brief Return the package, if any, otherwise 0. - map_pointer<pkgCache::Package> Pkg() const - { - return isVersion() ? 0 : map_pointer<pkgCache::Package>{mapPtr()}; - } - // \brief Return the version, if any, otherwise 0. - map_pointer<pkgCache::Version> Ver() const - { - return isVersion() ? map_pointer<pkgCache::Version>{mapPtr()} : 0; - } - // \brief Return the package iterator if storing a package, or an empty one - pkgCache::PkgIterator Pkg(pkgCache &cache) const - { - return isVersion() ? pkgCache::PkgIterator() : pkgCache::PkgIterator(cache, cache.PkgP + Pkg()); - } - // \brief Return the version iterator if storing a package, or an empty end. - pkgCache::VerIterator Ver(pkgCache &cache) const - { - return isVersion() ? pkgCache::VerIterator(cache, cache.VerP + Ver()) : pkgCache::VerIterator(); - } - // \brief Return a package, cast from version if needed - pkgCache::PkgIterator CastPkg(pkgCache &cache) const + // Helper functions for detecting obsolete packages + mutable FastContiguousCacheMap<pkgCache::Package, char> pkgObsolete; + bool Obsolete(pkgCache::PkgIterator pkg, bool AllowManual = false) const; + bool ObsoletedByNewerSourceVersion(pkgCache::VerIterator cand) const; + + // GetPriority() with caching + mutable FastContiguousCacheMap<pkgCache::Version, short> priorities; + short GetPriority(pkgCache::VerIterator ver) const { - return isVersion() ? Ver(cache).ParentPkg() : Pkg(cache); + if (priorities[ver] == 0) + priorities[ver] = policy.GetPriority(ver); + return priorities[ver]; } - // \brief Check if there is no reason. - constexpr bool empty() const { return value == 0; } - constexpr bool operator!=(Var const other) const { return value != other.value; } - constexpr bool operator==(Var const other) const { return value == other.value; } - std::string toString(pkgCache &cache) const + // GetCandidateVer() with caching + mutable ContiguousCacheMap<pkgCache::Package, pkgCache::VerIterator> candidates; + pkgCache::VerIterator GetCandidateVer(pkgCache::PkgIterator pkg) 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)"; + if (candidates[pkg].end()) + candidates[pkg] = policy.GetCandidateVer(pkg); + return candidates[pkg]; } -}; - -/** - * \brief A single clause - * - * A clause is a normalized, expanded dependency, translated into an implication - * in terms of Var objects, that is, `reason -> solutions[0] | ... | solutions[n]` - */ -struct APT::Solver::Clause -{ - // \brief Underyling dependency - pkgCache::Dependency *dep = nullptr; - // \brief Var for the work - Var reason; - // \brief The group we are in - Group group; - // \brief Possible solutions to this task, ordered in order of preference. - std::vector<Var> solutions{}; - // \brief An optional clause does not need to be satisfied - bool optional; - // \brief A negative clause negates the solutions, that is X->A|B you get X->!(A|B), aka X->!A&!B - bool negative; - - // \brief An optional clause may be eager - bool eager; + // \brief Discover variables + std::queue<Var> discoverQ; + /// \brief Discover the dependencies of the variable + void Discover(Var var) override; + /// \brief Link a clause into the watchers + const Clause *RegisterClause(Clause &&clause); + /// \brief Enqueue dependencies shared by all versions of the package. + void RegisterCommonDependencies(pkgCache::PkgIterator Pkg); - // Clauses merged with this clause - std::forward_list<Clause> merged; + /// \brief Translate an or group into a clause object + [[nodiscard]] Clause TranslateOrGroup(pkgCache::DepIterator start, pkgCache::DepIterator end, Var reason); - inline Clause(Var reason, Group group, bool optional = false, bool negative = false) : reason(reason), group(group), optional(optional), negative(negative), eager(not optional) {} + public: + // \brief Basic solver initializer. This cannot fail. + DependencySolver(pkgCache &Cache, pkgDepCache::Policy &Policy, EDSP::Request::Flags requestFlags); + ~DependencySolver() override; - std::string toString(pkgCache &cache, bool pretty = false, bool showMerged = true) const; + /// \brief Apply the selections from the dep cache to the solver + [[nodiscard]] bool FromDepCache(pkgDepCache &depcache); + /// \brief Apply the solver result to the depCache + [[nodiscard]] bool ToDepCache(pkgDepCache &depcache) const; + /// \brief Temporary internal API with external linkage for the `apt why` and `apt why-not` commands. + APT_PUBLIC static std::string InternalCliWhy(pkgDepCache &depcache, pkgCache::PkgIterator Pkg, bool assignment); }; - +}; // namespace APT::Solver /** * \brief A single work item * * A work item is a positive dependency that still needs to be resolved. Work - * is ordered, by depth, length of solutions, and optionality. + * is ordered, by level, length of solutions, and optionality. * * The work can always be recalculated from the state by iterating over dependencies * of all packages in there, finding solutions to them, and then adding all dependencies * not yet resolved to the work queue. */ -struct APT::Solver::Work +struct APT::Solver::Solver::Work { const Clause *clause; - // \brief The depth at which the item has been added - depth_type depth; + // \brief The level at which the item has been added + level_type level; - // Number of valid choices + /// Number of valid choices at insertion time size_t size{0}; // \brief This item should be removed from the queue. bool erased{false}; - bool operator<(APT::Solver::Work const &b) const; + bool operator<(APT::Solver::Solver::Work const &b) const; std::string toString(pkgCache &cache) const; - inline Work(const Clause *clause, depth_type depth) : clause(clause), depth(depth) {} -}; - -// \brief This essentially describes the install state in RFC2119 terms. -enum class APT::Solver::Decision : uint16_t -{ - // \brief We have not made a choice about the package yet - NONE, - // \brief We need to install this package - MUST, - // \brief We cannot install this package (need conflicts with it) - MUSTNOT, + inline Work(const Clause *clause, level_type level) : clause(clause), level(level) {} }; /** * \brief The solver state * - * For each version, the solver records a decision at a certain level. It + * For each version, the solver records a assignment at a certain level. It * maintains an array mapping from version ID to state. */ -struct APT::Solver::State +struct APT::Solver::Solver::State { - // \brief The reason for causing this state (invalid for NONE). + // \brief The reason for causing this state (invalid for Undefined). // // Rejects may have been caused by a later state. Consider we select - // between x1 and x2 in depth = N. If we now find dependencies of x1 + // between x1 and x2 in level = N. If we now find dependencies of x1 // leading to a conflict with a package in K < N, we will record all - // of them as REJECT in depth = K. + // of them as REJECT in level = K. // - // You can follow the reason chain upwards as long as the depth + // You can follow the reason chain upwards as long as the level // doesn't increase to unwind. // // Vars < 0 are package ID, reasons > 0 are version IDs. @@ -479,11 +540,10 @@ struct APT::Solver::State const char *reasonStr{}; - // \brief The depth at which the decision has been taken - depth_type depth{0}; + // \brief The level at which the value has been assigned + level_type level{0}; - // \brief This essentially describes the install state in RFC2119 terms. - Decision decision{Decision::NONE}; + LiftedBool assignment{LiftedBool::Undefined}; // \brief Flags. struct @@ -501,20 +561,26 @@ struct APT::Solver::State }; /** - * \brief A solved item. + * \brief A trail item. * - * Here we keep track of solved clauses and variable assignments such that we can easily undo - * them. + * In MiniSAT, a trail item is an assigned literal. However, we store an assigned variable instead, + * since the assignment is still recorded when we need to access the trail; there does not appear + * to be a substantial value in recording the sign here; but it produces a risk for a disagreement + * between the actual state and the sign recorded in the trail. + * + * In addition to MiniSAT's trail, we also need to keep a trail of solved Work items; that is + * clauses that were being solved, as when undoing the trail, we need to mark those clauses + * active again by putting them back on the work heap. */ -struct APT::Solver::Solved +struct APT::Solver::Solver::Trail { - // \brief A variable that has been assigned. We store this as a reason (FIXME: Rename Var to Var) + /// \brief A variable that got assigned True or False. May be reset to Undefined on backtracking. Var assigned; - // \brief A work item that has been solved. This needs to be put back on the queue. + /// \brief A work item (a clause) that was solved. Needs to be put back on the work heap on backtracking. std::optional<Work> work; }; -inline APT::Solver::State &APT::Solver::operator[](Var r) +inline APT::Solver::Solver::State &APT::Solver::Solver::operator[](APT::Solver::Var r) { if (auto P = r.Pkg()) return (*this)[cache.PkgP + P]; @@ -523,7 +589,7 @@ inline APT::Solver::State &APT::Solver::operator[](Var r) return *rootState.get(); } -inline const APT::Solver::State &APT::Solver::operator[](Var r) const +inline const APT::Solver::Solver::State &APT::Solver::Solver::operator[](APT::Solver::Var r) const { return const_cast<Solver &>(*this)[r]; } @@ -535,3 +601,11 @@ struct std::hash<APT::Solver::Var> std::hash<decltype(APT::Solver::Var::value)> hash_value; std::size_t operator()(const APT::Solver::Var &v) const noexcept { return hash_value(v.value); } }; + +// Custom specialization of std::hash can be injected in namespace std. +template <> +struct std::hash<APT::Solver::Lit> +{ + std::hash<decltype(APT::Solver::Lit::value)> hash_value; + std::size_t operator()(const APT::Solver::Lit &v) const noexcept { return hash_value(v.value); } +}; |