Changed the way replicated variables are handled and altered one of the tests accordingly
This commit is contained in:
parent
01783071a8
commit
fca070e1bc
|
@ -335,15 +335,11 @@ flatten other = throwError ("Unhandleable item found in expression: " ++ show ot
|
||||||
-- last two are in effect identical. Therefore we drop the i' prime
|
-- last two are in effect identical. Therefore we drop the i' prime
|
||||||
-- version, because it has i' but not i. In contrast, the first item
|
-- version, because it has i' but not i. In contrast, the first item
|
||||||
-- (i == i') is retained because it features both i and i'.
|
-- (i == i') is retained because it features both i and i'.
|
||||||
-- 2. For every equation that features both i and i', it adds two possible
|
-- 2. For every equation that features both i and i', it adds
|
||||||
-- versions. One with the inequality "i <= i' - 1", the other with the
|
-- the inequality "i <= i' - 1". Because all possible combinations of
|
||||||
-- inequality "i' <= i - 1". The inequalities make sure that i and i'
|
-- accesses are examined, in the case of [i,i + 1,i', i' + 1], the pairing
|
||||||
-- are distinct. This is important; otherwise [i == i'] would have the
|
-- will produce both "i = i' + 1" and "i + 1 = i'" so there is no need
|
||||||
-- obvious solution. The reason for having both inequalities is that
|
-- to vary the inequality itself.
|
||||||
-- otherwise there could be mistakes. "i == i' + 1" has no solution
|
|
||||||
-- when combined with "i <= i' - 1" (making it look safe), but when
|
|
||||||
-- combined with "i' <= i - 1" there is a solution, correctly identifying
|
|
||||||
-- the accesses as unsafe.
|
|
||||||
squareAndPair ::
|
squareAndPair ::
|
||||||
[(CoeffIndex, CoeffIndex)] ->
|
[(CoeffIndex, CoeffIndex)] ->
|
||||||
VarMap ->
|
VarMap ->
|
||||||
|
@ -351,23 +347,11 @@ squareAndPair ::
|
||||||
(EqualityConstraintEquation, EqualityConstraintEquation) ->
|
(EqualityConstraintEquation, EqualityConstraintEquation) ->
|
||||||
[(VarMap, (EqualityProblem, InequalityProblem))]
|
[(VarMap, (EqualityProblem, InequalityProblem))]
|
||||||
squareAndPair repVars s v lh
|
squareAndPair repVars s v lh
|
||||||
= [(s,squareEquations (eq,ineq ++ ex))
|
= [(s,squareEquations (eq,ineq ++ concat (applyAll (eq,ineq) (map addExtra repVars))))
|
||||||
| (eq,ineq) <- pairEqsAndBounds v lh
|
| (eq,ineq) <- pairEqsAndBounds v lh
|
||||||
,and (map (primeImpliesPlain (eq,ineq)) repVars)
|
,and (map (primeImpliesPlain (eq,ineq)) repVars)
|
||||||
,ex <- if repVars == []
|
|
||||||
-- If this was just the empty list, there be no values for
|
|
||||||
-- "ex" and thus the list comprehension would end up empty.
|
|
||||||
-- The correct value is a list with one empty list; this
|
|
||||||
-- way there is one possible value for "ex", which is blank.
|
|
||||||
-- Then the list comprehension will pan out properly.
|
|
||||||
then [[]]
|
|
||||||
else productLists (applyAll (eq,ineq) (map addExtra repVars))
|
|
||||||
]
|
]
|
||||||
where
|
where
|
||||||
productLists :: [[[a]]] -> [[a]]
|
|
||||||
productLists [] = [[]]
|
|
||||||
productLists (xs:xss) = [x ++ ys | x <- xs, ys <- productLists xss]
|
|
||||||
|
|
||||||
itemPresent :: CoeffIndex -> [Array CoeffIndex Integer] -> Bool
|
itemPresent :: CoeffIndex -> [Array CoeffIndex Integer] -> Bool
|
||||||
itemPresent x = any (\a -> arrayLookupWithDefault 0 a x /= 0)
|
itemPresent x = any (\a -> arrayLookupWithDefault 0 a x /= 0)
|
||||||
|
|
||||||
|
@ -379,17 +363,14 @@ squareAndPair repVars s v lh
|
||||||
-- No prime, therefore fine:
|
-- No prime, therefore fine:
|
||||||
else True
|
else True
|
||||||
|
|
||||||
addExtra :: (CoeffIndex, CoeffIndex) -> (EqualityProblem,InequalityProblem) -> [InequalityProblem]
|
addExtra :: (CoeffIndex, CoeffIndex) -> (EqualityProblem,InequalityProblem) -> InequalityProblem
|
||||||
addExtra (plain,prime) (eq, ineq)
|
addExtra (plain,prime) (eq, ineq)
|
||||||
| itemPresent plain (eq ++ ineq) && itemPresent prime (eq ++ ineq) = bothWays
|
| itemPresent plain (eq ++ ineq) && itemPresent prime (eq ++ ineq) = extraIneq
|
||||||
| otherwise = [[]] -- One item, empty. Note that this is not the empty list (no items), which would cause problems above
|
| otherwise = []
|
||||||
where
|
where
|
||||||
bothWays :: [InequalityProblem]
|
extraIneq :: InequalityProblem
|
||||||
bothWays = map (\elems -> [simpleArray elems])
|
|
||||||
-- prime >= plain + 1 (prime - plain - 1 >= 0)
|
-- prime >= plain + 1 (prime - plain - 1 >= 0)
|
||||||
[[(prime,1), (plain,-1), (0, -1)]
|
extraIneq = [simpleArray [(prime,1), (plain,-1), (0, -1)]]
|
||||||
-- plain >= prime + 1 (plain - prime - 1 >= 0)
|
|
||||||
,[(plain,1), (prime,-1), (0, -1)]]
|
|
||||||
|
|
||||||
-- | Odd helper function for getting/asserting the first item of a triple from a singleton list inside a monad transformer (!)
|
-- | Odd helper function for getting/asserting the first item of a triple from a singleton list inside a monad transformer (!)
|
||||||
getSingleItem :: MonadTrans m => String -> [(a,b,c)] -> m (Either String) a
|
getSingleItem :: MonadTrans m => String -> [(a,b,c)] -> m (Either String) a
|
||||||
|
|
|
@ -330,9 +330,9 @@ testMakeEquations = TestList
|
||||||
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,both_rep_i ([i === j],
|
,testRep (200,[(rep_i_mapping, [i === j],
|
||||||
leq [con 1, i, con 6] &&& leq [con 1, j, con 6] &&& [i <== j ++ con (-1)]
|
leq [con 1, i, con 6] &&& leq [con 1, j, con 6] &&& [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,[(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])]
|
,testRep (201,[(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])]
|
||||||
|
|
Loading…
Reference in New Issue
Block a user