solver3: Rename key concepts to MiniSAT names

This should make it easier for people with MiniSAT knowledge
to onboard themselves to the solver.

2 files changed, 56 insertions, 55 deletions

diff --git a/apt-pkg/solver3.cc b/apt-pkg/solver3.cc
index afed249e5..6f84a11a8 100644
--- a/apt-pkg/solver3.cc
+++ b/apt-pkg/solver3.cc
@@ -209,7 +209,7 @@ APT::Solver::Solver(pkgCache &cache, pkgDepCache::Policy &policy, EDSP::Request:
 {
    // Ensure trivially
    static_assert(std::is_trivially_destructible_v<Work>);
-   static_assert(std::is_trivially_destructible_v<Solved>);
+   static_assert(std::is_trivially_destructible_v<Trail>);
    static_assert(sizeof(APT::Solver::Var) == sizeof(map_pointer<pkgCache::Package>));
    static_assert(sizeof(APT::Solver::Var) == sizeof(map_pointer<pkgCache::Version>));
    // Root state is "true".
@@ -564,7 +564,7 @@ bool APT::Solver::Obsolete(pkgCache::PkgIterator pkg, bool AllowManual) const
 }
 bool APT::Solver::Assume(Lit lit, const Clause *reason)
 {
-   choices.push_back(solved.size());
+   trailLim.push_back(trail.size());
    return Enqueue(lit, std::move(reason));
 }
 
@@ -588,14 +588,14 @@ bool APT::Solver::Enqueue(Lit lit, const Clause *reason)
    }
 
    state.decision = decisionCast;
-   state.depth = depth();
+   state.depth = decisionLevel();
    state.reason = reason;
 
    // FIXME: Adjust call to bestReason to use lit
    if (unlikely(debug >= 1))
-      std::cerr << "[" << depth() << "] " << (lit.sign() ? "Reject" : "Install") << ":" << lit.var().toString(cache) << " (" << WhyStr(bestReason(reason, lit.var())) << ")\n";
+      std::cerr << "[" << decisionLevel() << "] " << (lit.sign() ? "Reject" : "Install") << ":" << lit.var().toString(cache) << " (" << WhyStr(bestReason(reason, lit.var())) << ")\n";
 
-   solved.push_back(Solved{lit.var(), std::nullopt});
+   trail.push_back(Trail{lit.var(), std::nullopt});
    propQ.push(lit.var());
 
    return true;
@@ -611,7 +611,7 @@ bool APT::Solver::Propagate()
       {
 	 Discover(var);
 	 for (auto &clause : (*this)[var].clauses)
-	    if (not AddWork(Work{clause.get(), depth()}))
+	    if (not AddWork(Work{clause.get(), decisionLevel()}))
 	       return false;
 	 for (auto rclause : (*this)[var].rclauses)
 	 {
@@ -642,7 +642,7 @@ bool APT::Solver::Propagate()
 	       if (rclause->optional)
 	       {
 		  // Enqueue duplicated item, this will ensure we see it at the correct time
-		  if (not AddWork(Work{rclause, depth()}))
+		  if (not AddWork(Work{rclause, decisionLevel()}))
 		     return false;
 	       }
 	       else
@@ -995,29 +995,29 @@ void APT::Solver::Push(Var var, Work work)
    if (unlikely(debug >= 2))
       std::cerr << "Trying choice for " << work.toString(cache) << std::endl;
 
-   choices.push_back(solved.size());
-   solved.push_back(Solved{var, std::move(work)});
+   trailLim.push_back(trail.size());
+   trail.push_back(Trail{var, std::move(work)});
 }
 
 void APT::Solver::UndoOne()
 {
-   auto solvedItem = solved.back();
+   auto trailItem = trail.back();
 
    if (unlikely(debug >= 4))
       std::cerr << "Undoing a single decision\n";
 
-   if (not solvedItem.assigned.empty())
+   if (not trailItem.assigned.empty())
    {
       if (unlikely(debug >= 4))
-	 std::cerr << "Unassign " << solvedItem.assigned.toString(cache) << "\n";
-      auto &state = (*this)[solvedItem.assigned];
+	 std::cerr << "Unassign " << trailItem.assigned.toString(cache) << "\n";
+      auto &state = (*this)[trailItem.assigned];
       state.decision = LiftedBool::Undefined;
       state.reason = nullptr;
       state.reasonStr = nullptr;
       state.depth = 0;
    }
 
-   if (auto work = solvedItem.work)
+   if (auto work = trailItem.work)
    {
       if (unlikely(debug >= 4))
 	 std::cerr << "Adding work item " << work->toString(cache) << std::endl;
@@ -1026,14 +1026,14 @@ void APT::Solver::UndoOne()
 	 abort();
    }
 
-   solved.pop_back();
+   trail.pop_back();
 
    // FIXME: Add the undo handling here once we have watchers.
 }
 
 bool APT::Solver::Pop()
 {
-   if (depth() == 0)
+   if (decisionLevel() == 0)
       return false;
 
    time_t now = time(nullptr);
@@ -1049,15 +1049,15 @@ bool APT::Solver::Pop()
    _error->Discard();
 
    // Assume() actually failed to enqueue anything, abort here
-   if (choices.back() == solved.size())
+   if (trailLim.back() == trail.size())
    {
-      choices.pop_back();
+      trailLim.pop_back();
       return true;
    }
 
-   assert(choices.back() < solved.size());
-   int itemsToUndo = solved.size() - choices.back();
-   auto choice = solved[choices.back()].assigned;
+   assert(trailLim.back() < trail.size());
+   int itemsToUndo = trail.size() - trailLim.back();
+   auto choice = trail[trailLim.back()].assigned;
 
    for (; itemsToUndo; --itemsToUndo)
       UndoOne();
@@ -1065,9 +1065,9 @@ bool APT::Solver::Pop()
    // We need to remove any work that is at a higher depth.
    // FIXME: We should just mark the entries as erased and only do a compaction
    //        of the heap once we have a lot of erased entries in it.
-   choices.pop_back();
+   trailLim.pop_back();
    work.erase(std::remove_if(work.begin(), work.end(), [this](Work &w) -> bool
-			     { return w.depth > depth() || w.erased; }),
+			     { return w.depth > decisionLevel() || w.erased; }),
 	      work.end());
    std::make_heap(work.begin(), work.end());
 
@@ -1136,7 +1136,7 @@ bool APT::Solver::Solve()
       }
       auto item = std::move(work.back());
       work.pop_back();
-      solved.push_back(Solved{Var(), item});
+      trail.push_back(Trail{Var(), item});
 
       if (std::any_of(item.clause->solutions.begin(), item.clause->solutions.end(), [this](auto ver)
 		      { return value(ver) == LiftedBool::True; }))
@@ -1265,7 +1265,7 @@ bool APT::Solver::FromDepCache(pkgDepCache &depcache)
 	    Clause w{Var(), Group, isOptional};
 	    w.solutions.push_back(Var(P));
 	    auto insertedW = RegisterClause(std::move(w));
-	    if (insertedW && not AddWork(Work{insertedW, depth()}))
+	    if (insertedW && not AddWork(Work{insertedW, decisionLevel()}))
 	       return false;
 
 	    if (not isAuto)
@@ -1281,7 +1281,7 @@ bool APT::Solver::FromDepCache(pkgDepCache &depcache)
 	       shortcircuit.solutions.push_back(Var(V));
 	    std::stable_sort(shortcircuit.solutions.begin(), shortcircuit.solutions.end(), CompareProviders3{cache, policy, P, *this});
 	    auto insertedShort = RegisterClause(std::move(shortcircuit));
-	    if (insertedShort && not AddWork(Work{insertedShort, depth()}))
+	    if (insertedShort && not AddWork(Work{insertedShort, decisionLevel()}))
 	       return false;
 
 	    // Discovery here is needed so the shortcircuit clause can actually become unit.
@@ -1300,7 +1300,7 @@ bool APT::Solver::FromDepCache(pkgDepCache &depcache)
 	 if (unlikely(debug >= 1))
 	    std::cerr << "Install essential package " << P << std::endl;
 	 auto inserted = RegisterClause(std::move(w));
-	 if (inserted && not AddWork(Work{inserted, depth()}))
+	 if (inserted && not AddWork(Work{inserted, decisionLevel()}))
 	    return false;
       }
    }
diff --git a/apt-pkg/solver3.h b/apt-pkg/solver3.h
index c4b87e9fe..eff2c50d6 100644
--- a/apt-pkg/solver3.h
+++ b/apt-pkg/solver3.h
@@ -89,7 +89,7 @@ class Solver
    struct State;
    struct Clause;
    struct Work;
-   struct Solved;
+   struct Trail;
    friend struct std::hash<APT::Solver::Var>;
    friend struct std::hash<APT::Solver::Lit>;
 
@@ -202,30 +202,25 @@ class Solver
 
    // \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<depth_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{};
 
@@ -273,10 +268,10 @@ class Solver
    // \brief Propagate all pending propagations
    [[nodiscard]] bool Propagate();
 
-   // \brief Return the current depth (choices.size() with casting)
-   depth_type depth()
+   // \brief Return the current depth (.size() with casting)
+   depth_type decisionLevel()
    {
-      return static_cast<depth_type>(choices.size());
+      return static_cast<depth_type>(trailLim.size());
    }
    inline Var bestReason(Clause const *clause, Var var) const;
    inline LiftedBool value(Lit lit) const;
@@ -286,7 +281,7 @@ class Solver
    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);
@@ -472,7 +467,7 @@ struct APT::Solver::Work
    // \brief The depth at which the item has been added
    depth_type depth;
 
-   // Number of valid choices
+   /// Number of valid choices at insertion time
    size_t size{0};
 
    // \brief This item should be removed from the queue.
@@ -539,16 +534,22 @@ struct APT::Solver::State
 };
 
 /**
- * \brief A solved item.
+ * \brief A trail item.
+ *
+ * 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.
  *
- * Here we keep track of solved clauses and variable assignments such that we can easily undo
- * them.
+ * 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::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;
 };