suzanne.soy/tock-mirror
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Removed the unused half of VariableMapping

Browse Source
This commit is contained in:
Neil Brown 2008-01-09 12:27:02 +00:00
parent 57f18e5b18
commit 8ec4832a03
1 changed files with 9 additions and 79 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

88
transformations/ArrayUsageCheck.hs
View File

@ -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