diff --git a/transformations/ArrayUsageCheck.hs b/transformations/ArrayUsageCheck.hs index 660d415..07aec9f 100644 --- a/transformations/ArrayUsageCheck.hs +++ b/transformations/ArrayUsageCheck.hs @@ -97,7 +97,6 @@ makeEquations es high = makeEquations' >>* (\(s,v,lh) -> (s,(pairEqs v, getIneqs getLH (sc, eq) = [eq `addEq` (scaleEq (-sc) low),(scaleEq sc high) `addEq` amap negate eq] addEq = arrayZipWith (+) - scaleEq n = amap (* n) makeEquation :: (Integer,[FlattenedExp]) -> StateT (Map.Map String Int) (Either String) (Integer,EqualityConstraintEquation) makeEquation (divisor, summedItems) @@ -125,14 +124,34 @@ type EqualityProblem = [EqualityConstraintEquation] type InequalityConstraintEquation = Array CoeffIndex Integer type InequalityProblem = [InequalityConstraintEquation] +-- Maps the indexes of the current variables to an equation involving the original variables +type VariableMapping = Map.Map CoeffIndex EqualityConstraintEquation + +-- | Given a maximum variable, produces a default mapping +defaultMapping :: Int -> VariableMapping +defaultMapping n = Map.fromList $ [ (i,array (0,n) [(j,if i == j then 1 else 0) | j <- [0 .. n]]) | i <- [0 .. n]] + +-- | Adds a new variable to a map +addToMapping :: (CoeffIndex,EqualityConstraintEquation) -> VariableMapping -> VariableMapping +addToMapping (k,eq) old = Map.insert k trans old + where + trans = foldl1 (arrayZipWith (+)) $ map (\(k,v) -> scaleEq v (forceLookup k old)) $ assocs eq + forceLookup k m = fromJust $ Map.lookup k m + +reverseEquality :: EqualityConstraintEquation -> VariableMapping -> EqualityConstraintEquation +reverseEquality eq mp = foldl1 (arrayZipWith (+)) $ map (\(k,v) -> scaleEq v (forceLookup k mp)) $ assocs eq + where + forceLookup k m = fromJust $ Map.lookup k m + +scaleEq :: Integer -> EqualityConstraintEquation -> EqualityConstraintEquation +scaleEq n = amap (* n) + -- | Solves all the constraints in the Equality Problem (taking them to be == 0), --- and transforms the InequalityProblems appropriately. --- TODO the function currently doesn't record the relation between the transformed variables --- (e.g. sigma for x_k) and the original variables (x_k). In order to feed back useful --- information to the user, we should do this at some point in future. -solveConstraints :: EqualityProblem -> InequalityProblem -> Maybe InequalityProblem -solveConstraints p ineq - = normaliseEq p >>= (\p' -> execStateT (solve p') ineq) +-- and transforms the InequalityProblems appropriately. It also records +-- a variable mapping so that we can feed back the final answer to the user +solveConstraints :: VariableMapping -> EqualityProblem -> InequalityProblem -> Maybe (VariableMapping, InequalityProblem) +solveConstraints vm p ineq + = normaliseEq p >>= (\p' -> execStateT (solve p') (vm,ineq)) where -- | Normalises an equation by dividing all coefficients by their greatest common divisor. -- If the unit coefficient (a_0) doesn't divide by this GCD, Nothing will be returned @@ -148,7 +167,7 @@ solveConstraints p ineq -- | Solves all equality problems in the given list. -- Will either succeed (Just () in the Error\/Maybe monad) or fail (Nothing) - solve :: EqualityProblem -> StateT InequalityProblem Maybe () + solve :: EqualityProblem -> StateT (VariableMapping, InequalityProblem) Maybe () solve [] = return () solve p = (solveUnits p >>* removeRedundant) >>= liftF checkFalsifiable >>= solveNext >>= solve @@ -177,21 +196,25 @@ solveConstraints p ineq -- all the equations in the list by adding x_k_val (scaled by a_k) to each equation and -- then zeroing out the a_k value. Note that the (x_k_val ! k) value will be ignored; -- it should be zero, in any case (otherwise x_k would be defined in terms of itself!). - substIn :: CoeffIndex -> Array CoeffIndex Integer -> EqualityProblem -> EqualityProblem - substIn k x_k_val = map substIn' + substIn :: CoeffIndex -> Array CoeffIndex Integer -> (VariableMapping, EqualityProblem) -> (VariableMapping, EqualityProblem) + substIn k x_k_val = transformPair (addToMapping (k,x_k_val)) (map substIn') where substIn' eq = (arrayZipWith (+) eq scaled_x_k_val) // [(k,0)] where scaled_x_k_val = amap (* (eq ! k)) x_k_val -- | Solves (i.e. removes by substitution) all unit coefficients in the given list of equations. - solveUnits :: EqualityProblem -> StateT InequalityProblem Maybe EqualityProblem + solveUnits :: EqualityProblem -> StateT (VariableMapping, InequalityProblem) Maybe EqualityProblem solveUnits p = case findFirstUnit p of (Nothing,p') -> return p' -- p' should equal p anyway - (Just (eq,ind),p') -> modify change >> ((lift $ normaliseEq $ change p') >>= solveUnits) + (Just (eq,ind),p') -> modify change >> change' p' >>= liftF normaliseEq >>= solveUnits where change = substIn ind (arrayMapWithIndex (modifyOthersZeroSpecific ind) eq) + change' p = do (mp,ineq) <- get + let (mp',p') = change (mp,p) + put (mp',ineq) + return p' origVal = eq ! ind -- Zeroes a specific coefficient, modifies the others as follows: @@ -216,14 +239,20 @@ solveConstraints p ineq cmpAbsSnd (_,x) (_,y) = compare (abs x) (abs y) -- | Solves the next equality and returns the new set of equalities. - solveNext :: EqualityProblem -> StateT InequalityProblem Maybe EqualityProblem + solveNext :: EqualityProblem -> StateT (VariableMapping, InequalityProblem) Maybe EqualityProblem solveNext [] = return [] solveNext (e:es) = -- We transform the kth variable into sigma, effectively -- So once we have x_k = ... (in terms of sigma) we add a_k * RHS -- to all other equations, AFTER zeroing the a_k coefficient (so -- that the multiple of sigma is added on properly) - modify (map alterEquation) >> (lift $ (normaliseEq . map alterEquation) (e:es)) + modify change >> change' (e:es) >>= liftF normaliseEq where + change' p = do (mp,ineq) <- get + let (mp',p') = change (mp,p) + put (mp',ineq) + return p' + change = transformPair (addToMapping (k,x_k_eq)) (map alterEquation) + -- | Adds a scaled version of x_k_eq onto the current equation, after zeroing out -- the a_k coefficient in the current equation. alterEquation :: EqualityConstraintEquation -> EqualityConstraintEquation @@ -355,9 +384,12 @@ pruneAndCheck ineq = do let (opps,others) = splitEither $ groupOpposites $ map p -- | Returns Nothing if there is definitely no solution, or (Just ineq) if -- further investigation is needed -solveAndPrune :: EqualityProblem -> InequalityProblem -> Maybe InequalityProblem -solveAndPrune [] ineq = return ineq -solveAndPrune eq ineq = solveConstraints eq ineq >>= pruneAndCheck >>= uncurry solveAndPrune +solveAndPrune' :: VariableMapping -> EqualityProblem -> InequalityProblem -> Maybe (VariableMapping,InequalityProblem) +solveAndPrune' vm [] ineq = return (vm,ineq) +solveAndPrune' vm eq ineq = solveConstraints vm eq ineq >>= (seqPair . transformPair return pruneAndCheck) >>= (\(x,(y,z)) -> solveAndPrune' x y z) + +solveAndPrune :: EqualityProblem -> InequalityProblem -> Maybe (VariableMapping,InequalityProblem) +solveAndPrune eq = solveAndPrune' (defaultMapping $ snd $ bounds $ head eq) eq -- | Returns the number of variables (of x_1 .. x_n; x_0 is not counted) -- that have non-zero coefficients in the given inequality problems. diff --git a/transformations/RainUsageCheckTest.hs b/transformations/RainUsageCheckTest.hs index c2ea8c8..c7ba62a 100644 --- a/transformations/RainUsageCheckTest.hs +++ b/transformations/RainUsageCheckTest.hs @@ -326,18 +326,20 @@ testArrayCheck = TestList -- Impossible/inconsistent equality constraints: -- -7 = 0 - ,TestCase $ assertEqual "testArrayCheck 1002" (Nothing) (solveConstraints [simpleArray [(0,7),(1,0)]] []) + ,TestCase $ assertEqual "testArrayCheck 1002" (Nothing) (solveConstraints' [simpleArray [(0,7),(1,0)]] []) -- x_1 = 3, x_1 = 4 - ,TestCase $ assertEqual "testArrayCheck 1003" (Nothing) (solveConstraints [simpleArray [(0,-3),(1,1)], simpleArray [(0,-4),(1,1)]] []) + ,TestCase $ assertEqual "testArrayCheck 1003" (Nothing) (solveConstraints' [simpleArray [(0,-3),(1,1)], simpleArray [(0,-4),(1,1)]] []) -- x_1 + x_2 = 0, x_1 + x_2 = -3 - ,TestCase $ assertEqual "testArrayCheck 1004" (Nothing) (solveConstraints [simpleArray [(0,0),(1,1),(2,1)], simpleArray [(0,3),(1,1),(2,1)]] []) + ,TestCase $ assertEqual "testArrayCheck 1004" (Nothing) (solveConstraints' [simpleArray [(0,0),(1,1),(2,1)], simpleArray [(0,3),(1,1),(2,1)]] []) -- 4x_1 = 7 - ,TestCase $ assertEqual "testArrayCheck 1005" (Nothing) (solveConstraints [simpleArray [(0,-7),(1,4)]] []) + ,TestCase $ assertEqual "testArrayCheck 1005" (Nothing) (solveConstraints' [simpleArray [(0,-7),(1,4)]] []) ] where + solveConstraints' = solveConstraints undefined + pass :: (Int, [[Integer]], [[Integer]], [[Integer]]) -> Test pass (ind, expIneq, inpEq, inpIneq) = TestCase $ assertEqual ("testArrayCheck " ++ show ind) - (Just $ map arrayise expIneq) (solveConstraints (map arrayise inpEq) (map arrayise inpIneq)) + (Just $ map arrayise expIneq) (transformMaybe snd $ solveConstraints' (map arrayise inpEq) (map arrayise inpIneq)) arrayise :: [Integer] -> Array Int Integer arrayise = simpleArray . zip [0..] @@ -432,7 +434,7 @@ testIndexes = TestList let ineq' = (uncurry solveAndPrune) (makeConsistent eq ineq) in case ineq' of Nothing -> assertFailure $ "testIndexes " ++ show ind ++ " expected to pass (solving+pruning) but failed; problem: " ++ show (eq,ineq) - Just ineq'' -> + Just (_,ineq'') -> if numVariables ineq'' <= 1 then return () -- Until we put in the route from original to mapped variables, @@ -442,16 +444,16 @@ testIndexes = TestList hardSolved :: (Int, [HandyEq], [HandyIneq]) -> Test hardSolved (ind, eq, ineq) = TestCase $ assertBool ("testIndexes " ++ show ind) $ isJust $ - (uncurry solveAndPrune) (makeConsistent eq ineq) >>= (pruneAndCheck . fmElimination) + (transformMaybe snd . uncurry solveAndPrune) (makeConsistent eq ineq) >>= (pruneAndCheck . fmElimination) notSolveable :: (Int, [HandyEq], [HandyIneq]) -> Test notSolveable (ind, eq, ineq) = TestCase $ assertEqual ("testIndexes " ++ show ind) Nothing $ - (uncurry solveAndPrune) (makeConsistent eq ineq) >>* ((<= 1) . numVariables) + (transformMaybe snd . uncurry solveAndPrune) (makeConsistent eq ineq) >>* ((<= 1) . numVariables) neverSolveable :: (Int, [HandyEq], [HandyIneq]) -> Test neverSolveable (ind, eq, ineq) = TestCase $ assertEqual ("testIndexes " ++ show ind) Nothing $ - (uncurry solveAndPrune) (makeConsistent eq ineq) >>= (pruneAndCheck . fmElimination) + (transformMaybe snd . uncurry solveAndPrune) (makeConsistent eq ineq) >>= (pruneAndCheck . fmElimination) -- The easy way of writing equations is built on the following Haskell magic. @@ -578,8 +580,8 @@ qcOmegaEquality = [scaleQC (40,200,2000,10000) prop] where prop (OMI (eq,ineq)) = omegaCheck actAnswer where - actAnswer = solveConstraints eq ineq - omegaCheck (Just ineqs) = all (all (== 0) . elems) ineqs + actAnswer = solveConstraints undefined eq ineq + omegaCheck (Just (_,ineqs)) = all (all (== 0) . elems) ineqs omegaCheck Nothing = False type MutatedEquation =