Commit a5f0301f authored by Edsko de Vries's avatar Edsko de Vries
Browse files

Merge pull request #3357 from haskell/solver

Fix construction of conflict sets once and for all (WIP) 
parents 9c48d380 2fc1c146
......@@ -64,22 +64,22 @@ data PreAssignment = PA PPreAssignment FAssignment SAssignment
extend :: (Extension -> Bool) -- ^ is a given extension supported
-> (Language -> Bool) -- ^ is a given language supported
-> (PN -> VR -> Bool) -- ^ is a given pkg-config requirement satisfiable
-> Goal QPN
-> Var QPN
-> PPreAssignment -> [Dep QPN] -> Either (ConflictSet QPN, [Dep QPN]) PPreAssignment
extend extSupported langSupported pkgPresent goal@(Goal var _) = foldM extendSingle
extend extSupported langSupported pkgPresent var = foldM extendSingle
where
extendSingle :: PPreAssignment -> Dep QPN
-> Either (ConflictSet QPN, [Dep QPN]) PPreAssignment
extendSingle a (Ext ext ) =
if extSupported ext then Right a
else Left (toConflictSet goal, [Ext ext])
else Left (varToConflictSet var, [Ext ext])
extendSingle a (Lang lang) =
if langSupported lang then Right a
else Left (toConflictSet goal, [Lang lang])
else Left (varToConflictSet var, [Lang lang])
extendSingle a (Pkg pn vr) =
if pkgPresent pn vr then Right a
else Left (toConflictSet goal, [Pkg pn vr])
else Left (varToConflictSet var, [Pkg pn vr])
extendSingle a (Dep qpn ci) =
let ci' = M.findWithDefault (Constrained []) qpn a
in case (\ x -> M.insert qpn x a) <$> merge ci' ci of
......@@ -90,9 +90,9 @@ extend extSupported langSupported pkgPresent goal@(Goal var _) = foldM extendSin
-- making a choice pkg == instance, and pkg => pkg == instance is a part
-- of the conflict, then this info is clear from the context and does not
-- have to be repeated.
simplify v (Fixed _ (Goal var' _)) c | v == var && var' == var = [c]
simplify v c (Fixed _ (Goal var' _)) | v == var && var' == var = [c]
simplify _ c d = [c, d]
simplify v (Fixed _ var') c | v == var && var' == var = [c]
simplify v c (Fixed _ var') | v == var && var' == var = [c]
simplify _ c d = [c, d]
-- | Delivers an ordered list of fully configured packages.
--
......
......@@ -67,7 +67,7 @@ extendOpen qpn' gs s@(BS { rdeps = gs', open = o' }) = go gs' o' gs
-- | Given the current scope, qualify all the package names in the given set of
-- dependencies and then extend the set of open goals accordingly.
scopedExtendOpen :: QPN -> I -> QGoalReasonChain -> FlaggedDeps Component PN -> FlagInfo ->
scopedExtendOpen :: QPN -> I -> QGoalReason -> FlaggedDeps Component PN -> FlagInfo ->
BuildState -> BuildState
scopedExtendOpen qpn i gr fdeps fdefs s = extendOpen qpn gs s
where
......@@ -97,13 +97,13 @@ scopedExtendOpen qpn i gr fdeps fdefs s = extendOpen qpn gs s
data BuildType =
Goals -- ^ build a goal choice node
| OneGoal (OpenGoal ()) -- ^ build a node for this goal
| Instance QPN I PInfo QGoalReasonChain -- ^ build a tree for a concrete instance
| Instance QPN I PInfo QGoalReason -- ^ build a tree for a concrete instance
deriving Show
build :: BuildState -> Tree QGoalReasonChain
build :: BuildState -> Tree QGoalReason
build = ana go
where
go :: BuildState -> TreeF QGoalReasonChain BuildState
go :: BuildState -> TreeF QGoalReason BuildState
-- If we have a choice between many goals, we just record the choice in
-- the tree. We select each open goal in turn, and before we descend, remove
......@@ -125,8 +125,13 @@ build = ana go
go (BS { index = _ , next = OneGoal (OpenGoal (Simple (Pkg _ _ ) _) _ ) }) =
error "Distribution.Client.Dependency.Modular.Builder: build.go called with Pkg goal"
go bs@(BS { index = idx, next = OneGoal (OpenGoal (Simple (Dep qpn@(Q _ pn) _) _) gr) }) =
-- If the package does not exist in the index, we construct an emty PChoiceF node for it
-- After all, we have no choices here. Alternatively, we could immediately construct
-- a Fail node here, but that would complicate the construction of conflict sets.
-- We will probably want to give this case special treatment when generating error
-- messages though.
case M.lookup pn idx of
Nothing -> FailF (toConflictSet (Goal (P qpn) gr)) (BuildFailureNotInIndex pn)
Nothing -> PChoiceF qpn gr (P.fromList [])
Just pis -> PChoiceF qpn gr (P.fromList (L.map (\ (i, info) ->
(POption i Nothing, bs { next = Instance qpn i info gr }))
(M.toList pis)))
......@@ -138,8 +143,8 @@ build = ana go
-- TODO: Should we include the flag default in the tree?
go bs@(BS { next = OneGoal (OpenGoal (Flagged qfn@(FN (PI qpn _) _) (FInfo b m w) t f) gr) }) =
FChoiceF qfn gr (w || trivial) m (P.fromList (reorder b
[(True, (extendOpen qpn (L.map (flip OpenGoal (FDependency qfn True : gr)) t) bs) { next = Goals }),
(False, (extendOpen qpn (L.map (flip OpenGoal (FDependency qfn False : gr)) f) bs) { next = Goals })]))
[(True, (extendOpen qpn (L.map (flip OpenGoal (FDependency qfn True )) t) bs) { next = Goals }),
(False, (extendOpen qpn (L.map (flip OpenGoal (FDependency qfn False)) f) bs) { next = Goals })]))
where
reorder True = id
reorder False = reverse
......@@ -152,8 +157,8 @@ build = ana go
go bs@(BS { next = OneGoal (OpenGoal (Stanza qsn@(SN (PI qpn _) _) t) gr) }) =
SChoiceF qsn gr trivial (P.fromList
[(False, bs { next = Goals }),
(True, (extendOpen qpn (L.map (flip OpenGoal (SDependency qsn : gr)) t) bs) { next = Goals })])
[(False, bs { next = Goals }),
(True, (extendOpen qpn (L.map (flip OpenGoal (SDependency qsn)) t) bs) { next = Goals })])
where
trivial = L.null t
......@@ -161,13 +166,13 @@ build = ana go
-- and furthermore we update the set of goals.
--
-- TODO: We could inline this above.
go bs@(BS { next = Instance qpn i (PInfo fdeps fdefs _) gr }) =
go ((scopedExtendOpen qpn i (PDependency (PI qpn i) : gr) fdeps fdefs bs)
go bs@(BS { next = Instance qpn i (PInfo fdeps fdefs _) _gr }) =
go ((scopedExtendOpen qpn i (PDependency (PI qpn i)) fdeps fdefs bs)
{ next = Goals })
-- | Interface to the tree builder. Just takes an index and a list of package names,
-- and computes the initial state and then the tree from there.
buildTree :: Index -> Bool -> [PN] -> Tree QGoalReasonChain
buildTree :: Index -> Bool -> [PN] -> Tree QGoalReason
buildTree idx ind igs =
build BS {
index = idx
......@@ -177,7 +182,7 @@ buildTree idx ind igs =
, qualifyOptions = defaultQualifyOptions idx
}
where
topLevelGoal qpn = OpenGoal (Simple (Dep qpn (Constrained [])) ()) [UserGoal]
topLevelGoal qpn = OpenGoal (Simple (Dep qpn (Constrained [])) ()) UserGoal
qpns | ind = makeIndependent igs
| otherwise = L.map (Q (PP DefaultNamespace Unqualified)) igs
......@@ -4,44 +4,31 @@ module Distribution.Client.Dependency.Modular.Cycles (
) where
import Prelude hiding (cycle)
import Control.Monad
import Control.Monad.Reader
import Data.Graph (SCC)
import Data.Set (Set)
import qualified Data.Graph as Gr
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Data.Traversable as T
#if !MIN_VERSION_base(4,8,0)
import Control.Applicative ((<$>))
#endif
import qualified Data.Graph as Gr
import qualified Data.Map as Map
import Distribution.Client.Dependency.Modular.Dependency
import Distribution.Client.Dependency.Modular.Flag
import Distribution.Client.Dependency.Modular.Package
import Distribution.Client.Dependency.Modular.Tree
import qualified Distribution.Client.Dependency.Modular.ConflictSet as CS
type DetectCycles = Reader (ConflictSet QPN)
-- | Find and reject any solutions that are cyclic
detectCyclesPhase :: Tree QGoalReasonChain -> Tree QGoalReasonChain
detectCyclesPhase = (`runReader` CS.empty) . cata go
detectCyclesPhase :: Tree QGoalReason -> Tree QGoalReason
detectCyclesPhase = cata go
where
-- Most cases are simple; we just need to remember which choices we made
go :: TreeF QGoalReasonChain (DetectCycles (Tree QGoalReasonChain)) -> DetectCycles (Tree QGoalReasonChain)
go (PChoiceF qpn gr cs) = PChoice qpn gr <$> local (CS.insert $ P qpn) (T.sequence cs)
go (FChoiceF qfn gr w m cs) = FChoice qfn gr w m <$> local (CS.insert $ F qfn) (T.sequence cs)
go (SChoiceF qsn gr w cs) = SChoice qsn gr w <$> local (CS.insert $ S qsn) (T.sequence cs)
go (GoalChoiceF cs) = GoalChoice <$> (T.sequence cs)
go (FailF cs reason) = return $ Fail cs reason
-- The only node of interest is DoneF
go :: TreeF QGoalReason (Tree QGoalReason) -> Tree QGoalReason
go (PChoiceF qpn gr cs) = PChoice qpn gr cs
go (FChoiceF qfn gr w m cs) = FChoice qfn gr w m cs
go (SChoiceF qsn gr w cs) = SChoice qsn gr w cs
go (GoalChoiceF cs) = GoalChoice cs
go (FailF cs reason) = Fail cs reason
-- We check for cycles only if we have actually found a solution
-- This minimizes the number of cycle checks we do as cycles are rare
go (DoneF revDeps) = do
fullSet <- ask
return $ case findCycles fullSet revDeps of
case findCycles revDeps of
Nothing -> Done revDeps
Just relSet -> Fail relSet CyclicDependencies
......@@ -49,10 +36,11 @@ detectCyclesPhase = (`runReader` CS.empty) . cata go
-- as the full conflict set containing all decisions that led to that 'Done'
-- node, check if the solution is cyclic. If it is, return the conflict set
-- containing all decisions that could potentially break the cycle.
findCycles :: ConflictSet QPN -> RevDepMap -> Maybe (ConflictSet QPN)
findCycles fullSet revDeps = do
guard $ not (null cycles)
return $ relevantConflictSet (Set.fromList (concat cycles)) fullSet
findCycles :: RevDepMap -> Maybe (ConflictSet QPN)
findCycles revDeps =
case cycles of
[] -> Nothing
c:_ -> Just $ CS.unions $ map (varToConflictSet . P) c
where
cycles :: [[QPN]]
cycles = [vs | Gr.CyclicSCC vs <- scc]
......@@ -62,13 +50,3 @@ findCycles fullSet revDeps = do
aux :: (QPN, [(comp, QPN)]) -> (QPN, QPN, [QPN])
aux (fr, to) = (fr, fr, map snd to)
-- | Construct the relevant conflict set given the full conflict set that
-- lead to this decision and the set of packages involved in the cycle
relevantConflictSet :: Set QPN -> ConflictSet QPN -> ConflictSet QPN
relevantConflictSet cycle = CS.filter isRelevant
where
isRelevant :: Var QPN -> Bool
isRelevant (P qpn) = qpn `Set.member` cycle
isRelevant (F (FN (PI qpn _i) _fn)) = qpn `Set.member` cycle
isRelevant (S (SN (PI qpn _i) _sn)) = qpn `Set.member` cycle
......@@ -19,6 +19,7 @@ module Distribution.Client.Dependency.Modular.Dependency (
, flattenFlaggedDeps
, QualifyOptions(..)
, qualifyDeps
, unqualifyDeps
-- ** Setting/forgetting components
, forgetCompOpenGoal
, setCompFlaggedDeps
......@@ -27,9 +28,11 @@ module Distribution.Client.Dependency.Modular.Dependency (
-- * Goals
, Goal(..)
, GoalReason(..)
, QGoalReasonChain
, ResetGoal(..)
, toConflictSet
, QGoalReason
, ResetVar(..)
, goalVarToConflictSet
, varToConflictSet
, goalReasonToVars
-- * Open goals
, OpenGoal(..)
, close
......@@ -61,7 +64,7 @@ import Distribution.Client.ComponentDeps (Component(..))
-- a fixed instance, and we record the package name for which the choice
-- is for convenience. Otherwise, it is a list of version ranges paired with
-- the goals / variables that introduced them.
data CI qpn = Fixed I (Goal qpn) | Constrained [VROrigin qpn]
data CI qpn = Fixed I (Var qpn) | Constrained [VROrigin qpn]
deriving (Eq, Show, Functor)
showCI :: CI QPN -> String
......@@ -85,13 +88,13 @@ showCI (Constrained vr) = showVR (collapse vr)
merge :: Ord qpn => CI qpn -> CI qpn -> Either (ConflictSet qpn, (CI qpn, CI qpn)) (CI qpn)
merge c@(Fixed i g1) d@(Fixed j g2)
| i == j = Right c
| otherwise = Left (CS.union (toConflictSet g1) (toConflictSet g2), (c, d))
| otherwise = Left (CS.union (varToConflictSet g1) (varToConflictSet g2), (c, d))
merge c@(Fixed (I v _) g1) (Constrained rs) = go rs -- I tried "reverse rs" here, but it seems to slow things down ...
where
go [] = Right c
go (d@(vr, g2) : vrs)
| checkVR vr v = go vrs
| otherwise = Left (CS.union (toConflictSet g1) (toConflictSet g2), (c, Constrained [d]))
| otherwise = Left (CS.union (varToConflictSet g1) (varToConflictSet g2), (c, Constrained [d]))
merge c@(Constrained _) d@(Fixed _ _) = merge d c
merge (Constrained rs) (Constrained ss) = Right (Constrained (rs ++ ss))
......@@ -161,12 +164,12 @@ data Dep qpn = Dep qpn (CI qpn) -- dependency on a package
deriving (Eq, Show)
showDep :: Dep QPN -> String
showDep (Dep qpn (Fixed i (Goal v _)) ) =
showDep (Dep qpn (Fixed i v) ) =
(if P qpn /= v then showVar v ++ " => " else "") ++
showQPN qpn ++ "==" ++ showI i
showDep (Dep qpn (Constrained [(vr, Goal v _)])) =
showDep (Dep qpn (Constrained [(vr, v)])) =
showVar v ++ " => " ++ showQPN qpn ++ showVR vr
showDep (Dep qpn ci ) =
showDep (Dep qpn ci ) =
showQPN qpn ++ showCI ci
showDep (Ext ext) = "requires " ++ display ext
showDep (Lang lang) = "requires " ++ display lang
......@@ -188,6 +191,12 @@ data QualifyOptions = QO {
-- | Apply built-in rules for package qualifiers
--
-- Although the behaviour of 'qualifyDeps' depends on the 'QualifyOptions',
-- it is important that these 'QualifyOptions' are _static_. Qualification
-- does NOT depend on flag assignment; in other words, it behaves the same no
-- matter which choices the solver makes (modulo the global 'QualifyOptions');
-- we rely on this in 'linkDeps' (see comment there).
--
-- NOTE: It's the _dependencies_ of a package that may or may not be independent
-- from the package itself. Package flag choices must of course be consistent.
qualifyDeps :: QualifyOptions -> QPN -> FlaggedDeps Component PN -> FlaggedDeps Component QPN
......@@ -239,6 +248,33 @@ qualifyDeps QO{..} (Q pp@(PP ns q) pn) = go
qSetup :: Component -> Bool
qSetup comp = qoSetupIndependent && comp == ComponentSetup
-- | Remove qualifiers from set of dependencies
--
-- This is used during link validation: when we link package @Q.A@ to @Q'.A@,
-- then all dependencies @Q.B@ need to be linked to @Q'.B@. In order to compute
-- what to link these dependencies to, we need to requalify @Q.B@ to become
-- @Q'.B@; we do this by first removing all qualifiers and then calling
-- 'qualifyDeps' again.
unqualifyDeps :: FlaggedDeps comp QPN -> FlaggedDeps comp PN
unqualifyDeps = go
where
go :: FlaggedDeps comp QPN -> FlaggedDeps comp PN
go = map go1
go1 :: FlaggedDep comp QPN -> FlaggedDep comp PN
go1 (Flagged fn nfo t f) = Flagged (fmap unq fn) nfo (go t) (go f)
go1 (Stanza sn t) = Stanza (fmap unq sn) (go t)
go1 (Simple dep comp) = Simple (goD dep) comp
goD :: Dep QPN -> Dep PN
goD (Dep qpn ci) = Dep (unq qpn) (fmap unq ci)
goD (Ext ext) = Ext ext
goD (Lang lang) = Lang lang
goD (Pkg pn vr) = Pkg pn vr
unq :: QPN -> PN
unq (Q _ pn) = pn
{-------------------------------------------------------------------------------
Setting/forgetting the Component
-------------------------------------------------------------------------------}
......@@ -280,12 +316,12 @@ type RevDepMap = Map QPN [(Component, QPN)]
Goals
-------------------------------------------------------------------------------}
-- | Goals are solver variables paired with information about
-- why they have been introduced.
data Goal qpn = Goal (Var qpn) (GoalReasonChain qpn)
-- | A goal is just a solver variable paired with a reason.
-- The reason is only used for tracing.
data Goal qpn = Goal (Var qpn) (GoalReason qpn)
deriving (Eq, Show, Functor)
-- | Reasons why a goal can be added to a goal set.
-- | Reason why a goal is being added to a goal set.
data GoalReason qpn =
UserGoal
| PDependency (PI qpn)
......@@ -293,41 +329,47 @@ data GoalReason qpn =
| SDependency (SN qpn)
deriving (Eq, Show, Functor)
-- | The first element is the immediate reason. The rest are the reasons
-- for the reasons ...
type GoalReasonChain qpn = [GoalReason qpn]
type QGoalReasonChain = GoalReasonChain QPN
class ResetGoal f where
resetGoal :: Goal qpn -> f qpn -> f qpn
type QGoalReason = GoalReason QPN
instance ResetGoal CI where
resetGoal g (Fixed i _) = Fixed i g
resetGoal g (Constrained vrs) = Constrained (L.map (\ (x, y) -> (x, resetGoal g y)) vrs)
class ResetVar f where
resetVar :: Var qpn -> f qpn -> f qpn
instance ResetGoal Dep where
resetGoal g (Dep qpn ci) = Dep qpn (resetGoal g ci)
resetGoal _ (Ext ext) = Ext ext
resetGoal _ (Lang lang) = Lang lang
resetGoal _ (Pkg pn vr) = Pkg pn vr
instance ResetVar CI where
resetVar v (Fixed i _) = Fixed i v
resetVar v (Constrained vrs) = Constrained (L.map (\ (x, y) -> (x, resetVar v y)) vrs)
instance ResetGoal Goal where
resetGoal = const
instance ResetVar Dep where
resetVar v (Dep qpn ci) = Dep qpn (resetVar v ci)
resetVar _ (Ext ext) = Ext ext
resetVar _ (Lang lang) = Lang lang
resetVar _ (Pkg pn vr) = Pkg pn vr
-- | Compute a conflict set from a goal. The conflict set contains the closure
-- of goal reasons as well as the variable of the goal itself.
toConflictSet :: Ord qpn => Goal qpn -> ConflictSet qpn
toConflictSet (Goal g grs) = CS.insert g (goalReasonChainToVars grs)
instance ResetVar Var where
resetVar = const
goalReasonToVars :: GoalReason qpn -> ConflictSet qpn
goalReasonToVars UserGoal = CS.empty
goalReasonToVars (PDependency (PI qpn _)) = CS.singleton (P qpn)
goalReasonToVars (FDependency qfn _) = CS.singleton (F qfn)
goalReasonToVars (SDependency qsn) = CS.singleton (S qsn)
goalReasonChainToVars :: Ord qpn => GoalReasonChain qpn -> ConflictSet qpn
goalReasonChainToVars = CS.unions . L.map goalReasonToVars
-- | Compute a singleton conflict set from a goal, containing just
-- the goal variable.
--
-- NOTE: This is just a call to 'varToConflictSet' under the hood;
-- the 'GoalReason' is ignored.
goalVarToConflictSet :: Goal qpn -> ConflictSet qpn
goalVarToConflictSet (Goal g _gr) = varToConflictSet g
-- | Compute a singleton conflict set from a 'Var'
varToConflictSet :: Var qpn -> ConflictSet qpn
varToConflictSet = CS.singleton
-- | A goal reason is mostly just a variable paired with the
-- decision we made for that variable (except for user goals,
-- where we cannot really point to a solver variable). This
-- function drops the decision and recovers the list of
-- variables (which will be empty or contain one element).
--
goalReasonToVars :: GoalReason qpn -> [Var qpn]
goalReasonToVars UserGoal = []
goalReasonToVars (PDependency (PI qpn _)) = [P qpn]
goalReasonToVars (FDependency qfn _) = [F qfn]
goalReasonToVars (SDependency qsn) = [S qsn]
{-------------------------------------------------------------------------------
Open goals
......@@ -335,7 +377,7 @@ goalReasonChainToVars = CS.unions . L.map goalReasonToVars
-- | For open goals as they occur during the build phase, we need to store
-- additional information about flags.
data OpenGoal comp = OpenGoal (FlaggedDep comp QPN) QGoalReasonChain
data OpenGoal comp = OpenGoal (FlaggedDep comp QPN) QGoalReason
deriving (Eq, Show)
-- | Closes a goal, i.e., removes all the extraneous information that we
......@@ -355,7 +397,7 @@ close (OpenGoal (Stanza qsn _) gr) = Goal (S qsn) gr
Version ranges paired with origins
-------------------------------------------------------------------------------}
type VROrigin qpn = (VR, Goal qpn)
type VROrigin qpn = (VR, Var qpn)
-- | Helper function to collapse a list of version ranges with origins into
-- a single, simplified, version range.
......
......@@ -16,7 +16,8 @@ import qualified Distribution.Client.Dependency.Modular.ConflictSet as CS
import Distribution.Client.Dependency.Modular.Tree
import qualified Distribution.Client.Dependency.Types as T
-- | This function takes the variable we're currently considering and a
-- | This function takes the variable we're currently considering, an
-- initial 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.
......@@ -31,8 +32,15 @@ import qualified Distribution.Client.Dependency.Types as T
-- 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.
backjump :: F.Foldable t => Var QPN -> t (ConflictSetLog a) -> ConflictSetLog a
backjump var xs = F.foldr combine logBackjump xs CS.empty
--
-- The initial 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'.
--
backjump :: F.Foldable t => Var QPN -> ConflictSet QPN -> t (ConflictSetLog a) -> ConflictSetLog a
backjump var initial xs = F.foldr combine logBackjump xs initial
where
combine :: ConflictSetLog a
-> (ConflictSet QPN -> ConflictSetLog a)
......@@ -50,27 +58,27 @@ type ConflictSetLog = T.Progress Message (ConflictSet QPN)
-- | A tree traversal that simultaneously propagates conflict sets up
-- the tree from the leaves and creates a log.
exploreLog :: Tree a -> (Assignment -> ConflictSetLog (Assignment, RevDepMap))
exploreLog :: Tree QGoalReason -> (Assignment -> ConflictSetLog (Assignment, RevDepMap))
exploreLog = cata go
where
go :: TreeF a (Assignment -> ConflictSetLog (Assignment, RevDepMap))
-> (Assignment -> ConflictSetLog (Assignment, RevDepMap))
go :: TreeF QGoalReason (Assignment -> ConflictSetLog (Assignment, RevDepMap))
-> (Assignment -> ConflictSetLog (Assignment, RevDepMap))
go (FailF c fr) _ = failWith (Failure c fr) c
go (DoneF rdm) a = succeedWith Success (a, rdm)
go (PChoiceF qpn _ ts) (A pa fa sa) =
backjump (P qpn) $ -- try children in order,
go (PChoiceF qpn gr ts) (A pa fa sa) =
backjump (P qpn) (avoidSet (P qpn) gr) $ -- try children in order,
P.mapWithKey -- when descending ...
(\ i@(POption k _) r -> tryWith (TryP qpn i) $ -- log and ...
r (A (M.insert qpn k pa) fa sa)) -- record the pkg choice
ts
go (FChoiceF qfn _ _ _ ts) (A pa fa sa) =
backjump (F qfn) $ -- try children in order,
go (FChoiceF qfn gr _ _ ts) (A pa fa sa) =
backjump (F qfn) (avoidSet (F qfn) gr) $ -- try children in order,
P.mapWithKey -- when descending ...
(\ k r -> tryWith (TryF qfn k) $ -- log and ...
r (A pa (M.insert qfn k fa) sa)) -- record the pkg choice
ts
go (SChoiceF qsn _ _ ts) (A pa fa sa) =
backjump (S qsn) $ -- try children in order,
go (SChoiceF qsn gr _ ts) (A pa fa sa) =
backjump (S qsn) (avoidSet (S qsn) gr) $ -- try children in order,
P.mapWithKey -- when descending ...
(\ k r -> tryWith (TryS qsn k) $ -- log and ...
r (A pa fa (M.insert qsn k sa))) -- record the pkg choice
......@@ -80,8 +88,35 @@ exploreLog = cata go
(failWith (Failure CS.empty EmptyGoalChoice) CS.empty) -- empty goal choice is an internal error
(\ k v _xs -> continueWith (Next (close k)) (v a)) -- commit to the first goal choice
-- | 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 actual 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 initial conflict set.
--
-- This has two effects:
--
-- - In a situation where there are no choices available at all (this happens
-- if an unknown package is requested), the initial conflict set becomes the
-- actual conflict set.
--
-- - In a situation where we backjump past the current node, the goal reason
-- of the current node will be added to the conflict set.
--
avoidSet :: Var QPN -> QGoalReason -> ConflictSet QPN
avoidSet var gr =
CS.fromList (var : goalReasonToVars gr)
-- | Interface.
backjumpAndExplore :: Tree a -> Log Message (Assignment, RevDepMap)
backjumpAndExplore :: Tree QGoalReason -> Log Message (Assignment, RevDepMap)
backjumpAndExplore t = toLog $ exploreLog t (A M.empty M.empty M.empty)
where
toLog :: T.Progress step fail done -> Log step done
......
......@@ -84,7 +84,7 @@ convIPId pn' idx ipid =
Nothing -> Nothing
Just ipi -> let i = I (pkgVersion (sourcePackageId ipi)) (Inst ipid)
pn = pkgName (sourcePackageId ipi)
in Just (D.Simple (Dep pn (Fixed i (Goal (P pn') []))) ())
in Just (D.Simple (Dep pn (Fixed i (P pn'))) ())
-- | Convert a cabal-install source package index to the simpler,
-- more uniform index format of the solver.
......@@ -300,7 +300,7 @@ convBranch os arch cinfo pi@(PI pn _) fds comp getInfo ipns (c', t', mf') =
-- occurrences of multiple version ranges, as all dependencies below this
-- point have been generated using 'convDep'.
extractCommon :: FlaggedDeps Component PN -> FlaggedDeps Component PN -> FlaggedDeps Component PN
extractCommon ps ps' = [ D.Simple (Dep pn1 (Constrained [(vr1 .||. vr2, Goal (P pn) [])])) comp
extractCommon ps ps' = [ D.Simple (Dep pn1 (Constrained [(vr1 .||. vr2, P pn)])) comp
| D.Simple (Dep pn1 (Constrained [(vr1, _)])) _ <- ps
, D.Simple (Dep pn2 (Constrained [(vr2, _)])) _ <- ps'
, pn1 == pn2
......@@ -308,7 +308,7 @@ convBranch os arch cinfo pi@(PI pn _) fds comp getInfo ipns (c', t', mf') =
-- | Convert a Cabal dependency to a solver-specific dependency.
convDep :: PN -> Dependency -> Dep PN
convDep pn' (Dependency pn vr) = Dep pn (Constrained [(vr, Goal (P pn') [])])
convDep pn' (Dependency pn vr) = Dep pn (Constrained [(vr, P pn')])
-- | Convert setup dependencies
convSetupBuildInfo :: PI PN -> SetupBuildInfo -> FlaggedDeps Component PN
......