Refactor handling of conflict set representing option to not choose a goal.

The conflict set that represents the option to not choose a value for a goal,
'initial', has two purposes:

1. 'initial' contributes to a node's conflict set, because it is unioned with
   the other conflict sets under the same choice node, if the current variable
   is contained in all of them.
2. 'initial' contributes to the conflict count.  When it is unioned with the
   other conflict sets, it is also added to the ConflictMap.

Previously, 'initial' was treated as the first of a node's children for (1) and
the last of the children for (2).  This refactoring treats 'initial' as the last
child in both cases, to make the code clearer, and renames it to 'lastCS'.
There should be no change in behavior.

cabal-install/Distribution/Solver/Modular/Explore.hs

@@ -21,8 +21,8 @@ import qualified Distribution.Solver.Modular.WeightedPSQ as W
 import Distribution.Solver.Types.PackagePath
 import Distribution.Solver.Types.Settings (EnableBackjumping(..), CountConflicts(..))
 
--- | This function takes the variable we're currently considering, an
--- initial conflict set and a
+-- | This function takes the variable we're currently considering, a
+-- last conflict set and a
 -- list of children's logs. Each log yields either a solution or a
 -- conflict set. The result is a combined log for the parent node that
 -- has explored a prefix of the children.
@@ -38,7 +38,7 @@ import Distribution.Solver.Types.Settings (EnableBackjumping(..), CountConflicts
 -- return it immediately. If all children contain conflict sets, we can
 -- take the union as the combined conflict set.
 --
--- The initial conflict set corresponds to the justification that we
+-- The last conflict set corresponds to the justification that we
 -- have to choose this goal at all. There is a reason why we have
 -- introduced the goal in the first place, and this reason is in conflict
 -- with the (virtual) option not to choose anything for the current
@@ -47,11 +47,8 @@ import Distribution.Solver.Types.Settings (EnableBackjumping(..), CountConflicts
 backjump :: EnableBackjumping -> Var QPN
          -> ConflictSet -> W.WeightedPSQ w k (ConflictMap -> ConflictSetLog a)
          -> ConflictMap -> ConflictSetLog a
-backjump (EnableBackjumping enableBj) var initial xs =
-    F.foldr combine (\cs !cm -> logBackjump cs $ updateCM initial cm) xs initial
-                      -- 'intial' instead of 'cs' here ---^
-                      -- since we do not want to double-count the
-                      -- additionally accumulated conflicts.
+backjump (EnableBackjumping enableBj) var lastCS xs =
+    F.foldr combine avoidGoal xs CS.empty
   where
     combine :: forall a . (ConflictMap -> ConflictSetLog a)
             -> (ConflictSet -> ConflictMap -> ConflictSetLog a)
@@ -63,6 +60,13 @@ backjump (EnableBackjumping enableBj) var initial xs =
           | enableBj && not (var `CS.member` cs) = logBackjump cs cm'
           | otherwise                            = f (csAcc `CS.union` cs) cm'
 
+    -- This function represents the option to not choose a value for this goal.
+    avoidGoal :: ConflictSet -> ConflictMap -> ConflictSetLog a
+    avoidGoal cs !cm = logBackjump (cs `CS.union` lastCS) (updateCM lastCS cm)
+                                -- 'lastCS' instead of 'cs' here ---^
+                                -- since we do not want to double-count the
+                                -- additionally accumulated conflicts.
+
     logBackjump :: ConflictSet -> ConflictMap -> ConflictSetLog a
     logBackjump cs cm = failWith (Failure cs Backjump) (cs, cm)
 
@@ -151,12 +155,12 @@ exploreLog enableBj (CountConflicts countConflicts) t = cata go t M.empty
 -- that the goal cannot be avoided. This is tracked in the "goal reason".
 -- The choice to avoid the goal therefore is a conflict between the goal itself
 -- and its goal reason. We build this set here, and pass it to the 'backjump'
--- function as the initial conflict set.
+-- function as the last conflict set.
 --
 -- This has two effects:
 --
 -- - In a situation where there are no choices available at all (this happens
--- if an unknown package is requested), the initial conflict set becomes the
+-- if an unknown package is requested), the last conflict set becomes the
 -- actual conflict set.
 --
 -- - In a situation where all of the children's conflict sets contain the