{-# 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 :: 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 (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 :: ConflictMap
esConflictMap = ConflictSet -> ConflictMap -> ConflictMap
updateCM ConflictSet
cs' (ExploreState -> ConflictMap
esConflictMap ExploreState
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 :: ConflictMap
esConflictMap = ConflictSet -> ConflictMap -> ConflictMap
updateCM ConflictSet
lastCS (ExploreState -> ConflictMap
esConflictMap ExploreState
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 :: Maybe Int -> ConflictSet -> ExploreState -> ConflictSetLog a
logBackjump Maybe Int
mbj ConflictSet
cs ExploreState
es =
    Message -> IntermediateFailure -> ConflictSetLog a
forall step fail done. step -> fail -> RetryLog step fail done
failWith (ConflictSet -> FailReason -> Message
Failure ConflictSet
cs FailReason
Backjump) (IntermediateFailure -> ConflictSetLog a)
-> IntermediateFailure -> ConflictSetLog 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 :: Int
esBackjumps = ExploreState -> Int
esBackjumps ExploreState
es Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
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 :: 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 :: 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 :: 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 (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 :: 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 :: 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 (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 (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 (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 (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 (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' :: 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 :: ConflictMap
esConflictMap = ConflictSet -> ConflictMap -> ConflictMap
updateCM ConflictSet
c (ExploreState -> ConflictMap
esConflictMap ExploreState
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 (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 (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 (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 :: ConflictMap -> Int -> ExploreState
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 (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 (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 (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)
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 :: QPN -> POption -> ConflictSet -> ExploreState -> ConflictSetLog a
logSkippedPackage QPN
qpn POption
pOption ConflictSet
cs ExploreState
es =
        Message -> ConflictSetLog a -> ConflictSetLog a
forall fail done.
Message -> RetryLog Message fail done -> RetryLog Message fail done
tryWith (QPN -> POption -> Message
TryP QPN
qpn POption
pOption) (ConflictSetLog a -> ConflictSetLog a)
-> ConflictSetLog a -> ConflictSetLog a
forall a b. (a -> b) -> a -> b
$
        Message -> IntermediateFailure -> ConflictSetLog 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 -> ConflictSetLog a)
-> IntermediateFailure -> ConflictSetLog 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 :: ConflictSet -> ExploreState -> ConflictSetLog a
logSkippedChoiceSimple 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 (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 :: 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