solver3: Store clauses as the reasons for decisions

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".

1 files changed, 5 insertions, 4 deletions

diff --git a/apt-pkg/solver3.h b/apt-pkg/solver3.h
index d4a584f2d..65a201222 100644
--- a/apt-pkg/solver3.h
+++ b/apt-pkg/solver3.h
@@ -259,6 +259,7 @@ class Solver
    {
       return static_cast<depth_type>(choices.size());
    }
+   inline Var bestReason(Clause const *clause, Var var) const;
 
    public:
    // \brief Create a new decision level.
@@ -274,9 +275,9 @@ class Solver
    Solver(pkgCache &Cache, pkgDepCache::Policy &Policy, EDSP::Request::Flags requestFlags);
 
    // Assume that the variable is decided as specified.
-   [[nodiscard]] bool Assume(Var var, bool decision, Var reason);
+   [[nodiscard]] bool Assume(Var var, bool decision, const Clause *reason = nullptr);
    // Enqueue a decision fact
-   [[nodiscard]] bool Enqueue(Var var, bool decision, Var reason);
+   [[nodiscard]] bool Enqueue(Var var, bool decision, const Clause *reason = nullptr);
 
    // \brief Apply the selections from the dep cache to the solver
    [[nodiscard]] bool FromDepCache(pkgDepCache &depcache);
@@ -340,7 +341,7 @@ struct APT::Solver::Var
    {
       return IsVersion == 0 && MapPtr == 0;
    }
-   bool operator==(Var const other)
+   bool operator==(Var const other) const
    {
       return IsVersion == other.IsVersion && MapPtr == other.MapPtr;
    }
@@ -447,7 +448,7 @@ struct APT::Solver::State
    // doesn't increase to unwind.
    //
    // Vars < 0 are package ID, reasons > 0 are version IDs.
-   Var reason{};
+   const Clause *reason{};
 
    // \brief The depth at which the decision has been taken
    depth_type depth{0};