From 8ec4832a03a2602dbb64b1e698d48ea04503fef2 Mon Sep 17 00:00:00 2001 From: Neil Brown Date: Wed, 9 Jan 2008 12:27:02 +0000 Subject: [PATCH] Removed the unused half of VariableMapping --- transformations/ArrayUsageCheck.hs | 88 +++--------------------------- 1 file changed, 9 insertions(+), 79 deletions(-) diff --git a/transformations/ArrayUsageCheck.hs b/transformations/ArrayUsageCheck.hs index bb32df4..67b4dda 100644 --- a/transformations/ArrayUsageCheck.hs +++ b/transformations/ArrayUsageCheck.hs @@ -230,34 +230,23 @@ type InequalityProblem = [InequalityConstraintEquation] -- x_k = a_k'.x_k' + sum (i = 0 .. n without k) of a_i . x_i -- where a_k' can be zero (no new variable is introduced). -- --- We want to keep a record of these substitutions, for two eventualities: --- * When we end up with a list of inequalities, we can express these inequalities --- in terms of the original variables (even if that may be slightly messy) --- * If we end up with no remaining inequalities, we know the exact results +-- We want to keep a record of these substitutions because then +-- if we end up with no remaining inequalities, we know the exact results -- assigned to each of our variables -- --- The first item in that list requires that we can map from the transformed variables --- back to the original; that is we can map from x_k' back to x_k. --- The second item in that list requires us to know the substitution for x_k; that is, +-- We need to know the substitution for x_k; that is, -- we can map from x_k to the RHS of its substitution (including the resolved value for x_k'). --- --- To achieve this, we keep track of two things. --- * The first is a map from all the current variables back to the original variables. --- Because of the way the subsitutions are performed, the coefficients must be fractions. --- * The second is a map from the original variables into the current variables. --- This does not require fractional coefficients. --- To get the final value for an original variable, you map "through" the second item, --- and then back through the first item. This may seem odd, but that's the way it is! -type VariableMapping = (Map.Map CoeffIndex (Array CoeffIndex Rational),Map.Map CoeffIndex EqualityConstraintEquation) +-- We keep a map from the original variables into the current variables. +-- This does not require fractional coefficients. +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,toRational $ if i == j then 1 else 0) | j <- [0 .. n]]) | i <- [0 .. n]], - Map.fromList $ [ (i,array (0,n) [(j,if i == j then 1 else 0) | j <- [0 .. n]]) | i <- [0 .. n]]) +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. The first parameter is (k,value of old x_k) addToMapping :: (CoeffIndex,EqualityConstraintEquation) -> VariableMapping -> VariableMapping -addToMapping (k, subst) = transformPair addNewToOld addOldToNew +addToMapping (k, subst) = addOldToNew where -- We want to update all the existing entries to be scaled according to the new substitution. -- Additionally, iff there was no previous entry for k, we should add the new substitution. @@ -287,71 +276,12 @@ addToMapping (k, subst) = transformPair addNewToOld addOldToNew where eq_k = eq ! k - -- We want to record the new mapping for x_k'. This only need be done if a_k' is not zero - -- (i.e. a new variable is being introduced). If no new variable is being introduced, the existing mapping - -- can remain untouched. - -- From the comment on VariableMapping we have: - -- x_k = a_k'.x_k' + sum (i = 0 .. n without k) of a_i . x_i - -- Therefore: - -- x_k' = (x_k - sum (i = 0 .. n without k) of a_i . x_i) / a_k' - -- - -- So we must take the current mapping for x_k (Remember, x_k here may not be the totally-original x_k), - -- scale it by (1/a_k') and - -- then for each i (i != k) we must multiply the current mapping of x_i by (-a_i / a_k') - -- and add the whole lot together to get the new substitution. - -- - -- As a readable example, you currently have a plain map: - -- - -- x = x - -- - -- You get a new substitution: - -- - -- x = -8sigma - 4y - z - 1 - -- - -- The sigma variable will effectively replace x. Therefore you need to set a new mapping: - -- - -- sigma = (x - 4y - z - 1) / (-8) - -- - -- Later when you want to record a mapping for y: - -- - -- y = sigma + 3 * tau - -- - -- You will try to get a tau mapping (tau replaces y): - -- - -- tau = (y - sigma) / 3 - -- - -- At which point you must substitute in the sigma mapping: - -- - -- tau = (y - ((x - 4y - z - 1) / (-8))) / 3 - -- - -- Which gives: - -- - -- tau = ((-1/8)x + (1/2)y + (-1/8)z + (-1/8)) / 3 - -- tau = (-1/24)x + (1/6)y + (-1/24)z + (-1/24) - - addNewToOld :: Map.Map CoeffIndex (Array CoeffIndex Rational) -> Map.Map CoeffIndex (Array CoeffIndex Rational) - addNewToOld before | a_k' == 0 = before - | otherwise = (flip $ Map.insert k) before $ foldl1 (arrayZipWith (+)) $ map (uncurry change) $ Map.assocs before - where - change :: CoeffIndex -> Array CoeffIndex Rational -> Array CoeffIndex Rational - change ind val | ind == 0 = val -- shortcut - | ind == k = scaleEq ((1 :: Integer) `over` a_k') (forceLookup k before) - | otherwise = scaleEq ((negate (val ! ind)) `over` a_k') (forceLookup ind before) - - over x y = (toRational x) / (toRational y) - - a_k' = subst ! k - - - -- TODO could maybe use a proper error monad instead - forceLookup k m = fromJust $ Map.lookup k m - -- | Returns a mapping from i to constant values of x_i for the solutions of the equations. -- This function should only be called if the VariableMapping comes from a problem that -- definitely has constant solutions after all equalities have been eliminated. -- If variables remain in the inequalities, you will get invalid\/odd answers from this function. getCounterEqs :: VariableMapping -> Map.Map CoeffIndex Integer -getCounterEqs (_, origToLast) = Map.delete 0 $ Map.map expressAsConst origToLast +getCounterEqs origToLast = Map.delete 0 $ Map.map expressAsConst origToLast where expressAsConst rhs = rhs ! 0