summaryrefslogtreecommitdiff
path: root/apt-pkg/solver3.h
Commit message (Collapse)AuthorAgeFilesLines
...
* solver3: Add const where helpfulJulian Andres Klode2025-02-071-6/+20
| | | | | operator[] is a bit annoying here, but oh well, what can we do?
* solver3: Point to stored clauses, do not copy themJulian Andres Klode2025-02-071-2/+2
| | | | | | This makes Work trivially destructible, and in turn solved, allowing their queues to be destructed without running destructors, and avoiding the copy should have a nice performance improvement.
* solver3: Use a package clause for optional rootsJulian Andres Klode2025-02-071-2/+3
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Instead of iterating over the version here and picking it, just enqueue the package as well, which should allow us to select the version at a later time. This also causes a funny inverse problem now, though, as was evidenced in one of the test cases: To summarize, if our optional roots are all single items, they will be considered soft-unit, causing them to be processed in order. However it can be that an optional root has a specific version selected because another version was rejected. Consider X Conflicts A (= 1) A, B have 2 versions: '2' available, '1' installed B (= n) Depends A (= n) Run `apt install X`. The expected result is for A and B to be upgraded to version 2. With only a package root, if B appears in the cache before A however, we will get: Install X Reject A (= 1) Install B Install B (= 1) # keep it installed Reject A (= 2) => A is being removed as both versions are rejected Hence we do also need to re-introduce the additional version clause, now we get: Install X Reject A (= 1) Install A (= 2) # it got "promoted" to a 'stronger' soft-unit Install B Fail B (= 1) # keep it installed Install B (= 2) Introduce a root state to hold all the clauses that don't have another owner. moo
* solver3: Refactor Dump() to toString()Julian Andres Klode2025-02-071-4/+2
| | | | | This vastly simplifies the code at the expense of performance, lol.
* solver3: Replace PropagateInstall() with Discover()Julian Andres Klode2025-02-071-18/+18
| | | | | | | | | | | | | | | Just propagate the stored clauses after we have discovered them; this is quite straightforward. We now more reliably discover common dependencies at the package level, adjust the test case accordingly. The next step is to make discovery recursive, or iterative, to build an entire recursive tree from all roots, and then we can reject reverse dependencies based on it. A bunch of refactorings are needed in the process. We remove the useless Hint enumeration and insert a flags struct into the State, such that we can record whether a package/version has been discovered, to avoid spending double time on discovery.
* solver3: Extract TranslateOrGroup() out of EnqueueOrGroup()Julian Andres Klode2025-02-071-1/+6
| | | | | | | This is not *purely* a refactoring, we accidentally used the version of the dependency when enqueuing conflicts rather than the reason, so the conflict string in the test case is different; the logging had the same issue.
* solver3: Extract Clause out of WorkJulian Andres Klode2025-02-071-12/+29
| | | | | Extract clause into a separate struct and embed a copy of it in our Work class.
* solver3: Cache all configuration callsJulian Andres Klode2025-02-071-0/+6
|
* solver3: Cache calls to policyJulian Andres Klode2025-02-071-0/+14
| | | | It's a bit silly otherwise.
* solver3: Propagate single choice clauses as factsJulian Andres Klode2025-02-071-1/+1
| | | | | | | | | | | | This removes a bunch of complexity, and generalizes the propagation behavior, such that we don't need to do if (w.solutions.size() == 1 && not w.optional) Enqueue() else AddWork(w); in our callers.
* solver3: Annotate all bool functions with [[nodiscard]]Julian Andres Klode2025-02-071-12/+12
| | | | | It is very important that we check the return value of all these functions, otherwise the logic is wrong.
* solver3: Partially generalize work items from Version to VarJulian Andres Klode2025-02-071-2/+13
| | | | | | | | Store all possible solutions and choices as Var. Currently any Var in here must be a Version because CompareProviders3 cannot compare versions against packages yet, but in the future (TM), this will allow storing packages directly in clauses, which allows defering version selection to a later point.
* solver3: Drop unused upgrade flagJulian Andres Klode2025-02-071-3/+1
| | | | This was leftover from before the groups were added.
* solver3: Use a propagation queueJulian Andres Klode2025-01-301-0/+5
| | | | | | | | | | | | | | | | | | | Instead of directly propagating in a recursive fashion, queue propagations in a queue and work on them in a loop per the miniSAT paper. We call Propagate() only at the end of the FromDepCache() function and then in the Solve loop. Delaying the initial propagation means that we get a stronger reasoning: Assume you have x->a->b->c, y->c and you install x,y: - Previously we traversed: x, y, x->a, a->b, b->c, (y->c) - but now we traverse: x, y, x->a, y->c, a->b, (b->c) Notably c now has the implication y->c instead of x->a->b->c. Inside the solver we need to call Propagate in a loop: Propagating facts can fail and we then backtrack. If backtracking is succesful, we have gained a new fact to propagate.
* solver3: Replace Install() with Enqueue(), and PropagateInstall()Julian Andres Klode2025-01-301-3/+3
| | | | | | Do not enqueue common dependencies if a version is selected already, this avoids test suites changing now in behavior as the ordering is different.
* solver3: Remove NewUnsatRecommends groupJulian Andres Klode2025-01-301-1/+0
| | | | | | This is more or less unused; but it particularly has the bad problem of forcing new unsat recommends to be solved *before* dependencies. Which is awkward.
* solver3: Reject all non-candidates outright for strict pinningJulian Andres Klode2024-12-031-2/+0
| | | | | | | | Reimplement strict pinning by rejecting the non-candidates when translating the problem from the depcache to the solver. This is substantially better than restricting the list of alternatives for an or group to only include allowed ones for debugging purposes, albeit a bit slower.
* solver3: Refactor Install(Ver) to PropagateInstall(Ver)Julian Andres Klode2024-11-021-2/+2
| | | | | | | | | | This is the first part of changing from Install() to Enqueue() for installs, affecting only the versions. For packages, we still have to resolve the group changing: When propagating cleanly, we don't have the information as to which group the package was part of, hence we are no longer able to queue the version selection of upgrades before obsolete packages, for example, which needs solving.
* solver3: Rename the 'dirty' bit to 'erased'Julian Andres Klode2024-11-021-2/+2
| | | | This captures the meaning better
* solver3: Remove the Reject() function, propagate in Enqueue() insteadJulian Andres Klode2024-11-021-4/+3
| | | | | Long term we should have a propagate queue, this is the minimal change to keep the behavior identical, a first step on the road.
* solver3: Introduce new Assume() and Enqueue() helpers and use themJulian Andres Klode2024-11-021-0/+14
| | | | | | | | | | | | | 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.
* solver3: Rename Reason to VarJulian Andres Klode2024-11-021-22/+22
|
* solver3: Track all assignments and undo them individuallyJulian Andres Klode2024-11-021-16/+45
| | | | | | | Adopt MiniSAT's strategy for dealing with assignments and choices, having a single step undoOne() function to undo one and record them all on the queue; this should likely speed up backtracking since we no longer need to rescan everything.
* Fix obsoleted-by handling for experimentalJulian Andres Klode2024-08-121-2/+3
| | | | | | | | | | Basically this boils down to checking that the priority of the source candidate candidate is higher or equal than the priority of the package's candidate that is being under consideration. It stands to reason if we maybe we should actually calculate a source candidate version; this will look similar but may perhaps perform slightly different.
* solver3: Refactor Reason.Pkg()/Reason.Ver() use with iteratorJulian Andres Klode2024-07-161-0/+10
| | | | More code but nicer to read
* solver3: Consider packages as obsolete and not versionsJulian Andres Klode2024-07-021-2/+2
| | | | | | | | | | | | | This makes more sense, as all package versions are obsolete that are not the candidate, usually. Pay special attention to no-strict-pinning: If we don't have strict pinning, a package without a candidate version may still be non-obsolete if the latest version is not obsolete. Likewise, in no-strict-pinning any later source version that exists will cause the package to be considered obsolete, rather than just candidates.
* solver3: Order obsolete choices lastJulian Andres Klode2024-06-131-0/+12
| | | | | | | | | | | | | | | | | | | | | | This has two aspects: 1. For a dependency A | B | C we order the obsolete packages last, that is, if A is obsolete, this gets reordered to B | C | A, such that we try to pick non-obsolete packages first to ease upgrade calculation. 2. When comparing two dependencies, we order dependencies into three groups: First we satisfy dependencies mentioning only non-installed (NEW) packages, then we satisfy "normal" dependencies, and finally we satisfy any dependencies mentioning obsolete packages. This means for example if you have obsolete libfoo1 and a new libfoo1t64, that we will see Depends: libfoo1t64 before any Depends: libfoo1 (which may expand to libfoo1 | libfoo1t64), so we effectively will have selected "replacement" packages this way already before getting to older packages where we would have to choose between the obsolete package and its replacement.
* solver3: Group work itemsJulian Andres Klode2024-06-131-6/+34
| | | | | | | | | | | | | | | | | | | | | Our backtracking is chronological, so we will first try alternative choices or skip optional items in later groups. So installing manually installed packages before automatically installed ones allows manually installed packages to remove automatically installed packages easily. If we did automatic packages first, we'd keep back upgrades for manual packages or change choices for their dependencies, or would have to backtrack harder to get back to the right decision level. That's silly. Ordering automatically installed packages last also allows us to calculate autoremovable packages. Since we will have installed all dependencies from manually installed packages by the point where we get to automatically installed packages, everything that will be installed in those Auto groups is inherently garbage.
* Initial implementation of the 3.0 solverJulian Andres Klode2024-05-141-0/+286
This is a simple backtracking brute-force solver with heurisitcs, this initial version has the following known gaps: - Errors are not kept from branches, the error reporting after backtracking isn't particularly useful. - We cannot show automatically removed packages - We cannot replace packages with others - We do not have conflict-driven clause learning yet Untested: - Multi-arch This solver is fundamentally different in key aspects: - It solves smaller dependency groups before larger ones, leading us to avoid installing A in A|B if B is installed more often and more consistently. - It only keeps the automatic packages reachable via the strongest path. Currently it only implements autoremoval, but not display of autoremoval as we simply enqueue all automatically installed packages at the end when not doing automatic removal. This will need some translation where we Solve() first, and then Solve() again with the automatically installed packages added such that we can mark them as Garbage for display purposes. - It does not remove manually installed packages. Hook the solver in via the EDSP framework, this allows us to achieve easy initial integration without lots of issues. A lot of this work was planned and executed in my free time and then some leaked into work time I suppose. Implementation notes: - Restore the full backlog of items The annoying thing is that we record only when an item was enqueued and not the level at which it was installed, so when going back a decision level we might have to reinstall packages that were queued at an earlier decision level because they were only installed at a later decision level. - When picking one version, reject the others - Propagate conflicts up to reverse dependencies This will recursively mark every reverse dependency that can no longer be satisfied as MUSTNOT. Also make sure to recursively call Reject(Ver) from Reject(Pkg) to make sure we trigger the Rejections there. This means we now end up having Recursion in the algorithm. An alternative approach would be to push *reject* items to the heap and then do them, but this is not entirely straight forward and it may simply not be necessary. - Sort upgrades before other optional installs containing subsets If I want to upgrade a package A, I schedule A3|A2|A1; if another thing depends specifically on A1; we'd not be installed. Hence we need to sort upgrades first. This only is needed for optional packages; manual packages will figure this out naturally. - Rescoring is lazily implemented. Instead of calling make_heap() after rescoring items, we just mark the items as dirty and reinsert them. We also only rescore from the main solve loop, Reject() marks the heap as needing a rescore due to a Conflict (as some versions will no longer be installable), and RescoreWorkIfNeeded() then will do the rescoring. - Recursive unit propagation: Install() and Reject() recursively call each other to promote decisions across single-version dependencies (or across not-anymore satisfiable reverse-depends). - Make Reason constructors explicit, this enhances readability This makes calls like the one in here be Reject(object, Reason(otherObject)) Ensuring that it's clear that the 2nd argument is a reason at the caller side. - Split Decision into Decision and Hint vs. first draft When branching/deciding, we do not want to override SHOULD and MAY. We do not actually use them yet, and we do actually clean them when backtracking, but let's at least keep the data structure correct. Convert the enum to a 16-bit integer so we can still fit in the same space as before.