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

Overhauled the ArrayUsageCheck system to label the resulting problems with the expressions of the two array indexes involved in each problem, and changed the tests accordingly

Browse Source
This commit is contained in:
Neil Brown 2008-01-26 22:16:42 +00:00
parent 7e7395d47f
commit 127cdea242
2 changed files with 167 additions and 95 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

136
transformations/ArrayUsageCheck.hs
View File

@ -33,6 +33,7 @@ import FlowGraph
import Metadata import Metadata
import Omega import Omega
import Pass import Pass
import ShowCode
import Types import Types
import UsageCheck import UsageCheck
import Utils import Utils
@ -92,11 +93,21 @@ checkArrayUsage graph = sequence_ $ checkPar checkArrayUsage' graph
Left err -> dieP m $ "Could not work with array indexes for array \"" ++ userArrName ++ "\": " ++ err Left err -> dieP m $ "Could not work with array indexes for array \"" ++ userArrName ++ "\": " ++ err
Right [] -> return () -- No problems to work with Right [] -> return () -- No problems to work with
Right problems -> Right problems ->
case mapMaybe (\(vm,p) -> seqPair (return vm,uncurry solveProblem p)) problems of case mapMaybe solve problems of
-- No solutions; no worries! -- No solutions; no worries!
[] -> return () [] -> return ()
((varMapping,vm):_) -> do sol <- formatSolution varMapping (getCounterEqs vm) (((lx,ly),varMapping,vm):_) ->
dieP m $ "Overlapping indexes of array \"" ++ userArrName ++ "\" when: " ++ sol do sol <- formatSolution varMapping (getCounterEqs vm)
cx <- showCode lx
cy <- showCode ly
dieP m $ "Overlapping indexes of array \"" ++ userArrName ++ "\""
++ "(\"" ++ cx ++ "\" could overlap with \"" ++ cy ++ "\")"
++ " when: " ++ sol
solve :: (labels,vm,(EqualityProblem,InequalityProblem)) -> Maybe (labels,vm,VariableMapping)
solve (ls,vm,(eq,ineq)) = case solveProblem eq ineq of
Nothing -> Nothing
Just vm' -> Just (ls,vm,vm')
formatSolution :: VarMap -> Map.Map CoeffIndex Integer -> m String formatSolution :: VarMap -> Map.Map CoeffIndex Integer -> m String
formatSolution varToIndex indexToConst = do names <- mapM valOfVar $ Map.assocs varToIndex formatSolution varToIndex indexToConst = do names <- mapM valOfVar $ Map.assocs varToIndex
@ -170,10 +181,10 @@ onlyConst _ = Nothing
-- With a Replicated, each item in the left branch can be paired with each item in the right branch. -- With a Replicated, each item in the left branch can be paired with each item in the right branch.
-- Each item in the left branch can be paired with each other, and each item in the left branch can -- Each item in the left branch can be paired with each other, and each item in the left branch can
-- be paired with all other items. -- be paired with all other items.
data ArrayAccess = data ArrayAccess label =
Single (ArrayAccessType, (EqualityConstraintEquation, EqualityProblem, InequalityProblem)) Single (label, ArrayAccessType, (EqualityConstraintEquation, EqualityProblem, InequalityProblem))
| Group [(ArrayAccessType, (EqualityConstraintEquation, EqualityProblem, InequalityProblem))] | Group [(label, ArrayAccessType, (EqualityConstraintEquation, EqualityProblem, InequalityProblem))]
| Replicated [ArrayAccess] [ArrayAccess] | Replicated [ArrayAccess label] [ArrayAccess label]
data ArrayAccessType = AAWrite | AARead data ArrayAccessType = AAWrite | AARead
@ -231,30 +242,41 @@ type VarMap = Map.Map FlattenedExp Int
-- The remainder of the work (correctly pairing equations) is done by -- The remainder of the work (correctly pairing equations) is done by
-- squareAndPair. -- squareAndPair.
makeReplicatedEquations :: [(A.Variable, A.Expression, A.Expression)] -> ([A.Expression],[A.Expression]) -> A.Expression -> makeReplicatedEquations :: [(A.Variable, A.Expression, A.Expression)] -> ([A.Expression],[A.Expression]) -> A.Expression ->
Either String [(VarMap, (EqualityProblem, InequalityProblem))] Either String [((A.Expression, A.Expression), VarMap, (EqualityProblem, InequalityProblem))]
makeReplicatedEquations repVars accesses bound makeReplicatedEquations repVars accesses bound
= do flattenedAccesses <- applyPairM (mapM flatten) accesses = do flattenedAccesses <- applyPairM (mapM copyAndFlatten) accesses
let flattenedAccessesMirror = applyPair concat $ unzip $ map (\(v,_,_) -> applyPair (map (setIndexVar v 1)) flattenedAccesses) repVars let flattenedAccessesMirror = applyPair (map mirrorAllVars) flattenedAccesses
bound' <- flatten bound bound' <- flatten bound
((v,h,repVars',repVarIndexes),s) <- (flip runStateT) Map.empty $ ((v,h,repVars',repVarIndexes),s) <- (flip runStateT) Map.empty $
do repVars' <- mapM (\(v,s,c) -> do repVars' <- mapM (\(v,s,c) ->
do s' <- lift (flatten s) >>= makeEquation (error "Type is irrelevant for replication count") do s' <- lift (flatten s) >>= makeEquation s (error "Type is irrelevant for replication count")
>>= getSingleAccessItem "Modulo or Divide not allowed in replication start" >>= getSingleAccessItem "Modulo or Divide not allowed in replication start"
c' <- lift (flatten c) >>= makeEquation (error "Type is irrelevant for replication count") c' <- lift (flatten c) >>= makeEquation c (error "Type is irrelevant for replication count")
>>= getSingleAccessItem "Modulo or Divide not allowed in replication count" >>= getSingleAccessItem "Modulo or Divide not allowed in replication count"
return (v,s',c')) repVars return (v,s',c')) repVars
accesses' <- mapM (makeEquationWithPossibleRepBounds repVars') =<< makeEquationsWR flattenedAccesses accesses' <- mapM (makeEquationWithPossibleRepBounds repVars') =<< makeEquationsWR flattenedAccesses
accesses'' <- mapM (makeEquationWithPossibleRepBounds repVars') =<< makeEquationsWR flattenedAccessesMirror accesses'' <- mapM (makeEquationWithPossibleRepBounds repVars') =<< makeEquationsWR flattenedAccessesMirror
high <- makeEquation (error "Type is irrelevant for uppper bound") bound' high <- makeEquation bound (error "Type is irrelevant for uppper bound") bound'
>>= getSingleAccessItem "Multiple possible upper bounds not supported" >>= getSingleAccessItem "Multiple possible upper bounds not supported"
repVarIndexes <- mapM (\(v,_,_) -> seqPair (varIndex (Scale 1 (v,0)), varIndex (Scale 1 (v,1)))) repVars repVarIndexes <- mapM (\(v,_,_) -> seqPair (varIndex (Scale 1 (v,0)), varIndex (Scale 1 (v,1)))) repVars
return (Replicated accesses' accesses'',high, repVars',repVarIndexes) return (Replicated accesses' accesses'',high, repVars',repVarIndexes)
return $ squareAndPair repVarIndexes s [v] (amap (const 0) h, addConstant (-1) h) return $ squareAndPair repVarIndexes s [v] (amap (const 0) h, addConstant (-1) h)
where where
makeEquationsWR :: ([[FlattenedExp]],[[FlattenedExp]]) -> StateT (VarMap) (Either String) [ArrayAccess] copyAndFlatten :: A.Expression -> Either String (A.Expression, [FlattenedExp])
makeEquationsWR (w,r) = do w' <- mapM (makeEquation AAWrite) w copyAndFlatten e = do f <- flatten e
r' <- mapM (makeEquation AARead) r return (e, f)
-- Mirrors all of repVars in the given equation
mirrorAllVars :: (A.Expression, [FlattenedExp]) -> (A.Expression, [FlattenedExp])
mirrorAllVars (e, f) = (e, foldl mirror f repVars)
where
mirror :: [FlattenedExp] -> (A.Variable, A.Expression, A.Expression) -> [FlattenedExp]
mirror exp (v,_,_) = setIndexVar v 1 exp
makeEquationsWR :: ([(A.Expression, [FlattenedExp])],[(A.Expression, [FlattenedExp])]) -> StateT (VarMap) (Either String) [ArrayAccess A.Expression]
makeEquationsWR (w,r) = do w' <- mapM (\(e,f) -> makeEquation e AAWrite f) w
r' <- mapM (\(e,f) -> makeEquation e AARead f) r
return (w' ++ r') return (w' ++ r')
@ -269,7 +291,7 @@ makeReplicatedEquations repVars accesses bound
setIndexVar' _ _ b e = (b,e) setIndexVar' _ _ b e = (b,e)
makeEquationWithPossibleRepBounds :: [(A.Variable, EqualityConstraintEquation, EqualityConstraintEquation)] -> makeEquationWithPossibleRepBounds :: [(A.Variable, EqualityConstraintEquation, EqualityConstraintEquation)] ->
ArrayAccess -> StateT (VarMap) (Either String) ArrayAccess ArrayAccess label -> StateT (VarMap) (Either String) (ArrayAccess label)
makeEquationWithPossibleRepBounds [] item = return item makeEquationWithPossibleRepBounds [] item = return item
makeEquationWithPossibleRepBounds ((v,lower,upper):vars) item makeEquationWithPossibleRepBounds ((v,lower,upper):vars) item
-- We fold over the variables, altering the items one at a time via mapM: -- We fold over the variables, altering the items one at a time via mapM:
@ -277,15 +299,16 @@ makeReplicatedEquations repVars accesses bound
flip addPossibleRepBound' (v,0,lower,upper) item' >>= flip addPossibleRepBound' (v,0,lower,upper) item' >>=
flip addPossibleRepBound' (v,1,lower,upper) flip addPossibleRepBound' (v,1,lower,upper)
addPossibleRepBound' :: ArrayAccess -> addPossibleRepBound' :: ArrayAccess label ->
(A.Variable, Int, EqualityConstraintEquation, EqualityConstraintEquation) -> (A.Variable, Int, EqualityConstraintEquation, EqualityConstraintEquation) ->
StateT (VarMap) (Either String) ArrayAccess StateT (VarMap) (Either String) (ArrayAccess label)
addPossibleRepBound' (Group accesses) v = mapM (seqPair . transformPair return (flip addPossibleRepBound v)) accesses >>* Group -- addPossibleRepBound' (Group accesses) v = mapM (seqPair . transformPair return (flip addPossibleRepBound v)) accesses >>* Group
addPossibleRepBound' (Group accesses) v = sequence [addPossibleRepBound acc v >>* (\acc' -> (l,t,acc')) | (l,t,acc) <- accesses ] >>* Group
addPossibleRepBound' (Replicated acc0 acc1) v addPossibleRepBound' (Replicated acc0 acc1) v
= do acc0' <- mapM (flip addPossibleRepBound' v) acc0 = do acc0' <- mapM (flip addPossibleRepBound' v) acc0
acc1' <- mapM (flip addPossibleRepBound' v) acc1 acc1' <- mapM (flip addPossibleRepBound' v) acc1
return $ Replicated acc0' acc1' return $ Replicated acc0' acc1'
addPossibleRepBound' (Single (t,acc)) v = addPossibleRepBound acc v >>* (\x -> Single (t,x)) addPossibleRepBound' (Single (l,t,acc)) v = addPossibleRepBound acc v >>* (\x -> Single (l,t,x))
addPossibleRepBound :: (EqualityConstraintEquation, EqualityProblem, InequalityProblem) -> addPossibleRepBound :: (EqualityConstraintEquation, EqualityProblem, InequalityProblem) ->
(A.Variable, Int, EqualityConstraintEquation, EqualityConstraintEquation) -> (A.Variable, Int, EqualityConstraintEquation, EqualityConstraintEquation) ->
@ -397,12 +420,12 @@ flatten other = throwError ("Unhandleable item found in expression: " ++ show ot
squareAndPair :: squareAndPair ::
[(CoeffIndex, CoeffIndex)] -> [(CoeffIndex, CoeffIndex)] ->
VarMap -> VarMap ->
[ArrayAccess] -> [ArrayAccess label] ->
(EqualityConstraintEquation, EqualityConstraintEquation) -> (EqualityConstraintEquation, EqualityConstraintEquation) ->
[(VarMap, (EqualityProblem, InequalityProblem))] [((label, label), VarMap, (EqualityProblem, InequalityProblem))]
squareAndPair repVars s v lh squareAndPair repVars s v lh
= [(s,squareEquations (eq,ineq ++ concat (applyAll (eq,ineq) (map addExtra repVars)))) = [(labels, s,squareEquations (eq,ineq ++ concat (applyAll (eq,ineq) (map addExtra repVars))))
| (eq,ineq) <- pairEqsAndBounds v lh | (labels, eq,ineq) <- pairEqsAndBounds v lh
,and (map (primeImpliesPlain (eq,ineq)) repVars) ,and (map (primeImpliesPlain (eq,ineq)) repVars)
] ]
where where
@ -434,8 +457,8 @@ getSingles err = mapM getSingle
getSingle _ = throwError err getSingle _ = throwError err
-} -}
getSingleAccessItem :: MonadTrans m => String -> ArrayAccess -> m (Either String) EqualityConstraintEquation getSingleAccessItem :: MonadTrans m => String -> ArrayAccess label -> m (Either String) EqualityConstraintEquation
getSingleAccessItem _ (Single (_,(acc,_,_))) = lift $ return acc getSingleAccessItem _ (Single (_,_,(acc,_,_))) = lift $ return acc
getSingleAccessItem err _ = lift $ throwError err getSingleAccessItem err _ = lift $ throwError err
{- {-
@ -455,22 +478,24 @@ getSingleItem err _ = lift $ throwError err
-- (unique, munged) variable name to variable-index in the equations. -- (unique, munged) variable name to variable-index in the equations.
-- TODO probably want to take this into the PassM monad at some point, to use the Meta in the error message -- TODO probably want to take this into the PassM monad at some point, to use the Meta in the error message
-- TODO allow "background knowledge" in the form of other equalities and inequalities -- TODO allow "background knowledge" in the form of other equalities and inequalities
makeEquations :: ([A.Expression],[A.Expression]) -> A.Expression -> Either String [(VarMap, (EqualityProblem, InequalityProblem))] makeEquations :: ([A.Expression],[A.Expression]) -> A.Expression -> Either String [((A.Expression, A.Expression), VarMap, (EqualityProblem, InequalityProblem))]
makeEquations (esW,esR) high = makeEquations' >>* uncurry3 (squareAndPair []) makeEquations (esW,esR) high = makeEquations' >>* uncurry3 (squareAndPair [])
where where
-- | The body of makeEquations; returns the variable mapping, the list of (nx,ex) pairs and a pair -- | The body of makeEquations; returns the variable mapping, the list of (nx,ex) pairs and a pair
-- representing the upper and lower bounds of the array (inclusive). -- representing the upper and lower bounds of the array (inclusive).
makeEquations' :: Either String (VarMap, [ArrayAccess], (EqualityConstraintEquation, EqualityConstraintEquation)) makeEquations' :: Either String (VarMap, [ArrayAccess A.Expression], (EqualityConstraintEquation, EqualityConstraintEquation))
makeEquations' = do ((v,h),s) <- (flip runStateT) Map.empty $ makeEquations' = do ((v,h),s) <- (flip runStateT) Map.empty $
do eqsW <- mapM (makeEquation AAWrite) =<< lift (mapM flatten esW) do eqsW <- mapM (makeEquationForItem AAWrite) esW
eqsR <- mapM (makeEquation AARead) =<< lift (mapM flatten esR) eqsR <- mapM (makeEquationForItem AARead) esR
high' <- (lift $ flatten high) >>= makeEquation (error "Type irrelevant for upper bound") high' <- (lift $ flatten high) >>= makeEquation high (error "Type irrelevant for upper bound")
>>= getSingleAccessItem "Multiple possible upper bounds not supported" >>= getSingleAccessItem "Multiple possible upper bounds not supported"
return (eqsW ++ eqsR,high') return (eqsW ++ eqsR,high')
return (s,v,(amap (const 0) h, addConstant (-1) h)) return (s,v,(amap (const 0) h, addConstant (-1) h))
makeEquationForItem :: ArrayAccessType -> A.Expression -> StateT VarMap (Either String) (ArrayAccess A.Expression)
makeEquationForItem t e = lift (flatten e) >>= makeEquation e t
-- | Finds the index associated with a particular variable; either by finding an existing index -- | Finds the index associated with a particular variable; either by finding an existing index
-- or allocating a new one. -- or allocating a new one.
@ -493,25 +518,33 @@ varIndex mod@(Modulo top bottom)
return ind return ind
-- | Pairs all possible combinations of the list of equations. -- | Pairs all possible combinations of the list of equations.
pairEqsAndBounds :: [ArrayAccess] -> (EqualityConstraintEquation, EqualityConstraintEquation) -> [(EqualityProblem, InequalityProblem)] pairEqsAndBounds :: [ArrayAccess label] -> (EqualityConstraintEquation, EqualityConstraintEquation) -> [((label,label),EqualityProblem, InequalityProblem)]
pairEqsAndBounds items bounds = (concatMap (uncurry pairEqs) . allPairs) items ++ concatMap pairRep items pairEqsAndBounds items bounds = (concatMap (uncurry pairEqs) . allPairs) items ++ concatMap pairRep items
where where
pairEqs :: ArrayAccess pairEqs :: ArrayAccess label
-> ArrayAccess -> ArrayAccess label
-> [(EqualityProblem, InequalityProblem)] -> [((label,label),EqualityProblem, InequalityProblem)]
pairEqs (Single acc) (Single acc') = maybeToList $ pairEqs' acc acc' pairEqs (Single acc) (Single acc') = maybeToList $ pairEqs'' acc acc'
pairEqs (Single acc) (Group accs) = mapMaybe (pairEqs' acc) accs pairEqs (Single acc) (Group accs) = mapMaybe (pairEqs'' acc) accs
pairEqs (Group accs) (Single acc) = mapMaybe (pairEqs' acc) accs pairEqs (Group accs) (Single acc) = mapMaybe (pairEqs'' acc) accs
pairEqs (Group accs) (Group accs') = mapMaybe (uncurry pairEqs') $ product2 (accs,accs') pairEqs (Group accs) (Group accs') = mapMaybe (uncurry pairEqs'') $ product2 (accs,accs')
pairEqs (Replicated rA rB) acc pairEqs (Replicated rA rB) lacc
= concatMap (pairEqs acc) rA = concatMap (pairEqs lacc) rA
pairEqs acc (Replicated rA rB) pairEqs lacc (Replicated rA rB)
= concatMap (pairEqs acc) rA = concatMap (pairEqs lacc) rA
-- Used to pair the items of a single instance of PAR replication with each other -- Used to pair the items of a single instance of PAR replication with each other
pairRep :: ArrayAccess -> [(EqualityProblem, InequalityProblem)] pairRep :: ArrayAccess label -> [((label,label),EqualityProblem, InequalityProblem)]
pairRep (Replicated rA rB) = (concatMap (uncurry pairEqs) $ product2 (rA,rB)) ++ concatMap (uncurry pairEqs) (allPairs rA) pairRep (Replicated rA rB) = concatMap (uncurry pairEqs) (product2 (rA,rB))
++ concatMap (uncurry pairEqs) (allPairs rA)
pairRep _ = [] pairRep _ = []
pairEqs'' :: (label, ArrayAccessType,(EqualityConstraintEquation, EqualityProblem, InequalityProblem))
-> (label, ArrayAccessType,(EqualityConstraintEquation, EqualityProblem, InequalityProblem))
-> Maybe ((label,label), EqualityProblem, InequalityProblem)
pairEqs'' (lx,x,x') (ly,y,y') = case pairEqs' (x,x') (y,y') of
Just (eq,ineq) -> Just ((lx,ly),eq,ineq)
Nothing -> Nothing
pairEqs' :: (ArrayAccessType,(EqualityConstraintEquation, EqualityProblem, InequalityProblem)) pairEqs' :: (ArrayAccessType,(EqualityConstraintEquation, EqualityProblem, InequalityProblem))
-> (ArrayAccessType,(EqualityConstraintEquation, EqualityProblem, InequalityProblem)) -> (ArrayAccessType,(EqualityConstraintEquation, EqualityProblem, InequalityProblem))
@ -535,13 +568,13 @@ getIneqs (low, high) = concatMap getLH
addEq = arrayZipWith' 0 (+) addEq = arrayZipWith' 0 (+)
-- | Given an expression, forms equations (and accompanying additional equation-sets) and returns it -- | Given an expression, forms equations (and accompanying additional equation-sets) and returns it
makeEquation :: ArrayAccessType -> [FlattenedExp] -> StateT VarMap (Either String) ArrayAccess makeEquation :: label -> ArrayAccessType -> [FlattenedExp] -> StateT VarMap (Either String) (ArrayAccess label)
makeEquation t summedItems makeEquation l t summedItems
= do eqs <- process summedItems = do eqs <- process summedItems
let eqs' = map (transformTriple mapToArray (map mapToArray) (map mapToArray)) eqs let eqs' = map (transformTriple mapToArray (map mapToArray) (map mapToArray)) eqs :: [(EqualityConstraintEquation, EqualityProblem, InequalityProblem)]
return $ case eqs' of return $ case eqs' of
[acc] -> Single (t,acc) [acc] -> Single (l,t,acc)
_ -> Group $ zip (repeat t) eqs' _ -> Group [(l,t,e) | e <- eqs']
where where
process :: [FlattenedExp] -> StateT VarMap (Either String) [(Map.Map Int Integer,[Map.Map Int Integer], [Map.Map Int Integer])] process :: [FlattenedExp] -> StateT VarMap (Either String) [(Map.Map Int Integer,[Map.Map Int Integer], [Map.Map Int Integer])]
process = foldM makeEquation' empty process = foldM makeEquation' empty
@ -662,3 +695,4 @@ squareEquations (eqs,ineqs) = uncurry transformPair (mkPair $ map $ makeSize (0,
where where
highest = maximum $ 0 : (concatMap indices $ eqs ++ ineqs) highest = maximum $ 0 : (concatMap indices $ eqs ++ ineqs)

126
transformations/ArrayUsageCheckTest.hs
View File

@ -23,6 +23,7 @@ import Data.Array.IArray
import Data.List import Data.List
import qualified Data.Map as Map import qualified Data.Map as Map
import Data.Maybe import Data.Maybe
import Data.Ord
import qualified Data.Set as Set import qualified Data.Set as Set
import Prelude hiding ((**),fail) import Prelude hiding ((**),fail)
import Test.HUnit import Test.HUnit
@ -260,20 +261,20 @@ testMakeEquations = TestLabel "testMakeEquations" $ TestList
[buildExpr $ Dy (Var "i") A.Mul (Lit $ intLiteral 2),exprVariable "j"],intLiteral 8) [buildExpr $ Dy (Var "i") A.Mul (Lit $ intLiteral 2),exprVariable "j"],intLiteral 8)
-- Testing (i REM 3) vs (4) -- Testing (i REM 3) vs (4)
,test (10,[ ,test' (10,[
(i_mod_mapping 3,[con 0 === con 4, i === con 0], leq [con 0,con 0,con 7] &&& leq [con 0,con 4,con 7]) ((0,1),i_mod_mapping 3,[con 0 === con 4, i === con 0], leq [con 0,con 0,con 7] &&& leq [con 0,con 4,con 7])
,(i_mod_mapping 3,[i ++ 3 ** j === con 4], leq [con 0,con 4,con 7] &&& leq [con 0,i ++ 3 ** j,con 7] &&& [i >== con 1] &&& [j <== con 0] &&& leq [con 0, i ++ 3 ** j, con 2]) ,((0,1),i_mod_mapping 3,[i ++ 3 ** j === con 4], leq [con 0,con 4,con 7] &&& leq [con 0,i ++ 3 ** j,con 7] &&& [i >== con 1] &&& [j <== con 0] &&& leq [con 0, i ++ 3 ** j, con 2])
,(i_mod_mapping 3,[i ++ 3 ** j === con 4], leq [con 0,con 4,con 7] &&& leq [con 0,i ++ 3 ** j,con 7] &&& [i <== con (-1)] &&& [j >== con 0] &&& leq [con (-2), i ++ 3 ** j, con 0]) ,((0,1),i_mod_mapping 3,[i ++ 3 ** j === con 4], leq [con 0,con 4,con 7] &&& leq [con 0,i ++ 3 ** j,con 7] &&& [i <== con (-1)] &&& [j >== con 0] &&& leq [con (-2), i ++ 3 ** j, con 0])
],[buildExpr $ Dy (Var "i") A.Rem (Lit $ intLiteral 3),intLiteral 4],intLiteral 8) ],[buildExpr $ Dy (Var "i") A.Rem (Lit $ intLiteral 3),intLiteral 4],intLiteral 8)
-- Testing ((3*i - 2*j REM 11) - 5) vs (i + j) -- Testing ((3*i - 2*j REM 11) - 5) vs (i + j)
-- Expressed as ((2 * (i - j)) + i) REM 11 - 5, and i + j -- Expressed as ((2 * (i - j)) + i) REM 11 - 5, and i + j
,test (11,[ ,test' (11,[
(_3i_2j_mod_mapping 11,[con (-5) === i ++ j, 3**i ++ (-2)**j === con 0], leq [con 0,con (-5),con 7] &&& leq [con 0,i ++ j,con 7]) ((0,1),_3i_2j_mod_mapping 11,[con (-5) === i ++ j, 3**i ++ (-2)**j === con 0], leq [con 0,con (-5),con 7] &&& leq [con 0,i ++ j,con 7])
,(_3i_2j_mod_mapping 11,[3**i ++ (-2)**j ++ 11 ** k ++ con (-5) === i ++ j], ,((0,1),_3i_2j_mod_mapping 11,[3**i ++ (-2)**j ++ 11 ** k ++ con (-5) === i ++ j],
leq [con 0,i ++ j,con 7] &&& leq [con 0,3**i ++ (-2)**j ++ 11 ** k ++ con (-5),con 7] leq [con 0,i ++ j,con 7] &&& leq [con 0,3**i ++ (-2)**j ++ 11 ** k ++ con (-5),con 7]
&&& [3**i ++ (-2)**j >== con 1] &&& [k <== con 0] &&& leq [con 0, 3**i ++ (-2)**j ++ 11 ** k, con 10]) &&& [3**i ++ (-2)**j >== con 1] &&& [k <== con 0] &&& leq [con 0, 3**i ++ (-2)**j ++ 11 ** k, con 10])
,(_3i_2j_mod_mapping 11,[3**i ++ (-2)**j ++ 11 ** k ++ con (-5) === i ++ j], ,((0,1),_3i_2j_mod_mapping 11,[3**i ++ (-2)**j ++ 11 ** k ++ con (-5) === i ++ j],
leq [con 0,i ++ j,con 7] &&& leq [con 0,3**i ++ (-2)**j ++ 11 ** k ++ con (-5),con 7] leq [con 0,i ++ j,con 7] &&& leq [con 0,3**i ++ (-2)**j ++ 11 ** k ++ con (-5),con 7]
&&& [3**i ++ (-2)**j <== con (-1)] &&& [k >== con 0] &&& leq [con (-10), 3**i ++ (-2)**j ++ 11 ** k, con 0]) &&& [3**i ++ (-2)**j <== con (-1)] &&& [k >== con 0] &&& leq [con (-10), 3**i ++ (-2)**j ++ 11 ** k, con 0])
],[buildExpr $ ],[buildExpr $
@ -288,7 +289,7 @@ testMakeEquations = TestLabel "testMakeEquations" $ TestList
,buildExpr $ Dy (Var "i") A.Add (Var "j")],intLiteral 8) ,buildExpr $ Dy (Var "i") A.Add (Var "j")],intLiteral 8)
-- Testing i REM 2 vs (i + 1) REM 4 -- Testing i REM 2 vs (i + 1) REM 4
,test (12,combine (i_ip1_mod_mapping 2 4) ,test' (12,combine (0,1) (i_ip1_mod_mapping 2 4)
[ [([con 0 === con 0],[]),rr_i_zero, rr_ip1_zero] [ [([con 0 === con 0],[]),rr_i_zero, rr_ip1_zero]
,[([con 0 === i ++ con 1 ++ 4**k],[]),rr_i_zero,rr_ip1_pos] ,[([con 0 === i ++ con 1 ++ 4**k],[]),rr_i_zero,rr_ip1_pos]
,[([con 0 === i ++ con 1 ++ 4**k],[]),rr_i_zero,rr_ip1_neg] ,[([con 0 === i ++ con 1 ++ 4**k],[]),rr_i_zero,rr_ip1_neg]
@ -305,72 +306,84 @@ testMakeEquations = TestLabel "testMakeEquations" $ TestList
-- TODO test REM + REM vs REM -- 27 combinations! -- TODO test REM + REM vs REM -- 27 combinations!
-- Testing i REM j vs 3 -- Testing i REM j vs 3
,test (100,[ ,test' (100,[
-- i = 0: -- i = 0:
(i_mod_j_mapping, [con 0 === con 3, i === con 0], leq [con 0, con 0, con 7] &&& leq [con 0, con 3, con 7]) ((0,1),i_mod_j_mapping, [con 0 === con 3, i === con 0], leq [con 0, con 0, con 7] &&& leq [con 0, con 3, con 7])
-- i positive, j positive, i REM j = i: -- i positive, j positive, i REM j = i:
,(i_mod_j_mapping, [i === con 3], [i >== con 1] &&& leq [con 0, i, j ++ con (-1)] &&& leq [con 0, i, con 7] &&& leq [con 0, con 3, con 7]) ,((0,1),i_mod_j_mapping, [i === con 3], [i >== con 1] &&& leq [con 0, i, j ++ con (-1)] &&& leq [con 0, i, con 7] &&& leq [con 0, con 3, con 7])
-- i positive, j positive, i REM j = i + k: -- i positive, j positive, i REM j = i + k:
,(i_mod_j_mapping, [i ++ k === con 3], [i >== con 1, k <== (-1)**j] &&& ,((0,1),i_mod_j_mapping, [i ++ k === con 3], [i >== con 1, k <== (-1)**j] &&&
leq [con 0, i ++ k, j ++ con (-1)] &&& leq [con 0, i ++ k, con 7] &&& leq [con 0, con 3, con 7]) leq [con 0, i ++ k, j ++ con (-1)] &&& leq [con 0, i ++ k, con 7] &&& leq [con 0, con 3, con 7])
-- i positive, j negative, i REM j = i: -- i positive, j negative, i REM j = i:
,(i_mod_j_mapping, [i === con 3], [i >== con 1] &&& leq [con 0, i, (-1)**j ++ con (-1)] &&& leq [con 0, i, con 7] &&& leq [con 0, con 3, con 7]) ,((0,1),i_mod_j_mapping, [i === con 3], [i >== con 1] &&& leq [con 0, i, (-1)**j ++ con (-1)] &&& leq [con 0, i, con 7] &&& leq [con 0, con 3, con 7])
-- i positive, j negative, i REM j = i + k: -- i positive, j negative, i REM j = i + k:
,(i_mod_j_mapping, [i ++ k === con 3], [i >== con 1, k <== j] &&& ,((0,1),i_mod_j_mapping, [i ++ k === con 3], [i >== con 1, k <== j] &&&
leq [con 0, i ++ k, (-1)**j ++ con (-1)] &&& leq [con 0, i ++ k, con 7] &&& leq [con 0, con 3, con 7]) leq [con 0, i ++ k, (-1)**j ++ con (-1)] &&& leq [con 0, i ++ k, con 7] &&& leq [con 0, con 3, con 7])
-- i negative, j positive, i REM j = i: -- i negative, j positive, i REM j = i:
,(i_mod_j_mapping, [i === con 3], [i <== con (-1)] &&& leq [(-1)**j ++ con 1, i, con 0] &&& leq [con 0, i, con 7] &&& leq [con 0, con 3, con 7]) ,((0,1),i_mod_j_mapping, [i === con 3], [i <== con (-1)] &&& leq [(-1)**j ++ con 1, i, con 0] &&& leq [con 0, i, con 7] &&& leq [con 0, con 3, con 7])
-- i negative, j positive, i REM j = i + k: -- i negative, j positive, i REM j = i + k:
,(i_mod_j_mapping, [i ++ k === con 3], [i <== con (-1), k >== j] &&& ,((0,1),i_mod_j_mapping, [i ++ k === con 3], [i <== con (-1), k >== j] &&&
leq [(-1)**j ++ con 1, i ++ k, con 0] &&& leq [con 0, i ++ k, con 7] &&& leq [con 0, con 3, con 7]) leq [(-1)**j ++ con 1, i ++ k, con 0] &&& leq [con 0, i ++ k, con 7] &&& leq [con 0, con 3, con 7])
-- i negative, j negative, i REM j = i: -- i negative, j negative, i REM j = i:
,(i_mod_j_mapping, [i === con 3], [i <== con (-1)] &&& leq [j ++ con 1, i, con 0] &&& leq [con 0, i, con 7] &&& leq [con 0, con 3, con 7]) ,((0,1),i_mod_j_mapping, [i === con 3], [i <== con (-1)] &&& leq [j ++ con 1, i, con 0] &&& leq [con 0, i, con 7] &&& leq [con 0, con 3, con 7])
-- i negative, j negative, i REM j = i + k: -- i negative, j negative, i REM j = i + k:
,(i_mod_j_mapping, [i ++ k === con 3], [i <== con (-1), k >== (-1)**j] &&& ,((0,1),i_mod_j_mapping, [i ++ k === con 3], [i <== con (-1), k >== (-1)**j] &&&
leq [j ++ con 1, i ++ k, con 0] &&& leq [con 0, i ++ k, con 7] &&& leq [con 0, con 3, con 7]) leq [j ++ con 1, i ++ k, con 0] &&& leq [con 0, i ++ k, con 7] &&& leq [con 0, con 3, con 7])
], [buildExpr $ Dy (Var "i") A.Rem (Var "j"), intLiteral 3], intLiteral 8) ], [buildExpr $ Dy (Var "i") A.Rem (Var "j"), intLiteral 3], intLiteral 8)
,testRep (200,[(rep_i_mapping, [i === j], ,testRep' (200,[((0,0),rep_i_mapping, [i === j],
ij_16 &&& [i <== j ++ con (-1)] ij_16 &&& [i <== j ++ con (-1)]
&&& leq [con 0, i, con 7] &&& leq [con 0, j, con 7])], &&& leq [con 0, i, con 7] &&& leq [con 0, j, con 7])],
[(variable "i", intLiteral 1, intLiteral 6)],[exprVariable "i"],intLiteral 8) [(variable "i", intLiteral 1, intLiteral 6)],[exprVariable "i"],intLiteral 8)
,testRep (201, ,testRep' (201,
[(rep_i_mapping, [i === j], [((0,0),rep_i_mapping, [i === j],
ij_16 &&& [i <== j ++ con (-1)] ij_16 &&& [i <== j ++ con (-1)]
&&& leq [con 0, i, con 7] &&& leq [con 0, j, con 7])] &&& leq [con 0, i, con 7] &&& leq [con 0, j, con 7])]
++ replicate 2 (rep_i_mapping,[i === con 3], leq [con 1,i, con 6] &&& leq [con 0, i, con 7] &&& leq [con 0, con 3, con 7]) ++ replicate 2 ((0,1),rep_i_mapping,[i === con 3], leq [con 1,i, con 6] &&& leq [con 0, i, con 7] &&& leq [con 0, con 3, con 7])
++ [(rep_i_mapping,[con 3 === con 3],concat $ replicate 2 (leq [con 0, con 3, con 7]))] ++ [((1,1),rep_i_mapping,[con 3 === con 3],concat $ replicate 2 (leq [con 0, con 3, con 7]))]
,[(variable "i", intLiteral 1, intLiteral 6)],[exprVariable "i", intLiteral 3],intLiteral 8) ,[(variable "i", intLiteral 1, intLiteral 6)],[exprVariable "i", intLiteral 3],intLiteral 8)
,testRep (202,[ ,testRep' (202,[
(rep_i_mapping,[i === j ++ con 1],ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, i, con 7] &&& leq [con 0, j ++ con 1, con 7]) ((0,1),rep_i_mapping,[i === j ++ con 1],ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, i, con 7] &&& leq [con 0, j ++ con 1, con 7])
,(rep_i_mapping,[i ++ con 1 === j],ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, i ++ con 1, con 7] &&& leq [con 0, j, con 7]) ,((0,1),rep_i_mapping,[i ++ con 1 === j],ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, i ++ con 1, con 7] &&& leq [con 0, j, con 7])
,(rep_i_mapping,[i === j],ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, i, con 7] &&& leq [con 0, j, con 7]) ,((0,0),rep_i_mapping,[i === j],ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, i, con 7] &&& leq [con 0, j, con 7])
,(rep_i_mapping,[i === j],ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, i ++ con 1, con 7] &&& leq [con 0, j ++ con 1, con 7])] ,((1,1),rep_i_mapping,[i === j],ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, i ++ con 1, con 7] &&& leq [con 0, j ++ con 1, con 7])]
++ [(rep_i_mapping, [i === i ++ con 1], leq [con 1, i, con 6] &&& leq [con 1, i, con 6] &&& -- deliberate repeat ++ [((0,1),rep_i_mapping, [i === i ++ con 1], leq [con 1, i, con 6] &&& leq [con 1, i, con 6] &&& -- deliberate repeat
leq [con 0, i, con 7] &&& leq [con 0,i ++ con 1, con 7])] leq [con 0, i, con 7] &&& leq [con 0,i ++ con 1, con 7])]
,[(variable "i", intLiteral 1, intLiteral 6)],[exprVariable "i", buildExpr $ Dy (Var "i") A.Add (Lit $ intLiteral 1)],intLiteral 8) ,[(variable "i", intLiteral 1, intLiteral 6)],[exprVariable "i", buildExpr $ Dy (Var "i") A.Add (Lit $ intLiteral 1)],intLiteral 8)
-- Only a constant: -- Only a constant:
,testRep (210,[(rep_i_mapping,[con 4 === con 4],concat $ replicate 2 $ leq [con 0, con 4, con 7])] ,testRep' (210,[((0,0),rep_i_mapping,[con 4 === con 4],concat $ replicate 2 $ leq [con 0, con 4, con 7])]
,[(variable "i", intLiteral 1, intLiteral 6)],[intLiteral 4],intLiteral 8) ,[(variable "i", intLiteral 1, intLiteral 6)],[intLiteral 4],intLiteral 8)
] ]
where where
-- These functions assume that you pair each list [x,y,z] as (x,y) (x,z) (y,z) in that order.
-- for more control use the test' and testRep' versions:
test :: (Integer,[(VarMap,[HandyEq],[HandyIneq])],[A.Expression],A.Expression) -> Test test :: (Integer,[(VarMap,[HandyEq],[HandyIneq])],[A.Expression],A.Expression) -> Test
test (ind, problems, exprs, upperBound) = test (ind, problems, exprs, upperBound) = test' (ind, zipWith (\n (vm,eq,ineq) -> (n,vm,eq,ineq)) (labelNums 0 $ length exprs) problems, exprs, upperBound)
TestCase $ assertEquivalentProblems ("testMakeEquations " ++ show ind)
(map (transformPair id (uncurry makeConsistent)) $ map pairLatterTwo problems) =<< (checkRight $ makeEquations (exprs,[]) upperBound) -- The ordering for the original list [0,1,2] should be [(0,1),(0,2),(1,2)]
-- So take each number, pair it with each remaining number in order, then increase
labelNums :: Int -> Int -> [(Int,Int)]
labelNums m n | m >= n = []
| otherwise = [(m,n') | n' <- [(m + 1) .. n]] ++ labelNums (m + 1) n
testRep :: (Integer,[(VarMap,[HandyEq],[HandyIneq])],[(A.Variable, A.Expression, A.Expression)],[A.Expression],A.Expression) -> Test test' :: (Integer,[((Int,Int),VarMap,[HandyEq],[HandyIneq])],[A.Expression],A.Expression) -> Test
testRep (ind, problems, reps, exprs, upperBound) = test' (ind, problems, exprs, upperBound) =
TestCase $ assertEquivalentProblems ("testMakeEquations " ++ show ind) TestCase $ assertEquivalentProblems ("testMakeEquations " ++ show ind) (zip [0..] exprs)
(map (transformPair id (uncurry makeConsistent)) $ map pairLatterTwo problems) (map (transformTriple (applyPair (exprs !!)) id (uncurry makeConsistent)) $ map pairLatterTwo problems) =<< (checkRight $ makeEquations (exprs,[]) upperBound)
testRep' :: (Integer,[((Int, Int), VarMap,[HandyEq],[HandyIneq])],[(A.Variable, A.Expression, A.Expression)],[A.Expression],A.Expression) -> Test
testRep' (ind, problems, reps, exprs, upperBound) =
TestCase $ assertEquivalentProblems ("testMakeEquations " ++ show ind) (zip [0..] exprs)
(map (transformTriple (applyPair (exprs !!)) id (uncurry makeConsistent)) $ map pairLatterTwo problems)
=<< (checkRight $ makeReplicatedEquations reps (exprs,[]) upperBound) =<< (checkRight $ makeReplicatedEquations reps (exprs,[]) upperBound)
pairLatterTwo (a,b,c) = (a,(b,c)) pairLatterTwo (l,a,b,c) = (l,a,(b,c))
joinMapping :: [VarMap] -> ([HandyEq],[HandyIneq]) -> [(VarMap,[HandyEq],[HandyIneq])] joinMapping :: [VarMap] -> ([HandyEq],[HandyIneq]) -> [(VarMap,[HandyEq],[HandyIneq])]
joinMapping vms (eq,ineq) = map (\vm -> (vm,eq,ineq)) vms joinMapping vms (eq,ineq) = map (\vm -> (vm,eq,ineq)) vms
@ -407,8 +420,8 @@ testMakeEquations = TestLabel "testMakeEquations" $ TestList
rr_i_neg = ([], leq [con 0, i ++ 2**j, con 7] &&& [i <== con (-1), j >== con 0] &&& leq [con (-1), i ++ 2**j, con 0]) rr_i_neg = ([], leq [con 0, i ++ 2**j, con 7] &&& [i <== con (-1), j >== con 0] &&& leq [con (-1), i ++ 2**j, con 0])
rr_ip1_neg = ([], leq [con 0, i ++ con 1 ++ 4**k, con 7] &&& [i ++ con 1 <== con (-1), k >== con 0] &&& leq [con (-3), i ++ con 1 ++ 4**k, con 0]) rr_ip1_neg = ([], leq [con 0, i ++ con 1 ++ 4**k, con 7] &&& [i ++ con 1 <== con (-1), k >== con 0] &&& leq [con (-3), i ++ con 1 ++ 4**k, con 0])
combine :: VarMap -> [[([HandyEq],[HandyIneq])]] -> [(VarMap,[HandyEq],[HandyIneq])] combine :: (Int,Int) -> VarMap -> [[([HandyEq],[HandyIneq])]] -> [((Int,Int),VarMap,[HandyEq],[HandyIneq])]
combine vm eq_ineqs = [(vm,e,i) | (e,i) <- map (transformPair concat concat . unzip) eq_ineqs] combine l vm eq_ineqs = [(l,vm,e,i) | (e,i) <- map (transformPair concat concat . unzip) eq_ineqs]
-- Helper functions for the replication: -- Helper functions for the replication:
@ -547,11 +560,36 @@ translateEquations mp = seqPair . transformPair (mapM swapColumns) (mapM swapCol
swapColumns' (x,v) = transformMaybe (\y -> (y,v)) $ transformMaybe fst $ find ((== x) . snd) mp swapColumns' (x,v) = transformMaybe (\y -> (y,v)) $ transformMaybe fst $ find ((== x) . snd) mp
-- | Asserts that the two problems are equivalent, once you take into account the potentially different variable mappings -- | Asserts that the two problems are equivalent, once you take into account the potentially different variable mappings
assertEquivalentProblems :: String -> [(VarMap, (EqualityProblem, InequalityProblem))] -> [(VarMap, (EqualityProblem, InequalityProblem))] -> Assertion assertEquivalentProblems :: String -> [(Int, A.Expression)] -> [((A.Expression, A.Expression), VarMap, (EqualityProblem, InequalityProblem))] ->
assertEquivalentProblems title exp act [((A.Expression, A.Expression), VarMap, (EqualityProblem, InequalityProblem))] -> Assertion
assertEquivalentProblems title indExpr exp act
= ((uncurry $ assertEqualCustomShow (showPairCustom show $ showListCustom $ showMaybe showProblem) title) = ((uncurry $ assertEqualCustomShow (showPairCustom show $ showListCustom $ showMaybe showProblem) title)
$ pairPairs (length exp, length act) $ transformPair sortProblem sortProblem $ unzip $ map (uncurry transform) $ zip exp act) $ pairPairs (length exp, length act) $ transformPair sortProblem sortProblem $ unzip $ map (uncurry transform)
$ map (uncurry checkLabel) $ zip (sortByLabels exp) (sortByLabels act))
where where
-- Since this is a test, I'm taking the lazy way out and allowing run-time errors in this
-- function rather than putting it all in a monad. In HUnit the effect will be about the same
checkLabel :: ((Int, Int), VarMap, (EqualityProblem, InequalityProblem)) ->
((Int, Int), VarMap, (EqualityProblem, InequalityProblem)) ->
((VarMap, (EqualityProblem, InequalityProblem)), (VarMap, (EqualityProblem, InequalityProblem)))
checkLabel (l,vm,p) (l',vm',p')
| l == l' = ((vm,p), (vm',p'))
| otherwise = error $ "Labels did not match, expected: " ++ show l ++ " but actual: " ++ show l'
sortByLabels :: [((A.Expression, A.Expression), VarMap, (EqualityProblem, InequalityProblem))] ->
[((Int, Int), VarMap, (EqualityProblem, InequalityProblem))]
sortByLabels = sortBy (comparing (\(l,_,_) -> l)) . map lookupIndexes
sortPair :: (Int,Int) -> (Int, Int)
sortPair (x,y) | x <= y = (x,y)
| otherwise = (y,x)
lookupIndexes :: ((A.Expression, A.Expression), VarMap, (EqualityProblem, InequalityProblem)) ->
((Int, Int), VarMap, (EqualityProblem, InequalityProblem))
lookupIndexes ((e,e'),vm, p) = (sortPair (lookup e, lookup e'), vm, p)
where
lookup e = maybe (-1) fst $ find ((== e) . snd) indExpr
transform :: (VarMap, (EqualityProblem, InequalityProblem)) -> (VarMap, (EqualityProblem, InequalityProblem)) -> transform :: (VarMap, (EqualityProblem, InequalityProblem)) -> (VarMap, (EqualityProblem, InequalityProblem)) ->
( Maybe (EqualityProblem, InequalityProblem), Maybe (EqualityProblem, InequalityProblem) ) ( Maybe (EqualityProblem, InequalityProblem), Maybe (EqualityProblem, InequalityProblem) )
transform exp act = (translatedExp, Just $ sortP $ snd act) transform exp act = (translatedExp, Just $ sortP $ snd act)