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

Added some tests for the Omega Test that are not "easily" solved

Browse Source
This commit is contained in:
Neil Brown 2007-12-14 12:25:29 +00:00
parent 97c670b2ff
commit 1dabdfef9d
1 changed files with 28 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
transformations/RainUsageCheckTest.hs
View File

@ -361,7 +361,16 @@ testIndexes = TestList
--should fail:
,notSolveable (2, [i === con 7],[i <== con 5])
,easilySolved (3, [i ++ con 1 === j], i_j_constraint 0 10)
-- Can i = j?
,notSolveable (3, [i === j], i_j_constraint 0 9)
-- TODO need to run the below exampls on a better test (they are not "easily" solved):
-- Can (j + 1 % 10 == i + 1 % 10)?
,notSolveable $ withKIsMod (i ++ con 1) 10 $ withNIsMod (j ++ con 1) 10 $ (4, [k === n], i_j_constraint 0 9)
-- Off by one (i + 1 % 9)
,easilySolved $ withKIsMod (i ++ con 1) 9 $ withNIsMod (j ++ con 1) 9 $ (5, [k === n], i_j_constraint 0 9)
,safeParTest 100 True (0,10) [i]
,safeParTest 120 False (0,10) [i,i ++ con 1]
@ -449,12 +458,27 @@ testIndexes = TestList
n ** var = map (transformPair id (* n)) var
con :: Integer -> [(Int,Integer)]
con c = [(0,c)]
i :: [(Int, Integer)]
i,j,k,m,n,p :: [(Int, Integer)]
i = [(1,1)]
j :: [(Int, Integer)]
j = [(2,1)]
k :: [(Int, Integer)]
k = [(3,1)]
m = [(4,1)]
n = [(5,1)]
p = [(6,1)]
isMod :: [(Int,Integer)] -> [(Int,Integer)] -> Integer -> ([HandyEq], [HandyIneq])
isMod var@[(ind,1)] alpha divisor = ([alpha_minus_div_sigma === var], leq [con 0, alpha_minus_div_sigma, con $ divisor - 1])
where
alpha_minus_div_sigma = alpha ++ (negate divisor) ** sigma
sigma = [(ind+1,1)]
-- | Adds both k and m to the equation!
withKIsMod :: [(Int,Integer)] -> Integer -> (Int, [HandyEq], [HandyIneq]) -> (Int, [HandyEq], [HandyIneq])
withKIsMod alpha divisor (ind,eq,ineq) = let (eq',ineq') = isMod k alpha divisor in (ind,eq ++ eq',ineq ++ ineq')
-- | Adds both n and p to the equation!
withNIsMod :: [(Int,Integer)] -> Integer -> (Int, [HandyEq], [HandyIneq]) -> (Int, [HandyEq], [HandyIneq])
withNIsMod alpha divisor (ind,eq,ineq) = let (eq',ineq') = isMod n alpha divisor in (ind,eq ++ eq',ineq ++ ineq')
makeConsistent :: [HandyEq] -> [HandyIneq] -> (EqualityProblem, InequalityProblem)
makeConsistent eqs ineqs = (map ensure eqs', map ensure ineqs')