@@ -73,13 +73,15 @@ solve maxUniverseLevel inpConstraints =
73 ULE a b -> do
73 ULE a b -> do
74 (lowerA, upperA) <- domainOf a
74 (lowerA, upperA) <- domainOf a
75 (lowerB, upperB) <- domainOf b
75 (lowerB, upperB) <- domainOf b
76− updateDomainOf (cons, fc) a (lowerA, min upperA upperB)
76+ when (upperB < upperA) $ updateDomainOf (cons, fc) a (lowerA, upperB)
77− updateDomainOf (cons, fc) b (max lowerB lowerA, upperB)
77+ when (lowerA > lowerB) $ updateDomainOf (cons, fc) b (lowerA, upperB)
78 ULT a b -> do
78 ULT a b -> do
79 (lowerA, upperA) <- domainOf a
79 (lowerA, upperA) <- domainOf a
80 (lowerB, upperB) <- domainOf b
80 (lowerB, upperB) <- domainOf b
81− updateDomainOf (cons, fc) a (lowerA, min upperA (pred upperB))
81+ let upperB_pred = pred upperB
82− updateDomainOf (cons, fc) b (max lowerB (succ lowerA), upperB)
82+ let lowerA_succ = succ lowerA
83+ when (upperB_pred < upperA) $ updateDomainOf (cons, fc) a (lowerA, upperB_pred)
84+ when (lowerA_succ > lowerB) $ updateDomainOf (cons, fc) b (lowerA_succ, upperB)
85 -- | extract a solution from the state.
87 -- | extract a solution from the state.
@@ -105,21 +107,18 @@ solve maxUniverseLevel inpConstraints =
105 -- | updates the domain of a variable.
107 -- | updates the domain of a variable.
106 -- this function is also where we fail, inc ase of a domain wipe-out.
108 -- this function is also where we fail, inc ase of a domain wipe-out.
107 updateDomainOf :: (UConstraint, FC) -> UExp -> (Int, Int) -> StateT SolverState TC ()
109 updateDomainOf :: (UConstraint, FC) -> UExp -> (Int, Int) -> StateT SolverState TC ()
108− updateDomainOf suspect (UVar var) dom = do
110+ updateDomainOf suspect (UVar var) newDom = do
109 doms <- gets domainStore
111 doms <- gets domainStore
110 let (oldDom, suspects) = doms M.! Var var
112 let (oldDom, suspects) = doms M.! Var var
111− let newDom = domainIntersect oldDom dom
112 when (wipeOut newDom) $ lift $ Error $ Msg $ unlines
113 when (wipeOut newDom) $ lift $ Error $ Msg $ unlines
113 $ "Universe inconsistency."
114 $ "Universe inconsistency."
114 : ("Working on: " ++ show (UVar var))
115 : ("Working on: " ++ show (UVar var))
115 : ("Old domain: " ++ show oldDom)
116 : ("Old domain: " ++ show oldDom)
116− : ("Inp domain: " ++ show dom)
117 : ("New domain: " ++ show newDom)
117 : ("New domain: " ++ show newDom)
118 : "Involved constraints: "
118 : "Involved constraints: "
119 : map (("\t"++) . show) (suspect : S.toList suspects)
119 : map (("\t"++) . show) (suspect : S.toList suspects)
120− unless (oldDom == newDom) $ do
121− modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }
120+ modify $ \ st -> st { domainStore = M.insert (Var var) (newDom, S.insert suspect suspects) doms }
122− addToQueue (Var var)
121+ addToQueue (Var var)
123 updateDomainOf _ UVal{} _ = return ()
122 updateDomainOf _ UVal{} _ = return ()
125 -- | add all constraints related to a variable.
124 -- | add all constraints related to a variable.
@@ -129,10 +128,6 @@ solve maxUniverseLevel inpConstraints =
129 Nothing -> return ()
128 Nothing -> return ()
130 Just cs -> modify $ \ st -> st { queue = S.union cs (queue st) }
129 Just cs -> modify $ \ st -> st { queue = S.union cs (queue st) }
132− -- | intersecting two domains, the resulting domain can be wiped out.
133− domainIntersect :: (Int, Int) -> (Int, Int) -> (Int, Int)
134− domainIntersect (a,b) (c,d) = (max a c, min b d)
136 -- | check if a domain is wiped out.
131 -- | check if a domain is wiped out.
137 wipeOut :: (Int, Int) -> Bool
132 wipeOut :: (Int, Int) -> Bool
138 wipeOut (l, u) = l > u
133 wipeOut (l, u) = l > u