From 97c670b2ff01500dded536fa994cc7a2633e40e0 Mon Sep 17 00:00:00 2001 From: Neil Brown Date: Fri, 14 Dec 2007 04:13:01 +0000 Subject: [PATCH] Fixed and documented the checkOpposite function so that it works properly and the tests pass --- transformations/ArrayUsageCheck.hs | 36 +++++++++++++++++++++++++----- 1 file changed, 31 insertions(+), 5 deletions(-) diff --git a/transformations/ArrayUsageCheck.hs b/transformations/ArrayUsageCheck.hs index 6ea190e..3ea1df7 100644 --- a/transformations/ArrayUsageCheck.hs +++ b/transformations/ArrayUsageCheck.hs @@ -214,8 +214,10 @@ mygcd x y = gcd x y -- As an additional step not specified in the paper, equations with no variables in them are checked -- for consistency. That is, all equations c >= 0 (where c is constant) are checked to ensure c is indeed >= 0. pruneAndCheck :: InequalityProblem -> Maybe (EqualityProblem, InequalityProblem) -pruneAndCheck ineq = let (opps,others) = splitEither $ groupOpposites $ map pruneGroup groupedIneq in - seqPair (mapM checkOpposite opps, mapM checkConstantEq others) +pruneAndCheck ineq = do let (opps,others) = splitEither $ groupOpposites $ map pruneGroup groupedIneq + (opps', eq) <- mapM checkOpposite opps >>* splitEither + checked <- mapM checkConstantEq (concat opps' ++ others) + return (eq, checked) where groupedIneq = groupBy (\x y -> EQ == coeffSort x y) $ sortBy coeffSort ineq @@ -249,9 +251,33 @@ pruneAndCheck ineq = let (opps,others) = splitEither $ groupOpposites $ map prun where negTarget = map negate $ tail $ elems target - checkOpposite :: (InequalityConstraintEquation,InequalityConstraintEquation) -> Maybe EqualityConstraintEquation - checkOpposite (x,y) | (x ! 0) == negate (y ! 0) = Just x -- doesn't matter which we pick to become the equality - | otherwise = Nothing -- The inequalities can't hold + -- Checks if two "opposite" constraints are inconsistent. If they are inconsistent, Nothing is returned. + -- If they could be consistent, either the resulting equality or the inequalities are returned + -- + -- If the equations are opposite, then setting z = sum (1 .. n) of a_n . x_n, the two equations must be: + -- b + z >= 0 + -- c - z >= 0 + -- The choice of which equation is which is arbitrary. + -- + -- It is easily seen that adding the two equations gives: + -- + -- (b + c) >= 0 + -- + -- Therefore if (b + c) < 0, the equations are inconsistent. + -- If (b + c) = 0, we can substitute into the original equations b = -c: + -- -c + z >= 0 + -- c - z >= 0 + -- Rearranging both gives: + -- z >= c + -- z <= c + -- This implies c = z. Therefore we can take either of the original inequalities + -- and treat them directly as equality (c - z = 0, and b + z = 0) + -- If (b + c) > 0 then the equations are consistent but we cannot do anything new with them + checkOpposite :: (InequalityConstraintEquation,InequalityConstraintEquation) -> + Maybe (Either [InequalityConstraintEquation] EqualityConstraintEquation) + checkOpposite (x,y) | (x ! 0) + (y ! 0) < 0 = Nothing + | (x ! 0) + (y ! 0) == 0 = Just $ Right x + | otherwise = Just $ Left [x,y] checkConstantEq :: InequalityConstraintEquation -> Maybe InequalityConstraintEquation checkConstantEq eq | all (== 0) (tail $ elems eq) = if (eq ! 0) >= 0 then Just eq else Nothing