@@ -62,14 +62,34 @@ solve maxUniverseLevel ucs =
6262 ]
6363 }
6464
65− -- | a map from variables to the list of constraints the variable occurs in.
66− constraints :: M.Map Var (S.Set ConstraintFC)
67− constraints = M.fromListWith S.union
65+ lhs (ULT (UVar x) _) = Just (Var x)
66+ lhs (ULE (UVar x) _) = Just (Var x)
67+ lhs _ = Nothing
68+
69+ rhs (ULT _ (UVar x)) = Just (Var x)
70+ rhs (ULE _ (UVar x)) = Just (Var x)
71+ rhs _ = Nothing
72+
73+ -- | a map from variables to the list of constraints the variable occurs in. (in the LHS of a constraint)
74+ constraintsLHS :: M.Map Var (S.Set ConstraintFC)
75+ constraintsLHS = M.fromListWith S.union
6876 [ (v, S.singleton (ConstraintFC c fc))
69− | ConstraintFC c fc <- inpConstraints
77+ | (ConstraintFC c fc) <- inpConstraints
7078 , let vars = varsIn c
7179 , length vars > 1 -- do not register unary constraints
7280 , v <- vars
81+ , lhs c == Just v
82+ ]
83+
84+ -- | a map from variables to the list of constraints the variable occurs in. (in the RHS of a constraint)
85+ constraintsRHS :: M.Map Var (S.Set ConstraintFC)
86+ constraintsRHS = M.fromListWith S.union
87+ [ (v, S.singleton (ConstraintFC c fc))
88+ | (ConstraintFC c fc) <- inpConstraints
89+ , let vars = varsIn c
90+ , length vars > 1 -- do not register unary constraints
91+ , v <- vars
92+ , rhs c == Just v
7393 ]
7494
7595 -- | this is where the actual work is done.
@@ -87,15 +107,15 @@ solve maxUniverseLevel ucs =
87107 ULE a b -> do
88108 Domain lowerA upperA <- domainOf a
89109 Domain lowerB upperB <- domainOf b
90− when (upperB < upperA) $ updateDomainOf (ConstraintFC cons fc) a (Domain lowerA upperB)
91− when (lowerA > lowerB) $ updateDomainOf (ConstraintFC cons fc) b (Domain lowerA upperB)
110+ when (upperB < upperA) $ updateUpperBoundOf (ConstraintFC cons fc) a upperB
111+ when (lowerA > lowerB) $ updateLowerBoundOf (ConstraintFC cons fc) b lowerA
92112 ULT a b -> do
93113 Domain lowerA upperA <- domainOf a
94114 Domain lowerB upperB <- domainOf b
95115 let upperB_pred = pred upperB
96116 let lowerA_succ = succ lowerA
97− when (upperB_pred < upperA) $ updateDomainOf (ConstraintFC cons fc) a (Domain lowerA upperB_pred)
98− when (lowerA_succ > lowerB) $ updateDomainOf (ConstraintFC cons fc) b (Domain lowerA_succ upperB)
117+ when (upperB_pred < upperA) $ updateUpperBoundOf (ConstraintFC cons fc) a upperB_pred
118+ when (lowerA_succ > lowerB) $ updateLowerBoundOf (ConstraintFC cons fc) b lowerA_succ
99119 propagate
100120
101121 -- | extract a solution from the state.
@@ -121,12 +141,11 @@ solve maxUniverseLevel ucs =
121141 domainOf (UVar var) = gets (fst . (M.! Var var) . domainStore)
122142 domainOf (UVal val) = return (Domain val val)
123143
124− -- | updates the domain of a variable.
125− -- this function is also where we fail, inc ase of a domain wipe-out.
126− updateDomainOf :: ConstraintFC -> UExp -> Domain -> StateT SolverState TC ()
127− updateDomainOf suspect (UVar var) newDom = do
144+ updateUpperBoundOf :: ConstraintFC -> UExp -> Int -> StateT SolverState TC ()
145+ updateUpperBoundOf suspect (UVar var) upper = do
128146 doms <- gets domainStore
129− let (oldDom, suspects) = doms M.! Var var
147+ let (oldDom@(Domain lower _), suspects) = doms M.! Var var
148+ let newDom = Domain lower upper
130149 when (wipeOut newDom) $ lift $ Error $ At (ufc suspect) $ Msg $ unlines
131150 $ "Universe inconsistency."
132151 : ("Working on: " ++ show (UVar var))
@@ -135,17 +154,48 @@ solve maxUniverseLevel ucs =
135154 : "Involved constraints: "
136155 : map (("\t"++) . show) (suspect : S.toList suspects)
137156 modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }
138− addToQueue (Var var)
139− updateDomainOf _ UVal{} _ = return ()
157+ addToQueueRHS (uconstraint suspect) (Var var)
158+ updateUpperBoundOf _ UVal{} _ = return ()
159+
160+ updateLowerBoundOf :: ConstraintFC -> UExp -> Int -> StateT SolverState TC ()
161+ updateLowerBoundOf suspect (UVar var) lower = do
162+ doms <- gets domainStore
163+ let (oldDom@(Domain _ upper), suspects) = doms M.! Var var
164+ let newDom = Domain lower upper
165+ when (wipeOut newDom) $ lift $ Error $ At (ufc suspect) $ Msg $ unlines
166+ $ "Universe inconsistency."
167+ : ("Working on: " ++ show (UVar var))
168+ : ("Old domain: " ++ show oldDom)
169+ : ("New domain: " ++ show newDom)
170+ : "Involved constraints: "
171+ : map (("\t"++) . show) (suspect : S.toList suspects)
172+ modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }
173+ addToQueueLHS (uconstraint suspect) (Var var)
174+ updateLowerBoundOf _ UVal{} _ = return ()
175+
176+ -- | add all constraints (with the given var on the lhs) to the queue
177+ addToQueueLHS :: MonadState SolverState m => UConstraint -> Var -> m ()
178+ addToQueueLHS thisCons var =
179+ case M.lookup var constraintsLHS of
180+ Nothing -> return ()
181+ Just cs -> do
182+ Queue list set <- gets queue
183+ let set' = S.insert thisCons set
184+ let newCons = [ c | c <- S.toList cs, uconstraint c `S.notMember` set' ]
185+ if null newCons
186+ then return ()
187+ else modify $ \ st -> st { queue = Queue (list ++ newCons)
188+ (S.union set (S.fromList (map uconstraint newCons))) }
140189
141− -- | add all constraints related to a variable.
142− addToQueue :: MonadState SolverState m => Var -> m ()
143− addToQueue var =
144− case M.lookup var constraints of
190+ -- | add all constraints (with the given var on the rhs) to the queue
191+ addToQueueRHS :: MonadState SolverState m => UConstraint -> Var -> m ()
192+ addToQueueRHS thisCons var =
193+ case M.lookup var constraintsRHS of
145194 Nothing -> return ()
146195 Just cs -> do
147196 Queue list set <- gets queue
148− let newCons = [ c | c <- S.toList cs, uconstraint c `S.notMember` set ]
197+ let set' = S.insert thisCons set
198+ let newCons = [ c | c <- S.toList cs, uconstraint c `S.notMember` set' ]
149199 if null newCons
150200 then return ()
151201 else modify $ \ st -> st { queue = Queue (list ++ newCons)