    {-# LANGUAGE BangPatterns #-}
    {-# LANGUAGE LambdaCase #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    module Distribution.Solver.Modular.Explore (backjumpAndExplore) where

    import Distribution.Solver.Compat.Prelude
    import Prelude ()

    import qualified Distribution.Solver.Types.Progress as P

    import qualified Data.List as L (foldl')
    import qualified Data.Map.Strict as M
    import qualified Data.Set as S

    import Distribution.Simple.Setup (asBool)

    import Distribution.Solver.Modular.Assignment
    import Distribution.Solver.Modular.Dependency
    import Distribution.Solver.Modular.Index
    import Distribution.Solver.Modular.Log
    import Distribution.Solver.Modular.Message
    import Distribution.Solver.Modular.Package
    import qualified Distribution.Solver.Modular.PSQ as P
    import qualified Distribution.Solver.Modular.ConflictSet as CS
    import Distribution.Solver.Modular.RetryLog
    import Distribution.Solver.Modular.Tree
    import Distribution.Solver.Modular.Version
    import qualified Distribution.Solver.Modular.WeightedPSQ as W
    import Distribution.Solver.Types.PackagePath
    import Distribution.Solver.Types.Settings
             (CountConflicts(..), EnableBackjumping(..), FineGrainedConflicts(..))
    import Distribution.Types.VersionRange (anyVersion)

    -- | 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.
    --
    -- We can stop traversing the children's logs if we find an individual
    -- conflict set that does not contain the current variable. In this
    -- case, we can just lift the conflict set to the current level,
    -- because the current level cannot possibly have contributed to this
    -- conflict, so no other choice at the current level would avoid the
    -- conflict.
    --
    -- If any of the children might contain a successful solution, we can
    -- return it immediately. If all children contain conflict sets, we can
    -- take the union as the combined conflict set.
    --
    -- 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
    -- variable. See also the comments for 'avoidSet'.
    --
    -- We can also skip a child if it does not resolve any of the conflicts paired
    -- with the current variable in the previous child's conflict set. 'backjump'
    -- takes a function to determine whether a child can be skipped. If the child
    -- can be skipped, the function returns a new conflict set to be merged with the
    -- previous conflict set.
    --
    backjump :: forall w k a . Maybe Int
             -> EnableBackjumping
             -> FineGrainedConflicts

             -> (k -> S.Set CS.Conflict -> Maybe ConflictSet)
                -- ^ Function that determines whether the given choice could resolve
                --   the given conflict. It indicates false by returning 'Just',
                --   with the new conflicts to be added to the conflict set.

             -> (k -> ConflictSet -> ExploreState -> ConflictSetLog a)
                -- ^ Function that logs the given choice that was skipped.

             -> Var QPN -- ^ The current variable.

             -> ConflictSet -- ^ Conflict set representing the reason that the goal
                            --   was introduced.

             -> W.WeightedPSQ w k (ExploreState -> ConflictSetLog a)
                -- ^ List of children's logs.

             -> ExploreState -> ConflictSetLog a
    backjump :: forall w k a.
    Maybe Int
    -> EnableBackjumping
    -> FineGrainedConflicts
    -> (k -> Set Conflict -> Maybe ConflictSet)
    -> (k -> ConflictSet -> ExploreState -> ConflictSetLog a)
    -> Var QPN
    -> ConflictSet
    -> WeightedPSQ w k (ExploreState -> ConflictSetLog a)
    -> ExploreState
    -> ConflictSetLog a
    backjump Maybe Int
    mbj EnableBackjumping
    enableBj FineGrainedConflicts
    fineGrainedConflicts k -> Set Conflict -> Maybe ConflictSet
    couldResolveConflicts
             k -> ConflictSet -> ExploreState -> ConflictSetLog a
    logSkippedChoice Var QPN
    var ConflictSet
    lastCS WeightedPSQ w k (ExploreState -> ConflictSetLog a)
    xs =
        ((k, ExploreState -> ConflictSetLog a)
     -> (ConflictSet
         -> Maybe ConflictSet -> ExploreState -> ConflictSetLog a)
     -> ConflictSet
     -> Maybe ConflictSet
     -> ExploreState
     -> ConflictSetLog a)
    -> (ConflictSet
        -> Maybe ConflictSet -> ExploreState -> ConflictSetLog a)
    -> [(k, ExploreState -> ConflictSetLog a)]
    -> ConflictSet
    -> Maybe ConflictSet
    -> ExploreState
    -> ConflictSetLog a
    forall a b. (a -> b -> b) -> b -> [a] -> b
    forall (t :: * -> *) a b.
    Foldable t =>
    (a -> b -> b) -> b -> t a -> b
    foldr (k, ExploreState -> ConflictSetLog a)
    -> (ConflictSet
        -> Maybe ConflictSet -> ExploreState -> ConflictSetLog a)
    -> ConflictSet
    -> Maybe ConflictSet
    -> ExploreState
    -> ConflictSetLog a
    combine ConflictSet
    -> Maybe ConflictSet -> ExploreState -> ConflictSetLog a
    avoidGoal [(k
    k, ExploreState -> ConflictSetLog a
    v) | (w
    _, k
    k, ExploreState -> ConflictSetLog a
    v) <- WeightedPSQ w k (ExploreState -> ConflictSetLog a)
    -> [(w, k, ExploreState -> ConflictSetLog a)]
    forall w k v. WeightedPSQ w k v -> [(w, k, v)]
    W.toList WeightedPSQ w k (ExploreState -> ConflictSetLog a)
    xs] ConflictSet
    CS.empty Maybe ConflictSet
    forall a. Maybe a
    Nothing
      where
        combine :: (k, ExploreState -> ConflictSetLog a)
                -> (ConflictSet -> Maybe ConflictSet -> ExploreState -> ConflictSetLog a)
                ->  ConflictSet -> Maybe ConflictSet -> ExploreState -> ConflictSetLog a
        combine :: (k, ExploreState -> ConflictSetLog a)
    -> (ConflictSet
        -> Maybe ConflictSet -> ExploreState -> ConflictSetLog a)
    -> ConflictSet
    -> Maybe ConflictSet
    -> ExploreState
    -> ConflictSetLog a
    combine (k
    k, ExploreState -> ConflictSetLog a
    x) ConflictSet
    -> Maybe ConflictSet -> ExploreState -> ConflictSetLog a
    f ConflictSet
    csAcc Maybe ConflictSet
    mPreviousCS ExploreState
    es =
            case (FineGrainedConflicts -> Bool
    forall a. BooleanFlag a => a -> Bool
    asBool FineGrainedConflicts
    fineGrainedConflicts, Maybe ConflictSet
    mPreviousCS) of
              (Bool
    True, Just ConflictSet
    previousCS) ->
                  case Var QPN -> ConflictSet -> Maybe (Set Conflict)
    CS.lookup Var QPN
    var ConflictSet
    previousCS of
                    Just Set Conflict
    conflicts ->
                      case k -> Set Conflict -> Maybe ConflictSet
    couldResolveConflicts k
    k Set Conflict
    conflicts of
                        Maybe ConflictSet
    Nothing           -> ConflictSetLog a
    -> (ConflictSet -> ExploreState -> ConflictSetLog a)
    -> ConflictSetLog a
    forall a.
    ConflictSetLog a
    -> (ConflictSet -> ExploreState -> ConflictSetLog a)
    -> ConflictSetLog a
    retryNoSolution (ExploreState -> ConflictSetLog a
    x ExploreState
    es) ConflictSet -> ExploreState -> ConflictSetLog a
    next
                        Just ConflictSet
    newConflicts -> ConflictSet -> ConflictSetLog a
    skipChoice (ConflictSet
    previousCS ConflictSet -> ConflictSet -> ConflictSet
    `CS.union` ConflictSet
    newConflicts)
                    Maybe (Set Conflict)
    _              -> ConflictSet -> ConflictSetLog a
    skipChoice ConflictSet
    previousCS
              (Bool, Maybe ConflictSet)
    _                       -> ConflictSetLog a
    -> (ConflictSet -> ExploreState -> ConflictSetLog a)
    -> ConflictSetLog a
    forall a.
    ConflictSetLog a
    -> (ConflictSet -> ExploreState -> ConflictSetLog a)
    -> ConflictSetLog a
    retryNoSolution (ExploreState -> ConflictSetLog a
    x ExploreState
    es) ConflictSet -> ExploreState -> ConflictSetLog a
    next
          where
            next :: ConflictSet -> ExploreState -> ConflictSetLog a
            next :: ConflictSet -> ExploreState -> ConflictSetLog a
    next !ConflictSet
    cs ExploreState
    es' = if EnableBackjumping -> Bool
    forall a. BooleanFlag a => a -> Bool
    asBool EnableBackjumping
    enableBj Bool -> Bool -> Bool
    && Bool -> Bool
    not (Var QPN
    var Var QPN -> ConflictSet -> Bool
    `CS.member` ConflictSet
    cs)
                           then ConflictSet -> ExploreState -> ConflictSetLog a
    skipLoggingBackjump ConflictSet
    cs ExploreState
    es'
                           else ConflictSet
    -> Maybe ConflictSet -> ExploreState -> ConflictSetLog a
    f (ConflictSet
    csAcc ConflictSet -> ConflictSet -> ConflictSet
    `CS.union` ConflictSet
    cs) (ConflictSet -> Maybe ConflictSet
    forall a. a -> Maybe a
    Just ConflictSet
    cs) ExploreState
    es'

            -- This function is for skipping the choice when it cannot resolve any
            -- of the previous conflicts.
            skipChoice :: ConflictSet -> ConflictSetLog a
            skipChoice :: ConflictSet -> ConflictSetLog a
    skipChoice ConflictSet
    newCS =
                ConflictSetLog a
    -> (ConflictSet -> ExploreState -> ConflictSetLog a)
    -> ConflictSetLog a
    forall a.
    ConflictSetLog a
    -> (ConflictSet -> ExploreState -> ConflictSetLog a)
    -> ConflictSetLog a
    retryNoSolution (k -> ConflictSet -> ExploreState -> ConflictSetLog a
    logSkippedChoice k
    k ConflictSet
    newCS ExploreState
    es) ((ConflictSet -> ExploreState -> ConflictSetLog a)
     -> ConflictSetLog a)
    -> (ConflictSet -> ExploreState -> ConflictSetLog a)
    -> ConflictSetLog a
    forall a b. (a -> b) -> a -> b
    $ \ConflictSet
    cs' ExploreState
    es' ->
                    ConflictSet
    -> Maybe ConflictSet -> ExploreState -> ConflictSetLog a
    f (ConflictSet
    csAcc ConflictSet -> ConflictSet -> ConflictSet
    `CS.union` ConflictSet
    cs') (ConflictSet -> Maybe ConflictSet
    forall a. a -> Maybe a
    Just ConflictSet
    cs') (ExploreState -> ConflictSetLog a)
    -> ExploreState -> ConflictSetLog a
    forall a b. (a -> b) -> a -> b
    $

                    -- Update the conflict map with the conflict set, to make up for
                    -- skipping the whole subtree.
                    ExploreState
    es' { esConflictMap = updateCM cs' (esConflictMap es') }

        -- This function represents the option to not choose a value for this goal.
        avoidGoal :: ConflictSet -> Maybe ConflictSet -> ExploreState -> ConflictSetLog a
        avoidGoal :: ConflictSet
    -> Maybe ConflictSet -> ExploreState -> ConflictSetLog a
    avoidGoal ConflictSet
    cs Maybe ConflictSet
    _mPreviousCS !ExploreState
    es =
            Maybe Int -> ConflictSet -> ExploreState -> ConflictSetLog a
    forall a.
    Maybe Int -> ConflictSet -> ExploreState -> ConflictSetLog a
    logBackjump Maybe Int
    mbj (ConflictSet
    cs ConflictSet -> ConflictSet -> ConflictSet
    `CS.union` ConflictSet
    lastCS) (ExploreState -> ConflictSetLog a)
    -> ExploreState -> ConflictSetLog a
    forall a b. (a -> b) -> a -> b
    $

            -- Use 'lastCS' below instead of 'cs' since we do not want to
            -- double-count the additionally accumulated conflicts.
            ExploreState
    es { esConflictMap = updateCM lastCS (esConflictMap es) }

        -- The solver does not count or log backjumps at levels where the conflict
        -- set does not contain the current variable. Otherwise, there would be many
        -- consecutive log messages about backjumping with the same conflict set.
        skipLoggingBackjump :: ConflictSet -> ExploreState -> ConflictSetLog a
        skipLoggingBackjump :: ConflictSet -> ExploreState -> ConflictSetLog a
    skipLoggingBackjump ConflictSet
    cs ExploreState
    es = Progress Message IntermediateFailure a -> ConflictSetLog a
    forall step fail done.
    Progress step fail done -> RetryLog step fail done
    fromProgress (Progress Message IntermediateFailure a -> ConflictSetLog a)
    -> Progress Message IntermediateFailure a -> ConflictSetLog a
    forall a b. (a -> b) -> a -> b
    $ IntermediateFailure -> Progress Message IntermediateFailure a
    forall step fail done. fail -> Progress step fail done
    P.Fail (ConflictSet -> ExploreState -> IntermediateFailure
    NoSolution ConflictSet
    cs ExploreState
    es)

    -- | Creates a failing ConflictSetLog representing a backjump. It inserts a
    -- "backjumping" message, checks whether the backjump limit has been reached,
    -- and increments the backjump count.
    logBackjump :: Maybe Int -> ConflictSet -> ExploreState -> ConflictSetLog a
    logBackjump :: forall a.
    Maybe Int -> ConflictSet -> ExploreState -> ConflictSetLog a
    logBackjump Maybe Int
    mbj ConflictSet
    cs ExploreState
    es =
        Message
    -> IntermediateFailure -> RetryLog Message IntermediateFailure a
    forall step fail done. step -> fail -> RetryLog step fail done
    failWith (ConflictSet -> FailReason -> Message
    Failure ConflictSet
    cs FailReason
    Backjump) (IntermediateFailure -> RetryLog Message IntermediateFailure a)
    -> IntermediateFailure -> RetryLog Message IntermediateFailure a
    forall a b. (a -> b) -> a -> b
    $
            if Int -> Bool
    reachedBjLimit (ExploreState -> Int
    esBackjumps ExploreState
    es)
            then IntermediateFailure
    BackjumpLimit
            else ConflictSet -> ExploreState -> IntermediateFailure
    NoSolution ConflictSet
    cs ExploreState
    es { esBackjumps = esBackjumps es + 1 }
      where
        reachedBjLimit :: Int -> Bool
    reachedBjLimit = case Maybe Int
    mbj of
                           Maybe Int
    Nothing    -> Bool -> Int -> Bool
    forall a b. a -> b -> a
    const Bool
    False
                           Just Int
    limit -> (Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    limit)

    -- | Like 'retry', except that it only applies the input function when the
    -- backjump limit has not been reached.
    retryNoSolution :: ConflictSetLog a
                    -> (ConflictSet -> ExploreState -> ConflictSetLog a)
                    -> ConflictSetLog a
    retryNoSolution :: forall a.
    ConflictSetLog a
    -> (ConflictSet -> ExploreState -> ConflictSetLog a)
    -> ConflictSetLog a
    retryNoSolution ConflictSetLog a
    lg ConflictSet -> ExploreState -> ConflictSetLog a
    f = ConflictSetLog a
    -> (IntermediateFailure -> ConflictSetLog a) -> ConflictSetLog a
    forall step fail1 done fail2.
    RetryLog step fail1 done
    -> (fail1 -> RetryLog step fail2 done) -> RetryLog step fail2 done
    retry ConflictSetLog a
    lg ((IntermediateFailure -> ConflictSetLog a) -> ConflictSetLog a)
    -> (IntermediateFailure -> ConflictSetLog a) -> ConflictSetLog a
    forall a b. (a -> b) -> a -> b
    $ \case
        IntermediateFailure
    BackjumpLimit    -> Progress Message IntermediateFailure a -> ConflictSetLog a
    forall step fail done.
    Progress step fail done -> RetryLog step fail done
    fromProgress (IntermediateFailure -> Progress Message IntermediateFailure a
    forall step fail done. fail -> Progress step fail done
    P.Fail IntermediateFailure
    BackjumpLimit)
        NoSolution ConflictSet
    cs ExploreState
    es -> ConflictSet -> ExploreState -> ConflictSetLog a
    f ConflictSet
    cs ExploreState
    es

    -- | The state that is read and written while exploring the search tree.
    data ExploreState = ES {
        ExploreState -> ConflictMap
    esConflictMap :: !ConflictMap
      , ExploreState -> Int
    esBackjumps   :: !Int
      }

    data IntermediateFailure =
        NoSolution ConflictSet ExploreState
      | BackjumpLimit

    type ConflictSetLog = RetryLog Message IntermediateFailure

    getBestGoal :: ConflictMap -> P.PSQ (Goal QPN) a -> (Goal QPN, a)
    getBestGoal :: forall a. ConflictMap -> PSQ (Goal QPN) a -> (Goal QPN, a)
    getBestGoal ConflictMap
    cm =
      (Goal QPN -> Int) -> PSQ (Goal QPN) a -> (Goal QPN, a)
    forall k a. (k -> Int) -> PSQ k a -> (k, a)
    P.maximumBy
        ( (Var QPN -> ConflictMap -> Int) -> ConflictMap -> Var QPN -> Int
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (Int -> Var QPN -> ConflictMap -> Int
    forall k a. Ord k => a -> k -> Map k a -> a
    M.findWithDefault Int
    0) ConflictMap
    cm
        (Var QPN -> Int) -> (Goal QPN -> Var QPN) -> Goal QPN -> Int
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (\ (Goal Var QPN
    v GoalReason QPN
    _) -> Var QPN
    v)
        )

    getFirstGoal :: P.PSQ (Goal QPN) a -> (Goal QPN, a)
    getFirstGoal :: forall a. PSQ (Goal QPN) a -> (Goal QPN, a)
    getFirstGoal PSQ (Goal QPN) a
    ts =
      PSQ (Goal QPN) a
    -> (Goal QPN, a)
    -> (Goal QPN -> a -> PSQ (Goal QPN) a -> (Goal QPN, a))
    -> (Goal QPN, a)
    forall k a r. PSQ k a -> r -> (k -> a -> PSQ k a -> r) -> r
    P.casePSQ PSQ (Goal QPN) a
    ts
        ([Char] -> (Goal QPN, a)
    forall a. HasCallStack => [Char] -> a
    error [Char]
    "getFirstGoal: empty goal choice") -- empty goal choice is an internal error
        (\ Goal QPN
    k a
    v PSQ (Goal QPN) a
    _xs -> (Goal QPN
    k, a
    v))  -- commit to the first goal choice

    updateCM :: ConflictSet -> ConflictMap -> ConflictMap
    updateCM :: ConflictSet -> ConflictMap -> ConflictMap
    updateCM ConflictSet
    cs ConflictMap
    cm =
      (ConflictMap -> Var QPN -> ConflictMap)
    -> ConflictMap -> [Var QPN] -> ConflictMap
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    L.foldl' (\ ConflictMap
    cmc Var QPN
    k -> (Int -> Int -> Int) -> Var QPN -> Int -> ConflictMap -> ConflictMap
    forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
    M.insertWith Int -> Int -> Int
    forall a. Num a => a -> a -> a
    (+) Var QPN
    k Int
    1 ConflictMap
    cmc) ConflictMap
    cm (ConflictSet -> [Var QPN]
    CS.toList ConflictSet
    cs)

    -- | Record complete assignments on 'Done' nodes.
    assign :: Tree d c -> Tree Assignment c
    assign :: forall d c. Tree d c -> Tree Assignment c
    assign Tree d c
    tree = Tree d c -> Assignment -> Tree Assignment c
    forall d c. Tree d c -> Assignment -> Tree Assignment c
    go Tree d c
    tree (PAssignment -> FAssignment -> SAssignment -> Assignment
    A PAssignment
    forall k a. Map k a
    M.empty FAssignment
    forall k a. Map k a
    M.empty SAssignment
    forall k a. Map k a
    M.empty)
      where
        go :: Tree d c -> Assignment -> Tree Assignment c
        go :: forall d c. Tree d c -> Assignment -> Tree Assignment c
    go (Fail ConflictSet
    c FailReason
    fr)            Assignment
    _                  = ConflictSet -> FailReason -> Tree Assignment c
    forall d c. ConflictSet -> FailReason -> Tree d c
    Fail ConflictSet
    c FailReason
    fr
        go (Done RevDepMap
    rdm d
    _)           Assignment
    a                  = RevDepMap -> Assignment -> Tree Assignment c
    forall d c. RevDepMap -> d -> Tree d c
    Done RevDepMap
    rdm Assignment
    a
        go (PChoice QPN
    qpn RevDepMap
    rdm c
    y       WeightedPSQ [Weight] POption (Tree d c)
    ts) (A PAssignment
    pa FAssignment
    fa SAssignment
    sa) = QPN
    -> RevDepMap
    -> c
    -> WeightedPSQ [Weight] POption (Tree Assignment c)
    -> Tree Assignment c
    forall d c.
    QPN
    -> RevDepMap
    -> c
    -> WeightedPSQ [Weight] POption (Tree d c)
    -> Tree d c
    PChoice QPN
    qpn RevDepMap
    rdm c
    y       (WeightedPSQ [Weight] POption (Tree Assignment c)
     -> Tree Assignment c)
    -> WeightedPSQ [Weight] POption (Tree Assignment c)
    -> Tree Assignment c
    forall a b. (a -> b) -> a -> b
    $ (POption -> (Assignment -> Tree Assignment c) -> Tree Assignment c)
    -> WeightedPSQ [Weight] POption (Assignment -> Tree Assignment c)
    -> WeightedPSQ [Weight] POption (Tree Assignment c)
    forall k v1 v2 w.
    (k -> v1 -> v2) -> WeightedPSQ w k v1 -> WeightedPSQ w k v2
    W.mapWithKey POption -> (Assignment -> Tree Assignment c) -> Tree Assignment c
    forall {t}. POption -> (Assignment -> t) -> t
    f ((Tree d c -> Assignment -> Tree Assignment c)
    -> WeightedPSQ [Weight] POption (Tree d c)
    -> WeightedPSQ [Weight] POption (Assignment -> Tree Assignment c)
    forall a b.
    (a -> b)
    -> WeightedPSQ [Weight] POption a -> WeightedPSQ [Weight] POption b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Tree d c -> Assignment -> Tree Assignment c
    forall d c. Tree d c -> Assignment -> Tree Assignment c
    go WeightedPSQ [Weight] POption (Tree d c)
    ts)
            where f :: POption -> (Assignment -> t) -> t
    f (POption I
    k Maybe PackagePath
    _) Assignment -> t
    r = Assignment -> t
    r (PAssignment -> FAssignment -> SAssignment -> Assignment
    A (QPN -> I -> PAssignment -> PAssignment
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert QPN
    qpn I
    k PAssignment
    pa) FAssignment
    fa SAssignment
    sa)
        go (FChoice QFN
    qfn RevDepMap
    rdm c
    y WeakOrTrivial
    t FlagType
    m Bool
    d WeightedPSQ [Weight] Bool (Tree d c)
    ts) (A PAssignment
    pa FAssignment
    fa SAssignment
    sa) = QFN
    -> RevDepMap
    -> c
    -> WeakOrTrivial
    -> FlagType
    -> Bool
    -> WeightedPSQ [Weight] Bool (Tree Assignment c)
    -> Tree Assignment c
    forall d c.
    QFN
    -> RevDepMap
    -> c
    -> WeakOrTrivial
    -> FlagType
    -> Bool
    -> WeightedPSQ [Weight] Bool (Tree d c)
    -> Tree d c
    FChoice QFN
    qfn RevDepMap
    rdm c
    y WeakOrTrivial
    t FlagType
    m Bool
    d (WeightedPSQ [Weight] Bool (Tree Assignment c)
     -> Tree Assignment c)
    -> WeightedPSQ [Weight] Bool (Tree Assignment c)
    -> Tree Assignment c
    forall a b. (a -> b) -> a -> b
    $ (Bool -> (Assignment -> Tree Assignment c) -> Tree Assignment c)
    -> WeightedPSQ [Weight] Bool (Assignment -> Tree Assignment c)
    -> WeightedPSQ [Weight] Bool (Tree Assignment c)
    forall k v1 v2 w.
    (k -> v1 -> v2) -> WeightedPSQ w k v1 -> WeightedPSQ w k v2
    W.mapWithKey Bool -> (Assignment -> Tree Assignment c) -> Tree Assignment c
    forall {t}. Bool -> (Assignment -> t) -> t
    f ((Tree d c -> Assignment -> Tree Assignment c)
    -> WeightedPSQ [Weight] Bool (Tree d c)
    -> WeightedPSQ [Weight] Bool (Assignment -> Tree Assignment c)
    forall a b.
    (a -> b)
    -> WeightedPSQ [Weight] Bool a -> WeightedPSQ [Weight] Bool b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Tree d c -> Assignment -> Tree Assignment c
    forall d c. Tree d c -> Assignment -> Tree Assignment c
    go WeightedPSQ [Weight] Bool (Tree d c)
    ts)
            where f :: Bool -> (Assignment -> t) -> t
    f Bool
    k             Assignment -> t
    r = Assignment -> t
    r (PAssignment -> FAssignment -> SAssignment -> Assignment
    A PAssignment
    pa (QFN -> Bool -> FAssignment -> FAssignment
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert QFN
    qfn Bool
    k FAssignment
    fa) SAssignment
    sa)
        go (SChoice QSN
    qsn RevDepMap
    rdm c
    y WeakOrTrivial
    t     WeightedPSQ [Weight] Bool (Tree d c)
    ts) (A PAssignment
    pa FAssignment
    fa SAssignment
    sa) = QSN
    -> RevDepMap
    -> c
    -> WeakOrTrivial
    -> WeightedPSQ [Weight] Bool (Tree Assignment c)
    -> Tree Assignment c
    forall d c.
    QSN
    -> RevDepMap
    -> c
    -> WeakOrTrivial
    -> WeightedPSQ [Weight] Bool (Tree d c)
    -> Tree d c
    SChoice QSN
    qsn RevDepMap
    rdm c
    y WeakOrTrivial
    t     (WeightedPSQ [Weight] Bool (Tree Assignment c)
     -> Tree Assignment c)
    -> WeightedPSQ [Weight] Bool (Tree Assignment c)
    -> Tree Assignment c
    forall a b. (a -> b) -> a -> b
    $ (Bool -> (Assignment -> Tree Assignment c) -> Tree Assignment c)
    -> WeightedPSQ [Weight] Bool (Assignment -> Tree Assignment c)
    -> WeightedPSQ [Weight] Bool (Tree Assignment c)
    forall k v1 v2 w.
    (k -> v1 -> v2) -> WeightedPSQ w k v1 -> WeightedPSQ w k v2
    W.mapWithKey Bool -> (Assignment -> Tree Assignment c) -> Tree Assignment c
    forall {t}. Bool -> (Assignment -> t) -> t
    f ((Tree d c -> Assignment -> Tree Assignment c)
    -> WeightedPSQ [Weight] Bool (Tree d c)
    -> WeightedPSQ [Weight] Bool (Assignment -> Tree Assignment c)
    forall a b.
    (a -> b)
    -> WeightedPSQ [Weight] Bool a -> WeightedPSQ [Weight] Bool b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Tree d c -> Assignment -> Tree Assignment c
    forall d c. Tree d c -> Assignment -> Tree Assignment c
    go WeightedPSQ [Weight] Bool (Tree d c)
    ts)
            where f :: Bool -> (Assignment -> t) -> t
    f Bool
    k             Assignment -> t
    r = Assignment -> t
    r (PAssignment -> FAssignment -> SAssignment -> Assignment
    A PAssignment
    pa FAssignment
    fa (QSN -> Bool -> SAssignment -> SAssignment
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert QSN
    qsn Bool
    k SAssignment
    sa))
        go (GoalChoice  RevDepMap
    rdm         PSQ (Goal QPN) (Tree d c)
    ts) Assignment
    a            = RevDepMap
    -> PSQ (Goal QPN) (Tree Assignment c) -> Tree Assignment c
    forall d c. RevDepMap -> PSQ (Goal QPN) (Tree d c) -> Tree d c
    GoalChoice  RevDepMap
    rdm         (PSQ (Goal QPN) (Tree Assignment c) -> Tree Assignment c)
    -> PSQ (Goal QPN) (Tree Assignment c) -> Tree Assignment c
    forall a b. (a -> b) -> a -> b
    $ ((Assignment -> Tree Assignment c) -> Tree Assignment c)
    -> PSQ (Goal QPN) (Assignment -> Tree Assignment c)
    -> PSQ (Goal QPN) (Tree Assignment c)
    forall a b. (a -> b) -> PSQ (Goal QPN) a -> PSQ (Goal QPN) b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((Assignment -> Tree Assignment c)
    -> Assignment -> Tree Assignment c
    forall a b. (a -> b) -> a -> b
    $ Assignment
    a) ((Tree d c -> Assignment -> Tree Assignment c)
    -> PSQ (Goal QPN) (Tree d c)
    -> PSQ (Goal QPN) (Assignment -> Tree Assignment c)
    forall a b. (a -> b) -> PSQ (Goal QPN) a -> PSQ (Goal QPN) b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap Tree d c -> Assignment -> Tree Assignment c
    forall d c. Tree d c -> Assignment -> Tree Assignment c
    go PSQ (Goal QPN) (Tree d c)
    ts)

    -- | A tree traversal that simultaneously propagates conflict sets up
    -- the tree from the leaves and creates a log.
    exploreLog :: Maybe Int
               -> EnableBackjumping
               -> FineGrainedConflicts
               -> CountConflicts
               -> Index
               -> Tree Assignment QGoalReason
               -> ConflictSetLog (Assignment, RevDepMap)
    exploreLog :: Maybe Int
    -> EnableBackjumping
    -> FineGrainedConflicts
    -> CountConflicts
    -> Index
    -> Tree Assignment (GoalReason QPN)
    -> ConflictSetLog (Assignment, RevDepMap)
    exploreLog Maybe Int
    mbj EnableBackjumping
    enableBj FineGrainedConflicts
    fineGrainedConflicts (CountConflicts Bool
    countConflicts) Index
    idx Tree Assignment (GoalReason QPN)
    t =
        (TreeF
       Assignment
       (GoalReason QPN)
       (ExploreState -> ConflictSetLog (Assignment, RevDepMap),
        Tree Assignment (GoalReason QPN))
     -> ExploreState -> ConflictSetLog (Assignment, RevDepMap))
    -> Tree Assignment (GoalReason QPN)
    -> ExploreState
    -> ConflictSetLog (Assignment, RevDepMap)
    forall d c a. (TreeF d c (a, Tree d c) -> a) -> Tree d c -> a
    para TreeF
      Assignment
      (GoalReason QPN)
      (ExploreState -> ConflictSetLog (Assignment, RevDepMap),
       Tree Assignment (GoalReason QPN))
    -> ExploreState -> ConflictSetLog (Assignment, RevDepMap)
    go Tree Assignment (GoalReason QPN)
    t ExploreState
    initES
      where
        getBestGoal' :: P.PSQ (Goal QPN) a -> ConflictMap -> (Goal QPN, a)
        getBestGoal' :: forall a. PSQ (Goal QPN) a -> ConflictMap -> (Goal QPN, a)
    getBestGoal'
          | Bool -> Bool
    forall a. BooleanFlag a => a -> Bool
    asBool Bool
    countConflicts = \ PSQ (Goal QPN) a
    ts ConflictMap
    cm -> ConflictMap -> PSQ (Goal QPN) a -> (Goal QPN, a)
    forall a. ConflictMap -> PSQ (Goal QPN) a -> (Goal QPN, a)
    getBestGoal ConflictMap
    cm PSQ (Goal QPN) a
    ts
          | Bool
    otherwise             = \ PSQ (Goal QPN) a
    ts ConflictMap
    _  -> PSQ (Goal QPN) a -> (Goal QPN, a)
    forall a. PSQ (Goal QPN) a -> (Goal QPN, a)
    getFirstGoal PSQ (Goal QPN) a
    ts

        go :: TreeF Assignment QGoalReason
                    (ExploreState -> ConflictSetLog (Assignment, RevDepMap), Tree Assignment QGoalReason)
                                        -> (ExploreState -> ConflictSetLog (Assignment, RevDepMap))
        go :: TreeF
      Assignment
      (GoalReason QPN)
      (ExploreState -> ConflictSetLog (Assignment, RevDepMap),
       Tree Assignment (GoalReason QPN))
    -> ExploreState -> ConflictSetLog (Assignment, RevDepMap)
    go (FailF ConflictSet
    c FailReason
    fr)                            = \ !ExploreState
    es ->
            let es' :: ExploreState
    es' = ExploreState
    es { esConflictMap = updateCM c (esConflictMap es) }
            in Message
    -> IntermediateFailure -> ConflictSetLog (Assignment, RevDepMap)
    forall step fail done. step -> fail -> RetryLog step fail done
    failWith (ConflictSet -> FailReason -> Message
    Failure ConflictSet
    c FailReason
    fr) (ConflictSet -> ExploreState -> IntermediateFailure
    NoSolution ConflictSet
    c ExploreState
    es')
        go (DoneF RevDepMap
    rdm Assignment
    a)                           = \ ExploreState
    _   -> Message
    -> (Assignment, RevDepMap)
    -> ConflictSetLog (Assignment, RevDepMap)
    forall step done fail. step -> done -> RetryLog step fail done
    succeedWith Message
    Success (Assignment
    a, RevDepMap
    rdm)
        go (PChoiceF QPN
    qpn RevDepMap
    _ GoalReason QPN
    gr       WeightedPSQ
      [Weight]
      POption
      (ExploreState -> ConflictSetLog (Assignment, RevDepMap),
       Tree Assignment (GoalReason QPN))
    ts)            =
          Maybe Int
    -> EnableBackjumping
    -> FineGrainedConflicts
    -> (POption -> Set Conflict -> Maybe ConflictSet)
    -> (POption
        -> ConflictSet
        -> ExploreState
        -> ConflictSetLog (Assignment, RevDepMap))
    -> Var QPN
    -> ConflictSet
    -> WeightedPSQ
         [Weight]
         POption
         (ExploreState -> ConflictSetLog (Assignment, RevDepMap))
    -> ExploreState
    -> ConflictSetLog (Assignment, RevDepMap)
    forall w k a.
    Maybe Int
    -> EnableBackjumping
    -> FineGrainedConflicts
    -> (k -> Set Conflict -> Maybe ConflictSet)
    -> (k -> ConflictSet -> ExploreState -> ConflictSetLog a)
    -> Var QPN
    -> ConflictSet
    -> WeightedPSQ w k (ExploreState -> ConflictSetLog a)
    -> ExploreState
    -> ConflictSetLog a
    backjump Maybe Int
    mbj EnableBackjumping
    enableBj FineGrainedConflicts
    fineGrainedConflicts
                   (QPN -> POption -> Set Conflict -> Maybe ConflictSet
    couldResolveConflicts QPN
    qpn)
                   (QPN
    -> POption
    -> ConflictSet
    -> ExploreState
    -> ConflictSetLog (Assignment, RevDepMap)
    forall a.
    QPN -> POption -> ConflictSet -> ExploreState -> ConflictSetLog a
    logSkippedPackage QPN
    qpn)
                   (QPN -> Var QPN
    forall qpn. qpn -> Var qpn
    P QPN
    qpn) (Var QPN -> GoalReason QPN -> ConflictSet
    avoidSet (QPN -> Var QPN
    forall qpn. qpn -> Var qpn
    P QPN
    qpn) GoalReason QPN
    gr) (WeightedPSQ
       [Weight]
       POption
       (ExploreState -> ConflictSetLog (Assignment, RevDepMap))
     -> ExploreState -> ConflictSetLog (Assignment, RevDepMap))
    -> WeightedPSQ
         [Weight]
         POption
         (ExploreState -> ConflictSetLog (Assignment, RevDepMap))
    -> ExploreState
    -> ConflictSetLog (Assignment, RevDepMap)
    forall a b. (a -> b) -> a -> b
    $ -- try children in order,
                   (POption
     -> (ExploreState -> ConflictSetLog (Assignment, RevDepMap))
     -> ExploreState
     -> ConflictSetLog (Assignment, RevDepMap))
    -> WeightedPSQ
         [Weight]
         POption
         (ExploreState -> ConflictSetLog (Assignment, RevDepMap))
    -> WeightedPSQ
         [Weight]
         POption
         (ExploreState -> ConflictSetLog (Assignment, RevDepMap))
    forall k v1 v2 w.
    (k -> v1 -> v2) -> WeightedPSQ w k v1 -> WeightedPSQ w k v2
    W.mapWithKey                    -- when descending ...
                     (\ POption
    k ExploreState -> ConflictSetLog (Assignment, RevDepMap)
    r ExploreState
    es -> Message
    -> ConflictSetLog (Assignment, RevDepMap)
    -> ConflictSetLog (Assignment, RevDepMap)
    forall fail done.
    Message -> RetryLog Message fail done -> RetryLog Message fail done
    tryWith (QPN -> POption -> Message
    TryP QPN
    qpn POption
    k) (ExploreState -> ConflictSetLog (Assignment, RevDepMap)
    r ExploreState
    es))
                     (((ExploreState -> ConflictSetLog (Assignment, RevDepMap),
      Tree Assignment (GoalReason QPN))
     -> ExploreState -> ConflictSetLog (Assignment, RevDepMap))
    -> WeightedPSQ
         [Weight]
         POption
         (ExploreState -> ConflictSetLog (Assignment, RevDepMap),
          Tree Assignment (GoalReason QPN))
    -> WeightedPSQ
         [Weight]
         POption
         (ExploreState -> ConflictSetLog (Assignment, RevDepMap))
    forall a b.
    (a -> b)
    -> WeightedPSQ [Weight] POption a -> WeightedPSQ [Weight] POption b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (ExploreState -> ConflictSetLog (Assignment, RevDepMap),
     Tree Assignment (GoalReason QPN))
    -> ExploreState -> ConflictSetLog (Assignment, RevDepMap)
    forall a b. (a, b) -> a
    fst WeightedPSQ
      [Weight]
      POption
      (ExploreState -> ConflictSetLog (Assignment, RevDepMap),
       Tree Assignment (GoalReason QPN))
    ts)
        go (FChoiceF QFN
    qfn RevDepMap
    _ GoalReason QPN
    gr WeakOrTrivial
    _ FlagType
    _ Bool
    _ WeightedPSQ
      [Weight]
      Bool
      (ExploreState -> ConflictSetLog (Assignment, RevDepMap),
       Tree Assignment (GoalReason QPN))
    ts)            =
          Maybe Int
    -> EnableBackjumping
    -> FineGrainedConflicts
    -> (Bool -> Set Conflict -> Maybe ConflictSet)
    -> (Bool
        -> ConflictSet
        -> ExploreState
        -> ConflictSetLog (Assignment, RevDepMap))
    -> Var QPN
    -> ConflictSet
    -> WeightedPSQ
         [Weight]
         Bool
         (ExploreState -> ConflictSetLog (Assignment, RevDepMap))
    -> ExploreState
    -> ConflictSetLog (Assignment, RevDepMap)
    forall w k a.
    Maybe Int
    -> EnableBackjumping
    -> FineGrainedConflicts
    -> (k -> Set Conflict -> Maybe ConflictSet)
    -> (k -> ConflictSet -> ExploreState -> ConflictSetLog a)
    -> Var QPN
    -> ConflictSet
    -> WeightedPSQ w k (ExploreState -> ConflictSetLog a)
    -> ExploreState
    -> ConflictSetLog a
    backjump Maybe Int
    mbj EnableBackjumping
    enableBj FineGrainedConflicts
    fineGrainedConflicts
                   (\Bool
    _ Set Conflict
    _ -> Maybe ConflictSet
    forall a. Maybe a
    Nothing)
                   ((ConflictSet
     -> ExploreState -> ConflictSetLog (Assignment, RevDepMap))
    -> Bool
    -> ConflictSet
    -> ExploreState
    -> ConflictSetLog (Assignment, RevDepMap)
    forall a b. a -> b -> a
    const ConflictSet
    -> ExploreState -> ConflictSetLog (Assignment, RevDepMap)
    forall a. ConflictSet -> ExploreState -> ConflictSetLog a
    logSkippedChoiceSimple)
                   (QFN -> Var QPN
    forall qpn. FN qpn -> Var qpn
    F QFN
    qfn) (Var QPN -> GoalReason QPN -> ConflictSet
    avoidSet (QFN -> Var QPN
    forall qpn. FN qpn -> Var qpn
    F QFN
    qfn) GoalReason QPN
    gr) (WeightedPSQ
       [Weight]
       Bool
       (ExploreState -> ConflictSetLog (Assignment, RevDepMap))
     -> ExploreState -> ConflictSetLog (Assignment, RevDepMap))
    -> WeightedPSQ
         [Weight]
         Bool
         (ExploreState -> ConflictSetLog (Assignment, RevDepMap))
    -> ExploreState
    -> ConflictSetLog (Assignment, RevDepMap)
    forall a b. (a -> b) -> a -> b
    $ -- try children in order,
                   (Bool
     -> (ExploreState -> ConflictSetLog (Assignment, RevDepMap))
     -> ExploreState
     -> ConflictSetLog (Assignment, RevDepMap))
    -> WeightedPSQ
         [Weight]
         Bool
         (ExploreState -> ConflictSetLog (Assignment, RevDepMap))
    -> WeightedPSQ
         [Weight]
         Bool
         (ExploreState -> ConflictSetLog (Assignment, RevDepMap))
    forall k v1 v2 w.
    (k -> v1 -> v2) -> WeightedPSQ w k v1 -> WeightedPSQ w k v2
    W.mapWithKey                    -- when descending ...
                     (\ Bool
    k ExploreState -> ConflictSetLog (Assignment, RevDepMap)
    r ExploreState
    es -> Message
    -> ConflictSetLog (Assignment, RevDepMap)
    -> ConflictSetLog (Assignment, RevDepMap)
    forall fail done.
    Message -> RetryLog Message fail done -> RetryLog Message fail done
    tryWith (QFN -> Bool -> Message
    TryF QFN
    qfn Bool
    k) (ExploreState -> ConflictSetLog (Assignment, RevDepMap)
    r ExploreState
    es))
                     (((ExploreState -> ConflictSetLog (Assignment, RevDepMap),
      Tree Assignment (GoalReason QPN))
     -> ExploreState -> ConflictSetLog (Assignment, RevDepMap))
    -> WeightedPSQ
         [Weight]
         Bool
         (ExploreState -> ConflictSetLog (Assignment, RevDepMap),
          Tree Assignment (GoalReason QPN))
    -> WeightedPSQ
         [Weight]
         Bool
         (ExploreState -> ConflictSetLog (Assignment, RevDepMap))
    forall a b.
    (a -> b)
    -> WeightedPSQ [Weight] Bool a -> WeightedPSQ [Weight] Bool b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (ExploreState -> ConflictSetLog (Assignment, RevDepMap),
     Tree Assignment (GoalReason QPN))
    -> ExploreState -> ConflictSetLog (Assignment, RevDepMap)
    forall a b. (a, b) -> a
    fst WeightedPSQ
      [Weight]
      Bool
      (ExploreState -> ConflictSetLog (Assignment, RevDepMap),
       Tree Assignment (GoalReason QPN))
    ts)
        go (SChoiceF QSN
    qsn RevDepMap
    _ GoalReason QPN
    gr WeakOrTrivial
    _     WeightedPSQ
      [Weight]
      Bool
      (ExploreState -> ConflictSetLog (Assignment, RevDepMap),
       Tree Assignment (GoalReason QPN))
    ts)            =
          Maybe Int
    -> EnableBackjumping
    -> FineGrainedConflicts
    -> (Bool -> Set Conflict -> Maybe ConflictSet)
    -> (Bool
        -> ConflictSet
        -> ExploreState
        -> ConflictSetLog (Assignment, RevDepMap))
    -> Var QPN
    -> ConflictSet
    -> WeightedPSQ
         [Weight]
         Bool
         (ExploreState -> ConflictSetLog (Assignment, RevDepMap))
    -> ExploreState
    -> ConflictSetLog (Assignment, RevDepMap)
    forall w k a.
    Maybe Int
    -> EnableBackjumping
    -> FineGrainedConflicts
    -> (k -> Set Conflict -> Maybe ConflictSet)
    -> (k -> ConflictSet -> ExploreState -> ConflictSetLog a)
    -> Var QPN
    -> ConflictSet
    -> WeightedPSQ w k (ExploreState -> ConflictSetLog a)
    -> ExploreState
    -> ConflictSetLog a
    backjump Maybe Int
    mbj EnableBackjumping
    enableBj FineGrainedConflicts
    fineGrainedConflicts
                   (\Bool
    _ Set Conflict
    _ -> Maybe ConflictSet
    forall a. Maybe a
    Nothing)
                   ((ConflictSet
     -> ExploreState -> ConflictSetLog (Assignment, RevDepMap))
    -> Bool
    -> ConflictSet
    -> ExploreState
    -> ConflictSetLog (Assignment, RevDepMap)
    forall a b. a -> b -> a
    const ConflictSet
    -> ExploreState -> ConflictSetLog (Assignment, RevDepMap)
    forall a. ConflictSet -> ExploreState -> ConflictSetLog a
    logSkippedChoiceSimple)
                   (QSN -> Var QPN
    forall qpn. SN qpn -> Var qpn
    S QSN
    qsn) (Var QPN -> GoalReason QPN -> ConflictSet
    avoidSet (QSN -> Var QPN
    forall qpn. SN qpn -> Var qpn
    S QSN
    qsn) GoalReason QPN
    gr) (WeightedPSQ
       [Weight]
       Bool
       (ExploreState -> ConflictSetLog (Assignment, RevDepMap))
     -> ExploreState -> ConflictSetLog (Assignment, RevDepMap))
    -> WeightedPSQ
         [Weight]
         Bool
         (ExploreState -> ConflictSetLog (Assignment, RevDepMap))
    -> ExploreState
    -> ConflictSetLog (Assignment, RevDepMap)
    forall a b. (a -> b) -> a -> b
    $ -- try children in order,
                   (Bool
     -> (ExploreState -> ConflictSetLog (Assignment, RevDepMap))
     -> ExploreState
     -> ConflictSetLog (Assignment, RevDepMap))
    -> WeightedPSQ
         [Weight]
         Bool
         (ExploreState -> ConflictSetLog (Assignment, RevDepMap))
    -> WeightedPSQ
         [Weight]
         Bool
         (ExploreState -> ConflictSetLog (Assignment, RevDepMap))
    forall k v1 v2 w.
    (k -> v1 -> v2) -> WeightedPSQ w k v1 -> WeightedPSQ w k v2
    W.mapWithKey                    -- when descending ...
                     (\ Bool
    k ExploreState -> ConflictSetLog (Assignment, RevDepMap)
    r ExploreState
    es -> Message
    -> ConflictSetLog (Assignment, RevDepMap)
    -> ConflictSetLog (Assignment, RevDepMap)
    forall fail done.
    Message -> RetryLog Message fail done -> RetryLog Message fail done
    tryWith (QSN -> Bool -> Message
    TryS QSN
    qsn Bool
    k) (ExploreState -> ConflictSetLog (Assignment, RevDepMap)
    r ExploreState
    es))
                     (((ExploreState -> ConflictSetLog (Assignment, RevDepMap),
      Tree Assignment (GoalReason QPN))
     -> ExploreState -> ConflictSetLog (Assignment, RevDepMap))
    -> WeightedPSQ
         [Weight]
         Bool
         (ExploreState -> ConflictSetLog (Assignment, RevDepMap),
          Tree Assignment (GoalReason QPN))
    -> WeightedPSQ
         [Weight]
         Bool
         (ExploreState -> ConflictSetLog (Assignment, RevDepMap))
    forall a b.
    (a -> b)
    -> WeightedPSQ [Weight] Bool a -> WeightedPSQ [Weight] Bool b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (ExploreState -> ConflictSetLog (Assignment, RevDepMap),
     Tree Assignment (GoalReason QPN))
    -> ExploreState -> ConflictSetLog (Assignment, RevDepMap)
    forall a b. (a, b) -> a
    fst WeightedPSQ
      [Weight]
      Bool
      (ExploreState -> ConflictSetLog (Assignment, RevDepMap),
       Tree Assignment (GoalReason QPN))
    ts)
        go (GoalChoiceF RevDepMap
    _           PSQ
      (Goal QPN)
      (ExploreState -> ConflictSetLog (Assignment, RevDepMap),
       Tree Assignment (GoalReason QPN))
    ts)            = \ ExploreState
    es ->
          let (Goal QPN
    k, (ExploreState -> ConflictSetLog (Assignment, RevDepMap)
    v, Tree Assignment (GoalReason QPN)
    tree)) = PSQ
      (Goal QPN)
      (ExploreState -> ConflictSetLog (Assignment, RevDepMap),
       Tree Assignment (GoalReason QPN))
    -> ConflictMap
    -> (Goal QPN,
        (ExploreState -> ConflictSetLog (Assignment, RevDepMap),
         Tree Assignment (GoalReason QPN)))
    forall a. PSQ (Goal QPN) a -> ConflictMap -> (Goal QPN, a)
    getBestGoal' PSQ
      (Goal QPN)
      (ExploreState -> ConflictSetLog (Assignment, RevDepMap),
       Tree Assignment (GoalReason QPN))
    ts (ExploreState -> ConflictMap
    esConflictMap ExploreState
    es)
          in Message
    -> ConflictSetLog (Assignment, RevDepMap)
    -> ConflictSetLog (Assignment, RevDepMap)
    forall step fail done.
    step -> RetryLog step fail done -> RetryLog step fail done
    continueWith (Goal QPN -> Message
    Next Goal QPN
    k) (ConflictSetLog (Assignment, RevDepMap)
     -> ConflictSetLog (Assignment, RevDepMap))
    -> ConflictSetLog (Assignment, RevDepMap)
    -> ConflictSetLog (Assignment, RevDepMap)
    forall a b. (a -> b) -> a -> b
    $
             -- Goal choice nodes are normally not counted as backjumps, since the
             -- solver always explores exactly one choice, which means that the
             -- backjump from the goal choice would be redundant with the backjump
             -- from the PChoice, FChoice, or SChoice below. The one case where the
             -- backjump is not redundant is when the chosen goal is a failure node,
             -- so we log a backjump in that case.
             case Tree Assignment (GoalReason QPN)
    tree of
               Fail ConflictSet
    _ FailReason
    _ -> ConflictSetLog (Assignment, RevDepMap)
    -> (ConflictSet
        -> ExploreState -> ConflictSetLog (Assignment, RevDepMap))
    -> ConflictSetLog (Assignment, RevDepMap)
    forall a.
    ConflictSetLog a
    -> (ConflictSet -> ExploreState -> ConflictSetLog a)
    -> ConflictSetLog a
    retryNoSolution (ExploreState -> ConflictSetLog (Assignment, RevDepMap)
    v ExploreState
    es) ((ConflictSet
      -> ExploreState -> ConflictSetLog (Assignment, RevDepMap))
     -> ConflictSetLog (Assignment, RevDepMap))
    -> (ConflictSet
        -> ExploreState -> ConflictSetLog (Assignment, RevDepMap))
    -> ConflictSetLog (Assignment, RevDepMap)
    forall a b. (a -> b) -> a -> b
    $ Maybe Int
    -> ConflictSet
    -> ExploreState
    -> ConflictSetLog (Assignment, RevDepMap)
    forall a.
    Maybe Int -> ConflictSet -> ExploreState -> ConflictSetLog a
    logBackjump Maybe Int
    mbj
               Tree Assignment (GoalReason QPN)
    _        -> ExploreState -> ConflictSetLog (Assignment, RevDepMap)
    v ExploreState
    es

        initES :: ExploreState
    initES = ES {
            esConflictMap :: ConflictMap
    esConflictMap = ConflictMap
    forall k a. Map k a
    M.empty
          , esBackjumps :: Int
    esBackjumps = Int
    0
          }

        -- Is it possible for this package instance (QPN and POption) to resolve any
        -- of the conflicts that were caused by the previous instance? The default
        -- is true, because it is always safe to explore a package instance.
        -- Skipping it is an optimization. If false, it returns a new conflict set
        -- to be merged with the previous one.
        couldResolveConflicts :: QPN -> POption -> S.Set CS.Conflict -> Maybe ConflictSet
        couldResolveConflicts :: QPN -> POption -> Set Conflict -> Maybe ConflictSet
    couldResolveConflicts currentQPN :: QPN
    currentQPN@(Q PackagePath
    _ PackageName
    pn) (POption i :: I
    i@(I Ver
    v Loc
    _) Maybe PackagePath
    _) Set Conflict
    conflicts =
          let (PInfo FlaggedDeps PackageName
    deps Map ExposedComponent ComponentInfo
    _ FlagInfo
    _ Maybe FailReason
    _) = Index
    idx Index -> PackageName -> Map I PInfo
    forall k a. Ord k => Map k a -> k -> a
    M.! PackageName
    pn Map I PInfo -> I -> PInfo
    forall k a. Ord k => Map k a -> k -> a
    M.! I
    i
              qdeps :: FlaggedDeps QPN
    qdeps = QualifyOptions -> QPN -> FlaggedDeps PackageName -> FlaggedDeps QPN
    qualifyDeps (Index -> QualifyOptions
    defaultQualifyOptions Index
    idx) QPN
    currentQPN FlaggedDeps PackageName
    deps

              couldBeResolved :: CS.Conflict -> Maybe ConflictSet
              couldBeResolved :: Conflict -> Maybe ConflictSet
    couldBeResolved Conflict
    CS.OtherConflict = Maybe ConflictSet
    forall a. Maybe a
    Nothing
              couldBeResolved (CS.GoalConflict QPN
    conflictingDep) =
                  -- Check whether this package instance also has 'conflictingDep'
                  -- as a dependency (ignoring flag and stanza choices).
                  if [()] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [() | Simple (LDep DependencyReason QPN
    _ (Dep (PkgComponent QPN
    qpn ExposedComponent
    _) CI
    _)) Component
    _ <- FlaggedDeps QPN
    qdeps, QPN
    qpn QPN -> QPN -> Bool
    forall a. Eq a => a -> a -> Bool
    == QPN
    conflictingDep]
                  then Maybe ConflictSet
    forall a. Maybe a
    Nothing
                  else ConflictSet -> Maybe ConflictSet
    forall a. a -> Maybe a
    Just ConflictSet
    CS.empty
              couldBeResolved (CS.VersionConstraintConflict QPN
    dep Ver
    excludedVersion) =
                  -- Check whether this package instance also excludes version
                  -- 'excludedVersion' of 'dep' (ignoring flag and stanza choices).
                  let vrs :: [VR]
    vrs = [VR
    vr | Simple (LDep DependencyReason QPN
    _ (Dep (PkgComponent QPN
    qpn ExposedComponent
    _) (Constrained VR
    vr))) Component
    _ <- FlaggedDeps QPN
    qdeps, QPN
    qpn QPN -> QPN -> Bool
    forall a. Eq a => a -> a -> Bool
    == QPN
    dep ]
                      vrIntersection :: VR
    vrIntersection = (VR -> VR -> VR) -> VR -> [VR] -> VR
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    L.foldl' VR -> VR -> VR
    (.&&.) VR
    anyVersion [VR]
    vrs
                  in if VR -> Ver -> Bool
    checkVR VR
    vrIntersection Ver
    excludedVersion
                     then Maybe ConflictSet
    forall a. Maybe a
    Nothing
                     else -- If we skip this package instance, we need to update the
                          -- conflict set to say that 'dep' was also excluded by
                          -- this package instance's constraint.
                          ConflictSet -> Maybe ConflictSet
    forall a. a -> Maybe a
    Just (ConflictSet -> Maybe ConflictSet)
    -> ConflictSet -> Maybe ConflictSet
    forall a b. (a -> b) -> a -> b
    $ Var QPN -> Conflict -> ConflictSet
    CS.singletonWithConflict (QPN -> Var QPN
    forall qpn. qpn -> Var qpn
    P QPN
    dep) (Conflict -> ConflictSet) -> Conflict -> ConflictSet
    forall a b. (a -> b) -> a -> b
    $
                          QPN -> OrderedVersionRange -> Conflict
    CS.VersionConflict QPN
    currentQPN (VR -> OrderedVersionRange
    CS.OrderedVersionRange VR
    vrIntersection)
              couldBeResolved (CS.VersionConflict QPN
    reverseDep (CS.OrderedVersionRange VR
    excludingVR)) =
                  -- Check whether this package instance's version is also excluded
                  -- by 'excludingVR'.
                  if VR -> Ver -> Bool
    checkVR VR
    excludingVR Ver
    v
                  then Maybe ConflictSet
    forall a. Maybe a
    Nothing
                  else -- If we skip this version, we need to update the conflict
                       -- set to say that the reverse dependency also excluded this
                       -- version.
                       ConflictSet -> Maybe ConflictSet
    forall a. a -> Maybe a
    Just (ConflictSet -> Maybe ConflictSet)
    -> ConflictSet -> Maybe ConflictSet
    forall a b. (a -> b) -> a -> b
    $ Var QPN -> Conflict -> ConflictSet
    CS.singletonWithConflict (QPN -> Var QPN
    forall qpn. qpn -> Var qpn
    P QPN
    reverseDep) (QPN -> Ver -> Conflict
    CS.VersionConstraintConflict QPN
    currentQPN Ver
    v)
          in ([ConflictSet] -> ConflictSet)
    -> Maybe [ConflictSet] -> Maybe ConflictSet
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap [ConflictSet] -> ConflictSet
    CS.unions (Maybe [ConflictSet] -> Maybe ConflictSet)
    -> Maybe [ConflictSet] -> Maybe ConflictSet
    forall a b. (a -> b) -> a -> b
    $ (Conflict -> Maybe ConflictSet)
    -> [Conflict] -> Maybe [ConflictSet]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse Conflict -> Maybe ConflictSet
    couldBeResolved (Set Conflict -> [Conflict]
    forall a. Set a -> [a]
    S.toList Set Conflict
    conflicts)

        logSkippedPackage :: QPN -> POption -> ConflictSet -> ExploreState -> ConflictSetLog a
        logSkippedPackage :: forall a.
    QPN -> POption -> ConflictSet -> ExploreState -> ConflictSetLog a
    logSkippedPackage QPN
    qpn POption
    pOption ConflictSet
    cs ExploreState
    es =
            Message
    -> RetryLog Message IntermediateFailure a
    -> RetryLog Message IntermediateFailure a
    forall fail done.
    Message -> RetryLog Message fail done -> RetryLog Message fail done
    tryWith (QPN -> POption -> Message
    TryP QPN
    qpn POption
    pOption) (RetryLog Message IntermediateFailure a
     -> RetryLog Message IntermediateFailure a)
    -> RetryLog Message IntermediateFailure a
    -> RetryLog Message IntermediateFailure a
    forall a b. (a -> b) -> a -> b
    $
            Message
    -> IntermediateFailure -> RetryLog Message IntermediateFailure a
    forall step fail done. step -> fail -> RetryLog step fail done
    failWith (Set Conflict -> Message
    Skip (Set Conflict -> Maybe (Set Conflict) -> Set Conflict
    forall a. a -> Maybe a -> a
    fromMaybe Set Conflict
    forall a. Set a
    S.empty (Maybe (Set Conflict) -> Set Conflict)
    -> Maybe (Set Conflict) -> Set Conflict
    forall a b. (a -> b) -> a -> b
    $ Var QPN -> ConflictSet -> Maybe (Set Conflict)
    CS.lookup (QPN -> Var QPN
    forall qpn. qpn -> Var qpn
    P QPN
    qpn) ConflictSet
    cs)) (IntermediateFailure -> RetryLog Message IntermediateFailure a)
    -> IntermediateFailure -> RetryLog Message IntermediateFailure a
    forall a b. (a -> b) -> a -> b
    $
            ConflictSet -> ExploreState -> IntermediateFailure
    NoSolution ConflictSet
    cs ExploreState
    es

        -- This function is used for flag and stanza choices, but it should not be
        -- called, because there is currently no way to skip a value for a flag or
        -- stanza.
        logSkippedChoiceSimple :: ConflictSet -> ExploreState -> ConflictSetLog a
        logSkippedChoiceSimple :: forall a. ConflictSet -> ExploreState -> ConflictSetLog a
    logSkippedChoiceSimple ConflictSet
    cs ExploreState
    es = Progress Message IntermediateFailure a
    -> RetryLog Message IntermediateFailure a
    forall step fail done.
    Progress step fail done -> RetryLog step fail done
    fromProgress (Progress Message IntermediateFailure a
     -> RetryLog Message IntermediateFailure a)
    -> Progress Message IntermediateFailure a
    -> RetryLog Message IntermediateFailure a
    forall a b. (a -> b) -> a -> b
    $ IntermediateFailure -> Progress Message IntermediateFailure a
    forall step fail done. fail -> Progress step fail done
    P.Fail (IntermediateFailure -> Progress Message IntermediateFailure a)
    -> IntermediateFailure -> Progress Message IntermediateFailure a
    forall a b. (a -> b) -> a -> b
    $ ConflictSet -> ExploreState -> IntermediateFailure
    NoSolution ConflictSet
    cs ExploreState
    es

    -- | Build a conflict set corresponding to the (virtual) option not to
    -- choose a solution for a goal at all.
    --
    -- In the solver, the set of goals is not statically determined, but depends
    -- on the choices we make. Therefore, when dealing with conflict sets, we
    -- always have to consider that we could perhaps make choices that would
    -- avoid the existence of the goal completely.
    --
    -- Whenever we actually introduce a choice in the tree, we have already established
    -- 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 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 last conflict set becomes the
    -- actual conflict set.
    --
    -- - In a situation where all of the children's conflict sets contain the
    -- current variable, the goal reason of the current node will be added to the
    -- conflict set.
    --
    avoidSet :: Var QPN -> QGoalReason -> ConflictSet
    avoidSet :: Var QPN -> GoalReason QPN -> ConflictSet
    avoidSet var :: Var QPN
    var@(P QPN
    qpn) GoalReason QPN
    gr =
      ConflictSet -> ConflictSet -> ConflictSet
    CS.union (Var QPN -> ConflictSet
    CS.singleton Var QPN
    var) (QPN -> GoalReason QPN -> ConflictSet
    goalReasonToConflictSetWithConflict QPN
    qpn GoalReason QPN
    gr)
    avoidSet Var QPN
    var         GoalReason QPN
    gr =
      ConflictSet -> ConflictSet -> ConflictSet
    CS.union (Var QPN -> ConflictSet
    CS.singleton Var QPN
    var) (GoalReason QPN -> ConflictSet
    goalReasonToConflictSet GoalReason QPN
    gr)

    -- | Interface.
    --
    -- Takes as an argument a limit on allowed backjumps. If the limit is 'Nothing',
    -- then infinitely many backjumps are allowed. If the limit is 'Just 0',
    -- backtracking is completely disabled.
    backjumpAndExplore :: Maybe Int
                       -> EnableBackjumping
                       -> FineGrainedConflicts
                       -> CountConflicts
                       -> Index
                       -> Tree d QGoalReason
                       -> RetryLog Message SolverFailure (Assignment, RevDepMap)
    backjumpAndExplore :: forall d.
    Maybe Int
    -> EnableBackjumping
    -> FineGrainedConflicts
    -> CountConflicts
    -> Index
    -> Tree d (GoalReason QPN)
    -> RetryLog Message SolverFailure (Assignment, RevDepMap)
    backjumpAndExplore Maybe Int
    mbj EnableBackjumping
    enableBj FineGrainedConflicts
    fineGrainedConflicts CountConflicts
    countConflicts Index
    idx =
        (IntermediateFailure -> SolverFailure)
    -> ConflictSetLog (Assignment, RevDepMap)
    -> RetryLog Message SolverFailure (Assignment, RevDepMap)
    forall fail1 fail2 step done.
    (fail1 -> fail2)
    -> RetryLog step fail1 done -> RetryLog step fail2 done
    mapFailure IntermediateFailure -> SolverFailure
    convertFailure
      (ConflictSetLog (Assignment, RevDepMap)
     -> RetryLog Message SolverFailure (Assignment, RevDepMap))
    -> (Tree d (GoalReason QPN)
        -> ConflictSetLog (Assignment, RevDepMap))
    -> Tree d (GoalReason QPN)
    -> RetryLog Message SolverFailure (Assignment, RevDepMap)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Maybe Int
    -> EnableBackjumping
    -> FineGrainedConflicts
    -> CountConflicts
    -> Index
    -> Tree Assignment (GoalReason QPN)
    -> ConflictSetLog (Assignment, RevDepMap)
    exploreLog Maybe Int
    mbj EnableBackjumping
    enableBj FineGrainedConflicts
    fineGrainedConflicts CountConflicts
    countConflicts Index
    idx
      (Tree Assignment (GoalReason QPN)
     -> ConflictSetLog (Assignment, RevDepMap))
    -> (Tree d (GoalReason QPN) -> Tree Assignment (GoalReason QPN))
    -> Tree d (GoalReason QPN)
    -> ConflictSetLog (Assignment, RevDepMap)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Tree d (GoalReason QPN) -> Tree Assignment (GoalReason QPN)
    forall d c. Tree d c -> Tree Assignment c
    assign
      where
        convertFailure :: IntermediateFailure -> SolverFailure
    convertFailure (NoSolution ConflictSet
    cs ExploreState
    es) = ConflictSet -> ConflictMap -> SolverFailure
    ExhaustiveSearch ConflictSet
    cs (ExploreState -> ConflictMap
    esConflictMap ExploreState
    es)
        convertFailure IntermediateFailure
    BackjumpLimit      = SolverFailure
    BackjumpLimitReached