| Commit message (Collapse) | Author | Age | Files | Lines |
| |
|
|
|
|
|
|
|
|
|
|
| |
Pushing the stack in push and popping it in pop did not
really work correctly and is more complex than needed.
Instead, push the error stack at the start of the Solve()
method and revert at the end, such that we leave exactly
at the same error stack level we entered.
To handle error clearing on backtracking, just discard any
pending errors.
|
| |
|
|
|
| |
Implement the moving of the auto bit. The whole auto-bit management
is not entirely optimal yet, but this works.
|
| |
|
|
|
| |
Deduplicate the copies in a central one, mark it unavailable to
external users.
|
| |
|
|
| |
Closes: #1096322
|
| |
|
|
| |
This makes the dump almost instant rather than take forever.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
| |
This is the first step that introduces a 1:1 mapping between version
and source version. In a future version this can use the fields
currently marked unavailable to deduplicate the SourceVersion
objects across the group.
The policy gains a member for storing pins for sourceversions.
Together, in the future we should be able to determine candidates
for source versions.
|
| |
|
|
|
| |
These templates are all inline and there is not much sense
exposing their vtables and typeinfo publicly.
|
| | |
|
| |
|
|
| |
Final ABI cleanup before unstable?!
|
| |
|
|
|
| |
main picked up a couple new ifdefs since the branch started; so
clean them up again.
|
| |
|
|
| |
constant string in .data
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
string{=> _view})
|
| |
|
|
| |
VectorizeString(), StringSplit(), SubstVar()
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
|
| |
This involves the use of goto to fix undefined behavior in
the for-loop restart which temporarily generates a K pointing
one element ahead of the start of the array (which is undefined).
|
| |
|
|
| |
This makes it clear from reading that we are accessing an array.
|
| | |
|
| | |
|
| | |
|
| |
|
|
|
| |
Some bit of private refactoring to avoid having to pass
the raw pointer.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
So far we only stored the last reason why something was decided,
for example, if "A depends B | C" and we assigned B=false, C=false,
we'd store "(not) C" as the reason for "(not) A".
This gives us only a partial implication graph; after all "C" was
not the *sole* reason for not installing A. This has two implications:
1. We cannot do conflict-driven clause learning
2. We cannot print excellent information about why packages cannot be
installed (or removed)
This commit is incomplete in addressing both; in particular, we always
store a clause as a reason for something that is not a root object;
whereas MiniSAT would only store a clause on propagation. That is,
if A depends B | C, and we install A, then we have to make a choice
between B|C. Let's say we pick B, we store 'A depends B|C' as the
reason whereas MiniSAT would not store a reason (because it picked
the "next best" unassigned literal).
Hopefully this is not going to be an issue. The reason is used to
calculate the assignments that caused the decision in MiniSAT, but
the idea is that we can just treat reason clauses with unassigned
values as "no reason".
The conflict explanation (WhyStr) has been changed to print the
strongest reason; which produces the same result as the previous
solution for the test suite. What does this mean?
If we look at A depends B|C, let's analyse:
Why not A?
We return the first assigned value for B|C, likely B.
We might have returned C here before as it was the
last assignment, but we might also return C here,
if B is not assigned.
Why B? We return A.
If we look at A conflicts B:
Why not A? Well B
Why not B? Well A
Thanks to the structure of the implication graph this is quite
simple, but also generalizing this to the CNF format should not
be hard.
A future version will extend clauses with backlinks to
pkgCache::Dependency*, allowing us to print useful information
to uses such as "A Depends B | C | D (>= 2)" in the real form, rather
than the expanded form which may be "A -> B | C | D=3 | D=2".
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Dependencies shared by all versions are enqueued at the package
level, so avoid enqueuing duplicates at the version level. This
presumably has no meaningful impact on performance, potentially
a negative performance impact on some workloads as we now need
to find the duplicates again; it can become useful when there
is a lot of backtracking.
More importantly though this improves error messages, because
now we can say that "all versions of foo depend on X", rather
than saying "foo=1 depends on X" and you are left wondering
why we did not select "foo=2".
In this commit though, improved error messages are not implemented,
they depend on redesigning the reason tracking to use clauses.
Also the rationale tracking includes a lot more dependencies of
the form "pkg:arch=version -> pkg:arch" which are annoying. Improved
error messages should fold them into one node.
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
Instead of expensive rescoring of all outstanding items, use
unit propagation to find new units after conflicts.
We still count the items when adding them; but unless they are
0 or 1, which they should not be, they don't have any effect:
The size field is now effectively static.
If the size of an optional clause changed to 1, it is inserted
a second time, and then moves up to the top of the optional
items per the Work::operator< rules.
|
| |
|
|
|
| |
Use Var::toString() to print the variable, instead of duplicating
the code :D
|
| |
|
|
|
|
|
|
|
|
| |
When we call an EDSP solver from ResolveByKeep(), we are not
in an upgrade context: In an upgrade context, we call the solver
directly from upgrade.cc instead of doing any Resolve() or
ResolveByKeep() calls.
This fixes the test-bug-602412-dequote-redirect test case,
where ResolveByKeep() was called as part of --fix-missing
|
| |
|
|
|
|
|
| |
This was a rather silly way to communicate state, and it was
in the wrong place. Notably also, multiple calls to the solver
had the options sticky, that is, if you run upgrade and then
it calls ResolveByKeep(), for example.
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
We inadvertently performed a global ordering of all possible
solutions for the or group using CompareProviders3.
This however is not correct, as we lose the ordering of the
dependency group *too* much. Mostly this has no effect, but
you can see for example in test-explore-or-groups-in-markinstall
various instances of it.
Adjust said test case to work with the 3.0 solver to the extent
possible under the current design. The 3.0 solver does Recommends
after processing any manually installed packages; as such the
various Recommends test cases do not work: A `Recommends: okay|upgrade`
will not upgrade `upgrade` if it visited `upgrade` first.
This may change at a future time, but the correct semantics for
Recommends are not entirely clear. Notably, the existing solver
is not always consistent. You can see here where they matter,
but recently I added test-solver-recommends-depends in which
the Recommends do not influence the choice of other Depends.
|
| |
|
|
|
|
|
|
| |
Phased updates are ignored when strict pinning is on; such that
only the installed version will be available. By design of SAT
solvers, this means that the version selection clause is unit,
and hence the version can be directly propagated, i.e. that
choice is safe.
|
| |
|
|
|
|
|
|
|
|
| |
Already satisfied Recommends should be promoted to Depends; as well
as Recommends that are new, if the version they are from is an upgrade
(such that upgrading does not introduce unsat Recommends).
This only works for the case where the new Recommends actually
exist; test-resolve-by-keep-new-recommends is not yet implemented,
but this means the phasing tests will behave correctly.
|
| |
|
|
|
|
| |
This fixes the difference in test-unpack-different-version-unpacked,
but more importantly this is needed for phasing to be displayed
correctly once that is implemented.
|
| |
|
|
|
|
|
|
| |
This is a bit gnarly, but dist-upgrade is mapped to
is an upgrade + removals allowed + installs allowed
:D
|
| |
|
|
|
|
| |
Restore the depcache's MarkRequired logic for 3.0 solver; and
change the MarkInstall() call to pass a more correct value for
FromUser, to not override an existing automatic status.
|
| |
|
|
|
|
| |
We forgot this in the previous iteration. This makes the reasoning
in the test cases much nicer and apt-test's mantic-to-noble-jak.edsp
now finishes rather than running into the timeout (potentially forever).
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Instead of utilizing the reverse depends functionality of the cache
and marking all possible reverse dependencies for removal, mark them
ourselves by keeping track of reverse-implication-clauses.
Notably, this improves the reverse dependency rejection substantially:
The previous RejectReverseDependencies() function did not handle
Provides.
For this to work correctly right now, we need to discover optional
clauses too when queuing them. This is somewhat suboptimal as we
technically we don't care if they become unsat, we just waste time
tracking them.
The tests get a bit awkward, but oh well, we use what we can
use.
|
| |
|
|
|
| |
A SAT solver can run more or less forever, but that's not a good
user experience.
|