ddbec737f2
For some reason, the usage check tests are now very slow to run (perhaps because of all the operator definitions added to each one?), which needs further investigation.
1205 lines
62 KiB
Haskell
1205 lines
62 KiB
Haskell
{-
|
|
Tock: a compiler for parallel languages
|
|
Copyright (C) 2007 University of Kent
|
|
|
|
This program is free software; you can redistribute it and/or modify it
|
|
under the terms of the GNU General Public License as published by the
|
|
Free Software Foundation, either version 2 of the License, or (at your
|
|
option) any later version.
|
|
|
|
This program is distributed in the hope that it will be useful, but
|
|
WITHOUT ANY WARRANTY; without even the implied warranty of
|
|
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU
|
|
General Public License for more details.
|
|
|
|
You should have received a copy of the GNU General Public License along
|
|
with this program. If not, see <http://www.gnu.org/licenses/>.
|
|
-}
|
|
|
|
module ArrayUsageCheckTest (vioqcTests) where
|
|
|
|
import Control.Monad.Identity
|
|
import Control.Monad.Reader
|
|
import Control.Monad.State
|
|
import Control.Monad.Writer (tell)
|
|
import Data.Array.IArray
|
|
import Data.List
|
|
import qualified Data.Map as Map
|
|
import Data.Maybe
|
|
import Data.Ord
|
|
import qualified Data.Set as Set
|
|
import Prelude hiding ((**),fail)
|
|
import Test.HUnit
|
|
import Test.QuickCheck hiding (check)
|
|
|
|
|
|
import ArrayUsageCheck
|
|
import qualified AST as A
|
|
import CompState
|
|
import Metadata
|
|
import Omega
|
|
import ShowCode
|
|
import TestFramework
|
|
import TestHarness
|
|
import TestUtils
|
|
import Types
|
|
import UsageCheckUtils hiding (Var)
|
|
import qualified UsageCheckUtils
|
|
import Utils
|
|
|
|
instance Show FlattenedExp where
|
|
show fexp = runIdentity $ showFlattenedExp (return . showOccam) fexp
|
|
|
|
testCompState :: CompState
|
|
testCompState = emptyState
|
|
rr :: ReaderT CompState m a -> m a
|
|
rr = flip runReaderT testCompState
|
|
|
|
testArrayCheck :: Test
|
|
testArrayCheck = TestList
|
|
[
|
|
-- x_1 = 0
|
|
pass (0, [], [[0,1]], [])
|
|
-- x_1 = 0, 3x_1 >= 0 --> 0 >= 0
|
|
,pass (1, [[0,0]], [[0,1]], [[0,3]])
|
|
-- -7 + x_1 = 0
|
|
,pass (2, [], [[-7,1]], [])
|
|
-- x_1 = 9, 3 + 2x_1 >= 0 --> 21 >= 0
|
|
,pass (3, [[21,0]], [[-9,1]], [[3,2]])
|
|
-- x_1 + x_2 = 0, 4x_1 = 8, 2x_2 = -4
|
|
,pass (4, [], [[0,1,1], [-8,4,0], [4,0,2]], [])
|
|
-- - x_1 + x_2 = 0, 4x_1 = 8, 2x_2 = 4
|
|
,pass (5, [], [[0,-1,1], [-8,4,0], [-4,0,2]], [])
|
|
-- -x_1 = -9, 3 + 2x_1 >= 0 --> 21 >= 0
|
|
,pass (6, [[21,0]], [[9,-1]], [[3,2]])
|
|
|
|
|
|
-- From the Omega Test paper (x = x_1, y = x_2, z = x_3, sigma = x_1 (effectively)):
|
|
,pass (100, [[11,13,0,0], [28,-13,0,0], [47,-5,0,0], [53,5,0,0]], [[-17,7,12,31], [-7,3,5,14]],
|
|
[[-1,1,0,0], [40,-1,0,0], [50,0,1,0], [50,0,-1,0]])
|
|
|
|
-- Impossible/inconsistent equality constraints:
|
|
|
|
-- -7 = 0
|
|
,TestCase $ assertEqual "testArrayCheck 1002" (Nothing) (solveConstraints' [simpleArray [(0,7),(1,0)]] [])
|
|
-- x_1 = 3, x_1 = 4
|
|
,TestCase $ assertEqual "testArrayCheck 1003" (Nothing) (solveConstraints' [simpleArray [(0,-3),(1,1)], simpleArray [(0,-4),(1,1)]] [])
|
|
-- x_1 + x_2 = 0, x_1 + x_2 = -3
|
|
,TestCase $ assertEqual "testArrayCheck 1004" (Nothing) (solveConstraints' [simpleArray [(0,0),(1,1),(2,1)], simpleArray [(0,3),(1,1),(2,1)]] [])
|
|
-- 4x_1 = 7
|
|
,TestCase $ assertEqual "testArrayCheck 1005" (Nothing) (solveConstraints' [simpleArray [(0,-7),(1,4)]] [])
|
|
]
|
|
where
|
|
solveConstraints' = solveConstraints undefined
|
|
|
|
pass :: (Int, [[Integer]], [[Integer]], [[Integer]]) -> Test
|
|
pass (ind, expIneq, inpEq, inpIneq) = TestCase $ assertEqual ("testArrayCheck " ++ show ind)
|
|
(Just $ map arrayise expIneq) (transformMaybe snd $ solveConstraints' (map arrayise inpEq) (map arrayise inpIneq))
|
|
|
|
arrayise :: [Integer] -> Array Int Integer
|
|
arrayise = simpleArray . zip [0..]
|
|
|
|
-- Various helpers for easily creating equations.
|
|
-- Rules for writing equations:
|
|
-- * You must use the variables i, j, k in that order as you need them.
|
|
-- Never write an equation just involving i and k, or j and k. Always
|
|
-- use (i), (i and j), or (i and j and k).
|
|
-- * Constant scaling must always be on the left, and does not need the con
|
|
-- function. con 1 ** i won't compile.
|
|
|
|
-- Useful to make sure the equation types are not mixed up:
|
|
newtype HandyEq = Eq [(Int, Integer)] deriving (Show, Eq)
|
|
newtype HandyIneq = Ineq [(Int, Integer)] deriving (Show, Eq)
|
|
|
|
-- | The constraint for an arbitrary i,j that exist between low and high (inclusive)
|
|
-- and where i and j are distinct and i is taken to be the lower index.
|
|
i_j_constraint :: Integer -> Integer -> [HandyIneq]
|
|
i_j_constraint low high = [con low <== i, i ++ con 1 <== j, j <== con high]
|
|
|
|
-- The easy way of writing equations is built on the following Haskell magic.
|
|
-- Essentially, everything is a list of (index, coefficient). You can scale
|
|
-- with the ** operator, and you can form equalities and inequalities with
|
|
-- the ===, <== and >== operators. The type system saves you from doing anything
|
|
-- nonsensical. The other neat thing is that + is ++. An &&& operator is defined
|
|
-- for combining inequality lists.
|
|
|
|
leq :: [[(Int,Integer)]] -> [HandyIneq]
|
|
leq [] = []
|
|
leq [_] = []
|
|
leq (x:y:zs) = (x <== y) : (leq (y:zs))
|
|
|
|
(&&&) :: [a] -> [a] -> [a]
|
|
(&&&) = (++)
|
|
|
|
infixr 4 ===
|
|
infixr 4 <==
|
|
infixr 4 >==
|
|
infix 6 **
|
|
|
|
(===) :: [(Int,Integer)] -> [(Int,Integer)] -> HandyEq
|
|
lhs === rhs = Eq $ lhs ++ negateVars rhs
|
|
(<==) :: [(Int,Integer)] -> [(Int,Integer)] -> HandyIneq
|
|
lhs <== rhs = Ineq $ negateVars lhs ++ rhs
|
|
(>==) :: [(Int,Integer)] -> [(Int,Integer)] -> HandyIneq
|
|
lhs >== rhs = Ineq $ lhs ++ negateVars rhs
|
|
negateVars :: [(Int,Integer)] -> [(Int,Integer)]
|
|
negateVars = map (transformPair id negate)
|
|
(**) :: Integer -> [(Int,Integer)] -> [(Int,Integer)]
|
|
n ** var = map (transformPair id (* n)) var
|
|
con :: Integer -> [(Int,Integer)]
|
|
con c = [(0,c)]
|
|
i,j,k,m,n,p :: [(Int, Integer)]
|
|
i = [(1,1)]
|
|
j = [(2,1)]
|
|
k = [(3,1)]
|
|
m = [(4,1)]
|
|
n = [(5,1)]
|
|
p = [(6,1)]
|
|
|
|
-- Turns a list like [(i,3),(j,4)] into proper answers
|
|
answers :: [([(Int, Integer)],Integer)] -> Map.Map CoeffIndex Integer
|
|
answers = Map.fromList . map (transformPair (fst . head) id)
|
|
|
|
-- Shows the answers in terms of the test variables
|
|
showTestAnswers :: VariableMapping -> String
|
|
showTestAnswers (VariableMapping vm) = concat $ intersperse "\n" $ map showAnswer $ Map.assocs vm
|
|
where
|
|
showAnswer :: (CoeffIndex,Either a EqualityConstraintEquation) -> String
|
|
showAnswer (x,eq) = mylookup x ++ " = " ++ either (const "") showItems eq
|
|
|
|
showItems :: EqualityConstraintEquation -> String
|
|
showItems eq = concat (intersperse " + " (filter (not . null) $ map showItem (assocs eq)))
|
|
|
|
showItem :: (CoeffIndex,Integer) -> String
|
|
showItem (k,a_k) | a_k == 0 = ""
|
|
| k == 0 = show a_k
|
|
| a_k == 1 = mylookup k
|
|
| otherwise = show a_k ++ mylookup k
|
|
|
|
mylookup :: CoeffIndex -> String
|
|
mylookup x = Map.findWithDefault "unknown" x lookupTable
|
|
|
|
lookupTable :: Map.Map CoeffIndex String
|
|
lookupTable = Map.fromList $ zip [1..] ["i","j","k","m","n","p"]
|
|
++ [ (n,"y_" ++ show n) | n <- [7..100]] -- needed for showing QuickCheck failures
|
|
|
|
showInequality :: InequalityConstraintEquation -> String
|
|
showInequality ineq = "0 <= " ++ zeroIfBlank (showItems ineq)
|
|
|
|
showInequalities :: InequalityProblem -> String
|
|
showInequalities ineqs = concat $ intersperse "\n" $ map showInequality ineqs
|
|
|
|
showEquality :: InequalityConstraintEquation -> String
|
|
showEquality eq = "0 = " ++ zeroIfBlank (showItems eq)
|
|
|
|
showEqualities :: InequalityProblem -> String
|
|
showEqualities eqs = concat $ intersperse "\n" $ map showEquality eqs
|
|
|
|
zeroIfBlank :: String -> String
|
|
zeroIfBlank s | null s = "0"
|
|
| otherwise = s
|
|
|
|
showProblem :: (EqualityProblem,InequalityProblem) -> String
|
|
showProblem (eqs,ineqs) = showEqualities eqs ++ "\n" ++ showInequalities ineqs
|
|
|
|
makeConsistent :: [HandyEq] -> [HandyIneq] -> (EqualityProblem, InequalityProblem)
|
|
makeConsistent eqs ineqs = (map ensure eqs', map ensure ineqs')
|
|
where
|
|
eqs' = map (\(Eq e) -> e) eqs
|
|
ineqs' = map (\(Ineq e) -> e) ineqs
|
|
|
|
ensure :: [(CoeffIndex, Integer)] -> EqualityConstraintEquation
|
|
ensure = accumArray (+) 0 (0, largestIndex)
|
|
largestIndex = maximum $ map (maximum . map fst) $ [[(0,0)]] ++ eqs' ++ ineqs'
|
|
|
|
|
|
-- | Returns Nothing if there is definitely no solution, or (Just ineq) if
|
|
-- further investigation is needed
|
|
|
|
|
|
solveAndPrune' :: VariableMapping -> EqualityProblem -> InequalityProblem -> Maybe (VariableMapping,InequalityProblem)
|
|
solveAndPrune' vm [] ineq = return (vm,ineq)
|
|
solveAndPrune' vm eq ineq = solveConstraints vm eq ineq >>= (seqPair . transformPair return pruneIneq) >>= (\(x,(y,z)) -> solveAndPrune' x y z)
|
|
|
|
solveAndPrune :: EqualityProblem -> InequalityProblem -> Maybe (VariableMapping,InequalityProblem)
|
|
solveAndPrune eq ineq = solveAndPrune' (defaultMapping maxVar) eq ineq
|
|
where
|
|
maxVar = if null eq && null ineq then 0 else
|
|
if null eq then snd $ bounds $ head ineq else snd $ bounds $ head eq
|
|
|
|
|
|
-- | A problem's "solveability"; essentially how much of the Omega Test do you have to
|
|
-- run before the result is known, and which result is it
|
|
data Solveability =
|
|
SolveEq (Map.Map CoeffIndex Integer)
|
|
-- ^ Solveable just by solving equalities and pruning.
|
|
-- In other words, solveAndPrune will give (Just [])
|
|
| ImpossibleEq -- ^ Definitely not solveable just from the equalities.
|
|
-- In other words, solveAndPrune will give Nothing
|
|
| SolveIneq -- ^ Reduceable to inequalities, where the inequalities (therefore) have a solution.
|
|
-- In other words, solveAndPrune will give (Just a) (a /= []),
|
|
-- and then feeding a through fmElimination will give back an inequality set
|
|
-- that can be fed into <SOME FUNCTION TODO> to give a possible solution
|
|
| ImpossibleIneq -- ^ The inequalities are impossible to solve.
|
|
-- In other words, solveAndPrune will give (Just a) (a /= []),
|
|
-- but feeding this through fmElimination will give Nothing.
|
|
-- TODO do we need an option where one variable is left in the inequalities?
|
|
deriving (Eq,Show)
|
|
|
|
check :: Solveability -> (Int,[HandyEq], [HandyIneq]) -> Test
|
|
check s (ind, eq, ineq) =
|
|
case s of
|
|
ImpossibleEq -> TestCase $ assertEqual testName Nothing sapped
|
|
SolveEq {} -> TestCase $ return ()
|
|
{- SolveEq ans -> TestCase $ assertEqual testName (Just (VariableMapping $ fmap Right ans,[]))
|
|
(transformMaybe (transformPair getCounterEqs (either
|
|
(const 0) id)) sapped) -}
|
|
ImpossibleIneq -> TestCase $ assertEqual testName Nothing elimed
|
|
SolveIneq -> TestCase $ assertBool testName (isJust elimed) -- TODO check for a solution to the inequality
|
|
where problem = makeConsistent eq ineq
|
|
sapped = uncurry solveAndPrune problem
|
|
elimed = uncurry solveProblem problem
|
|
testName = "check " ++ show s ++ " " ++ show ind
|
|
++ "(VM after pruning was: " ++ showMaybe showTestAnswers (transformMaybe fst sapped) ++
|
|
", ineqs: " ++ showMaybe showInequalities (transformMaybe snd sapped) ++ ")"
|
|
|
|
testMakeEquations :: Test
|
|
testMakeEquations = TestLabel "testMakeEquations" $ TestList
|
|
[
|
|
test (0,[(Map.empty,[con 0 === con 1],leq [con 0,con 1,con 7] &&& leq [con 0,con 2,con 7])],
|
|
[intLiteral 1, intLiteral 2],intLiteral 8)
|
|
|
|
,test (1,[(i_mapping,[i === con 3],leq [con 0,con 3,con 7] &&& leq [con 0,i,con 7])],
|
|
[exprVariable "i",intLiteral 3],intLiteral 8)
|
|
|
|
,test (2,[(ij_mapping,[i === j],leq [con 0,i,con 7] &&& leq [con 0,j,con 7])],
|
|
[exprVariable "i",exprVariable "j"],intLiteral 8)
|
|
|
|
,test (3,[(ij_mapping,[i ++ con 3 === j],leq [con 0,i ++ con 3,con 7] &&& leq [con 0,j,con 7])],
|
|
[buildExpr $ Dy (Var "i") "+" (Lit $ intLiteral 3),exprVariable "j"],intLiteral 8)
|
|
|
|
,test (4,[(ij_mapping,[2 ** i === j],leq [con 0,2 ** i,con 7] &&& leq [con 0,j,con 7])],
|
|
[buildExpr $ Dy (Var "i") "*" (Lit $ intLiteral 2),exprVariable "j"],intLiteral 8)
|
|
|
|
,test' (5, [(((0,[]),(1,[])), ijk_mapping, [j === k], leq [con 0, j, i ++ con (-1)] &&& leq [con 0, k, i ++ con (-1)])],
|
|
[exprVariable "j", exprVariable "k"], exprVariable "i")
|
|
|
|
-- Testing (i REM 3) vs (4)
|
|
,test' (10,[
|
|
(( (0,[XZero]), (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])
|
|
,(( (0,[XPos]), (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])
|
|
,(( (0,[XNeg]), (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") "\\" (Lit $ intLiteral 3),intLiteral 4],intLiteral 8)
|
|
|
|
-- Testing ((3*i - 2*j REM 11) - 5) vs (i + j)
|
|
-- Expressed as ((2 * (i - j)) + i) REM 11 - 5, and i + j
|
|
,test' (11,[
|
|
(( (0,[XZero]), (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])
|
|
,(( (0,[XPos]), (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]
|
|
&&& [3**i ++ (-2)**j >== con 1] &&& [k <== con 0] &&& leq [con 0, 3**i ++ (-2)**j ++ 11 ** k, con 10])
|
|
,(( (0,[XNeg]), (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]
|
|
&&& [3**i ++ (-2)**j <== con (-1)] &&& [k >== con 0] &&& leq [con (-10), 3**i ++ (-2)**j ++ 11 ** k, con 0])
|
|
],[buildExpr $
|
|
Dy (Dy (Dy (Dy (Lit $ intLiteral 2)
|
|
"*" (Dy (Var "i") "-" (Var "j"))
|
|
)
|
|
"+" (Var "i")
|
|
)
|
|
"\\" (Lit $ intLiteral 11)
|
|
)
|
|
"-" (Lit $ intLiteral 5)
|
|
,buildExpr $ Dy (Var "i") "+" (Var "j")],intLiteral 8)
|
|
|
|
-- Testing i REM 2 vs (i + 1) REM 4
|
|
,test' (12,combine (0,1) (i_ip1_mod_mapping 2 4)
|
|
[ ([XZero],[XZero],[([con 0 === con 0],[]),rr_i_zero, rr_ip1_zero])
|
|
,([XZero],[XPos],[([con 0 === i ++ con 1 ++ 4**k],[]),rr_i_zero,rr_ip1_pos])
|
|
,([XZero],[XNeg],[([con 0 === i ++ con 1 ++ 4**k],[]),rr_i_zero,rr_ip1_neg])
|
|
,([XPos],[XZero],[([i ++ 2**j === con 0],[]),rr_i_pos,rr_ip1_zero])
|
|
,([XPos],[XPos],[([i ++ 2**j === i ++ con 1 ++ 4**k],[]),rr_i_pos,rr_ip1_pos])
|
|
,([XPos],[XNeg],[([i ++ 2**j === i ++ con 1 ++ 4**k],[]),rr_i_pos,rr_ip1_neg])
|
|
,([XNeg],[XZero],[([i ++ 2**j === con 0],[]),rr_i_neg,rr_ip1_zero])
|
|
,([XNeg],[XPos],[([i ++ 2**j === i ++ con 1 ++ 4**k],[]),rr_i_neg,rr_ip1_pos])
|
|
,([XNeg],[XNeg],[([i ++ 2**j === i ++ con 1 ++ 4**k],[]),rr_i_neg,rr_ip1_neg])
|
|
], [buildExpr $ Dy (Var "i") "\\" (Lit $ intLiteral 2)
|
|
,buildExpr $ Dy (Dy (Var "i") "+" (Lit $ intLiteral 1)) "\\" (Lit $ intLiteral 4)
|
|
], intLiteral 8)
|
|
|
|
-- Testing i REM j vs 3
|
|
,test' (100,[
|
|
-- i = 0:
|
|
(((0,[XZero]),(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:
|
|
,(((0,[XPosYPosAZero]),(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:
|
|
,(((0,[XPosYPosANonZero]),(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])
|
|
-- i positive, j negative, i REM j = i:
|
|
,(((0,[XPosYNegAZero]),(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:
|
|
,(((0,[XPosYNegANonZero]),(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])
|
|
|
|
-- i negative, j positive, i REM j = i:
|
|
,(((0,[XNegYPosAZero]),(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:
|
|
,(((0,[XNegYPosANonZero]),(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])
|
|
-- i negative, j negative, i REM j = i:
|
|
,(((0,[XNegYNegAZero]),(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:
|
|
,(((0,[XNegYNegANonZero]),(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])
|
|
], [buildExpr $ Dy (Var "i") "\\" (Var "j"), intLiteral 3], intLiteral 8)
|
|
|
|
|
|
-- i vs. i'
|
|
,testRep' (199,[(((0,[]),(0,[])),rep_i_mapping, [i === j],
|
|
leq [con 3, i, con 4] &&& leq [con 3, j, con 4] &&& [i <== j ++ con (-1)]
|
|
&&& leq [con 0, i, con 7] &&& leq [con 0, j, con 7])],
|
|
("i", intLiteral 3, intLiteral 2),[exprVariable "i"],intLiteral 8)
|
|
|
|
-- i vs. i'
|
|
,testRep' (200,[(((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])],
|
|
("i", intLiteral 1, intLiteral 6),[exprVariable "i"],intLiteral 8)
|
|
|
|
-- i vs i' vs 3
|
|
,let common = ij_16 &&& [i <== j ++ con (-1)] in testRep' (201,
|
|
[(((0,[]),(0,[])),rep_i_mapping, [i === j],
|
|
common &&& leq [con 0, i, con 7] &&& leq [con 0, j, con 7])]
|
|
++ replicate 2 (((0,[]),(1,[])),rep_i_mapping,[i === con 3], common
|
|
&&& leq [con 0, i, con 7] &&& leq [con 0, con 3, con 7])
|
|
++ [(((1,[]),(1,[])),rep_i_mapping,[con 3 === con 3],common &&& (concat $ replicate 2 (leq [con 0, con 3, con 7])))]
|
|
,("i", intLiteral 1, intLiteral 6),[exprVariable "i", intLiteral 3],intLiteral 8)
|
|
|
|
-- i vs i + 1 vs i' vs i' + 1
|
|
,let common = ij_16 &&& [i <== j ++ con (-1)] in testRep' (202,[
|
|
(((0,[]),(1,[])),rep_i_mapping,[i === j ++ con 1],common &&& leq [con 0, i, con 7] &&& leq [con 0, j ++ con 1, con 7])
|
|
,(((0,[]),(1,[])),rep_i_mapping,[i ++ con 1 === j],common &&& leq [con 0, i ++ con 1, con 7] &&& leq [con 0, j, con 7])
|
|
,(((0,[]),(0,[])),rep_i_mapping,[i === j],common &&& leq [con 0, i, con 7] &&& leq [con 0, j, con 7])
|
|
,(((1,[]),(1,[])),rep_i_mapping,[i === j],common &&& leq [con 0, i ++ con 1, con 7] &&& leq [con 0, j ++ con 1, con 7])]
|
|
++ [(((0,[]),(1,[])),rep_i_mapping, [i === i ++ con 1], common &&&
|
|
leq [con 0, i, con 7] &&& leq [con 0,i ++ con 1, con 7])]
|
|
,("i", intLiteral 1, intLiteral 6),[exprVariable "i", buildExpr $ Dy (Var "i") "+" (Lit $ intLiteral 1)],intLiteral 8)
|
|
|
|
-- Only a constant:
|
|
,testRep' (210,[(((0,[]),(0,[])),rep_i_mapping,[con 4 === con 4],ij_16 &&& [i <== j ++ con (-1)] &&& (concat $ replicate 2 $ leq [con 0, con 4, con 7]))]
|
|
,("i", intLiteral 1, intLiteral 6),[intLiteral 4],intLiteral 8)
|
|
|
|
|
|
-- i REM 3 vs i' REM 3
|
|
,testRep' (220,[
|
|
-- i REM 3 == 0 and i' REM 3 == 0
|
|
(((0,[XZero]),(0,[XZero])), rep_i_mod_mapping 3, [con 0 === con 0, i === con 0, j === con 0], ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, con 0, con 7] &&& leq [con 0, con 0, con 7])
|
|
-- i REM 3 == 0 and i' >= 1
|
|
,(((0,[XZero]),(0,[XPos])), rep_i_mod_mapping 3, [con 0 === j ++ 3**m, i === con 0], ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, con 0, con 7]
|
|
&&& leq [con 0, j ++ 3**m, con 7] &&& [m <== con 0, j >== con 1] &&& leq [con 0, j ++ 3**m, con 2])
|
|
-- i REM 3 == 0 and i' <= -1
|
|
,(((0,[XZero]),(0,[XNeg])), rep_i_mod_mapping 3, [con 0 === j ++ 3**m, i === con 0], ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, con 0, con 7]
|
|
&&& leq [con 0, j ++ 3**m, con 7] &&& [m >== con 0, j <== con (-1)] &&& leq [con (-2), j ++ 3**m, con 0])
|
|
-- i >= 1 and i' REM 3 == 0
|
|
,(((0,[XPos]),(0,[XZero])), rep_i_mod_mapping 3, [i ++ 3**k === con 0, j === con 0], ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, con 0, con 7]
|
|
&&& leq [con 0, i ++ 3**k, con 7] &&& [k <== con 0, i >== con 1] &&& leq [con 0, i ++ 3**k, con 2])
|
|
-- i >= 1 and i' >= 1
|
|
,(((0,[XPos]),(0,[XPos])), rep_i_mod_mapping 3, [i ++ 3**k === j ++ 3**m], ij_16 &&& [i <== j ++ con (-1)]
|
|
&&& leq [con 0, i ++ 3**k, con 7] &&& leq [con 0, j ++ 3**m, con 7]
|
|
&&& [m <== con 0, k <== con 0, i >== con 1, j >== con 1]
|
|
&&& leq [con 0, i ++ 3**k, con 2] &&& leq [con 0, j ++ 3**m, con 2])
|
|
-- i >= 1 and i' <= -1
|
|
,(((0,[XPos]),(0,[XNeg])), rep_i_mod_mapping 3, [i ++ 3**k === j ++ 3**m], ij_16 &&& [i <== j ++ con (-1)]
|
|
&&& leq [con 0, i ++ 3**k, con 7] &&& leq [con 0, j ++ 3**m, con 7]
|
|
&&& [m >== con 0, k <== con 0, i >== con 1, j <== con (-1)]
|
|
&&& leq [con 0, i ++ 3**k, con 2] &&& leq [con (-2), j ++ 3**m, con 0])
|
|
-- i <= -1 and i' REM 3 == 0
|
|
,(((0,[XNeg]),(0,[XZero])), rep_i_mod_mapping 3, [i ++ 3**k === con 0, j === con 0], ij_16 &&& [i <== j ++ con (-1)] &&& leq [con 0, con 0, con 7]
|
|
&&& leq [con 0, i ++ 3**k, con 7] &&& [k >== con 0, i <== con (-1)] &&& leq [con (-2), i ++ 3**k, con 0])
|
|
-- i <= - 1 and i' >= 1
|
|
,(((0,[XNeg]),(0,[XPos])), rep_i_mod_mapping 3, [i ++ 3**k === j ++ 3**m], ij_16 &&& [i <== j ++ con (-1)]
|
|
&&& leq [con 0, i ++ 3**k, con 7] &&& leq [con 0, j ++ 3**m, con 7]
|
|
&&& [m <== con 0, k >== con 0, i <== con (-1), j >== con 1]
|
|
&&& leq [con (-2), i ++ 3**k, con 0] &&& leq [con 0, j ++ 3**m, con 2])
|
|
-- i <= - 1 and i' <= -1
|
|
,(((0,[XNeg]),(0,[XNeg])), rep_i_mod_mapping 3, [i ++ 3**k === j ++ 3**m], ij_16 &&& [i <== j ++ con (-1)]
|
|
&&& leq [con 0, i ++ 3**k, con 7] &&& leq [con 0, j ++ 3**m, con 7]
|
|
&&& [m >== con 0, k >== con 0, i <== con (-1), j <== con (-1)]
|
|
&&& leq [con (-2), i ++ 3**k, con 0] &&& leq [con (-2), j ++ 3**m, con 0])
|
|
],("i", intLiteral 1, intLiteral 6),[buildExpr $ Dy (Var "i") "\\" (Lit $ intLiteral 3)], intLiteral 8)
|
|
|
|
|
|
-- TODO test reads and writes are paired properly
|
|
|
|
-- TODO test background knowledge being used
|
|
]
|
|
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 (ind, problems, exprs, upperBound) = test' (ind, zipWith (\n (vm,eq,ineq) -> (n,vm,eq,ineq)) (labelNums 0 $ length exprs) problems, 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,[a]),(Int,[a]))]
|
|
labelNums m n | m >= n = []
|
|
| otherwise = [((m,[]),(n',[])) | n' <- [(m + 1) .. n]] ++ labelNums (m + 1) n
|
|
|
|
|
|
makeParItems :: BK -> [A.Expression] -> ParItems (BK, [A.Expression],[A.Expression])
|
|
makeParItems bk es = ParItems $ map (\e -> SeqItems [(bk,[e],[])]) es
|
|
|
|
lookup :: [A.Expression] -> (Int, a) -> (A.Expression, a)
|
|
lookup es (n,b) = (es !! n, b)
|
|
|
|
test' :: (Integer,[(((Int, [ModuloCase]),(Int,[ModuloCase])),VarMap,[HandyEq],[HandyIneq])],[A.Expression],A.Expression) -> Test
|
|
test' (ind, problems, exprs, upperBound) =
|
|
TestCase $ assertEquivalentProblems ("testMakeEquations " ++ show ind)
|
|
(map (\((a0,a1),b,c,d) -> ((lookup exprs a0, lookup exprs a1), b, makeConsistent c d)) problems)
|
|
=<< (checkRight $ rr $ makeEquations (makeParItems [] exprs) upperBound)
|
|
|
|
testRep' :: (Integer,[(((Int,[ModuloCase]), (Int,[ModuloCase])), VarMap,[HandyEq],[HandyIneq])],(String, A.Expression, A.Expression),[A.Expression],A.Expression) -> Test
|
|
testRep' (ind, problems, (repName, repFrom, repFor), exprs, upperBound) =
|
|
TestCase $ assertEquivalentProblems ("testMakeEquations " ++ show ind)
|
|
(map (\((a0,a1),b,c,d) -> ((lookup exprs a0, lookup exprs a1), b, makeConsistent c d)) problems)
|
|
=<< (checkRight $ rr $ makeEquations (RepParItem (simpleName "i", A.For emptyMeta repFrom repFor (makeConstant emptyMeta 1)) $
|
|
makeParItems [Map.fromList [(UsageCheckUtils.Var $ variable "i",
|
|
[RepBoundsIncl (variable "i") repFrom (subOneInt $ addExprsInt repFrom repFor)])]] exprs) upperBound)
|
|
|
|
pairLatterTwo (l,a,b,c) = (l,a,(b,c))
|
|
|
|
joinMapping :: [VarMap] -> ([HandyEq],[HandyIneq]) -> [(VarMap,[HandyEq],[HandyIneq])]
|
|
joinMapping vms (eq,ineq) = map (\vm -> (vm,eq,ineq)) vms
|
|
|
|
i_mapping :: VarMap
|
|
i_mapping = Map.singleton (Scale 1 $ (exprVariable "i",0)) 1
|
|
ij_mapping :: VarMap
|
|
ij_mapping = Map.fromList [(Scale 1 $ (exprVariable "i",0),1),(Scale 1 $ (exprVariable "j",0),2)]
|
|
ijk_mapping :: VarMap
|
|
ijk_mapping = Map.fromList [(Scale 1 $ (exprVariable "i",0),1),(Scale 1 $ (exprVariable "j",0),2),(Scale 1 $ (exprVariable "k",0),3)]
|
|
i_mod_mapping :: Integer -> VarMap
|
|
i_mod_mapping n = Map.fromList [(Scale 1 $ (exprVariable "i",0),1),(Modulo 1 (Set.singleton $ Scale 1 $ (exprVariable "i",0)) (Set.singleton $ Const n),2)]
|
|
i_mod_j_mapping :: VarMap
|
|
i_mod_j_mapping = Map.fromList [(Scale 1 $ (exprVariable "i",0),1),(Scale 1 $ (exprVariable "j",0),2),
|
|
(Modulo 1 (Set.singleton $ Scale 1 $ (exprVariable "i",0)) (Set.singleton $ Scale 1 $ (exprVariable "j",0)),3)]
|
|
_3i_2j_mod_mapping n = Map.fromList [(Scale 1 $ (exprVariable "i",0),1),(Scale 1 $ (exprVariable "j",0),2),
|
|
(Modulo 1 (Set.fromList [(Scale 3 $ (exprVariable "i",0)),(Scale (-2) $ (exprVariable "j",0))]) (Set.singleton $ Const n),3)]
|
|
-- i REM m, i + 1 REM n
|
|
i_ip1_mod_mapping m n = Map.fromList [(Scale 1 $ (exprVariable "i",0),1)
|
|
,(Modulo 1 (Set.singleton $ Scale 1 $ (exprVariable "i",0)) (Set.singleton $ Const m),2)
|
|
,(Modulo 1 (Set.fromList [Scale 1 $ (exprVariable "i",0), Const 1]) (Set.singleton $ Const n),3)
|
|
]
|
|
|
|
rep_i_mapping :: VarMap
|
|
rep_i_mapping = Map.fromList [((Scale 1 (exprVariable "i",0)),1), ((Scale 1 (exprVariable "i",1)),2)]
|
|
rep_i_mapping' :: VarMap
|
|
rep_i_mapping' = Map.fromList [((Scale 1 (exprVariable "i",0)),2), ((Scale 1 (exprVariable "i",1)),1)]
|
|
|
|
both_rep_i = joinMapping [rep_i_mapping, rep_i_mapping']
|
|
|
|
rep_i_mod_mapping :: Integer -> VarMap
|
|
rep_i_mod_mapping n = Map.fromList [((Scale 1 (exprVariable "i",0)),1), ((Scale 1 (exprVariable "i",1)),2)
|
|
,(Modulo 1 (Set.singleton $ Scale 1 $ (exprVariable "i",0)) (Set.singleton $ Const n),3)
|
|
,(Modulo 1 (Set.singleton $ Scale 1 $ (exprVariable "i",1)) (Set.singleton $ Const n),4)]
|
|
|
|
-- Helper functions for i REM 2 vs (i + 1) REM 4. Each one is a pair of equalities, inequalities
|
|
rr_i_zero = ([i === con 0], leq [con 0,con 0,con 7])
|
|
rr_ip1_zero = ([i ++ con 1 === con 0], leq [con 0,con 0,con 7])
|
|
rr_i_pos = ([], leq [con 0, i ++ 2**j, con 7] &&& [i >== con 1, j <== con 0] &&& leq [con 0, i ++ 2**j, con 1])
|
|
rr_ip1_pos = ([], leq [con 0, i ++ con 1 ++ 4**k, con 7] &&& [i ++ con 1 >== con 1, k <== con 0] &&& leq [con 0, i ++ con 1 ++ 4**k, con 3])
|
|
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])
|
|
|
|
combine :: (Int,Int) -> VarMap -> [([ModuloCase],[ModuloCase],[([HandyEq],[HandyIneq])])] -> [(((Int,[ModuloCase]),(Int,[ModuloCase])),VarMap,[HandyEq],[HandyIneq])]
|
|
combine (l0,l1) vm eq_ineqs = [(((l0,m0),(l1,m1)),vm,e,i) | (m0,m1,(e,i)) <- map (\(a,b,c) -> (a,b,transformPair concat concat $ unzip c)) eq_ineqs]
|
|
|
|
-- Helper functions for the replication:
|
|
|
|
ij_16 = leq [con 1, i, con 6] &&& leq [con 1, j, con 6]
|
|
|
|
testMakeEquation :: TestMonad m r => ([(((A.Expression, [ModuloCase]), (A.Expression, [ModuloCase])), VarMap,[HandyEq],[HandyIneq])],ParItems [A.Expression],A.Expression) -> m ()
|
|
testMakeEquation (problems, exprs, upperBound) =
|
|
assertEquivalentProblems ""
|
|
(map (\(x,y,z) -> (x, y, uncurry makeConsistent z)) $ map pairLatterTwo problems)
|
|
=<< (checkRight $ rr $ makeEquations (transformParItems pairWithEmpty exprs) upperBound)
|
|
where
|
|
pairWithEmpty a = ([],a,[])
|
|
pairLatterTwo (l,a,b,c) = (l,a,(b,c))
|
|
|
|
-- TODO add background knowledge
|
|
-- TODO add replicators
|
|
newtype MakeEquationInput = MEI ([(((A.Expression, [ModuloCase]), (A.Expression, [ModuloCase])), VarMap,[HandyEq],[HandyIneq])],ParItems [A.Expression],A.Expression)
|
|
|
|
-- Show isn't very useful on QuickCheck failure in this case and just spams the screen:
|
|
instance Show MakeEquationInput where
|
|
show = const ""
|
|
|
|
instance Arbitrary MakeEquationInput where
|
|
arbitrary = generateEquationInput >>* MEI
|
|
|
|
frequency' :: [(Int, StateT s Gen a)] -> StateT s Gen a
|
|
frequency' items = do dist <- lift $ choose (0, (sum $ map fst items) - 1)
|
|
findDist dist items
|
|
where
|
|
findDist n ((sz, x):sxs)
|
|
| n < sz = x
|
|
| otherwise = findDist (n - sz) sxs
|
|
|
|
-- | The item corresponding to the
|
|
type GenEqItems = (A.Expression, [(CoeffIndex, Integer)])
|
|
|
|
-- exprDepth is only really used to stop the possible infinite recursion in the multiplied variable * expression.
|
|
-- All other recursions are barred by never recursing with specialAllowed = True (outside of the above item)
|
|
|
|
-- Generates a new variable, or multiplied variable pair
|
|
genNewItem :: Int -> Bool -> StateT VarMap Gen (GenEqItems, FlattenedExp)
|
|
genNewItem exprDepth specialAllowed
|
|
= do (exp, fexp, nextId) <- frequency' $
|
|
[(80, do m <- get
|
|
let nextId = 1 + maximum (0 : Map.elems m)
|
|
let exp = exprVariable $ "x" ++ show nextId
|
|
return (exp, Scale 1 (exp,0), nextId))
|
|
,(20, if exprDepth <= 1
|
|
then
|
|
do m <- get
|
|
let nextId = 1 + maximum (0 : Map.elems m)
|
|
let exp = mulExprsInt (exprVariable $ "y" ++ show nextId) (exprVariable $ "y" ++ show nextId)
|
|
return (exp,Scale 1 (exp, 0), nextId)
|
|
else
|
|
do m <- get
|
|
((expToMult,_),_) <- genNewItem (exprDepth - 1) True
|
|
-- We deliberately overwrite the state here, because we don't need/want the items
|
|
-- produced in expToMult to be in the variable map (the real code won't bother
|
|
-- inserting them, only the multiplied item
|
|
put m
|
|
let nextId = 1 + maximum (0 : Map.elems m)
|
|
let exp = mulExprsInt (exprVariable $ "y" ++ show nextId) expToMult
|
|
return (exp, Scale 1 (exp, 0), nextId)
|
|
)
|
|
] ++ if not specialAllowed then []
|
|
else [(10, do ((eT,iT),fT) <- genNewExp (exprDepth - 1) False True
|
|
((eB,iB),fB) <- genNewExp (exprDepth - 1) False True
|
|
m <- get
|
|
let nextId = 1 + maximum (0 : Map.elems m)
|
|
return (dyadicExprInt "\\" eT eB, Modulo 1 (errorOrRight $ makeExpSet fT) (errorOrRight $ makeExpSet fB), nextId)
|
|
),(10,do ((eT,iT),fT) <- genNewExp (exprDepth - 1) False True
|
|
((eB,iB),fB) <- genConst
|
|
m <- get
|
|
let nextId = 1 + maximum (0 : Map.elems m)
|
|
return (divExprsInt eT eB, Divide 1 (errorOrRight $ makeExpSet fT) (Set.singleton fB), nextId)
|
|
)]
|
|
modify (Map.insert fexp nextId)
|
|
return ((exp, [(nextId,1)]), fexp)
|
|
|
|
errorOrRight :: Show a => Either a b -> b
|
|
errorOrRight (Left x) = error $ "Not Right: Left " ++ show x
|
|
errorOrRight (Right x) = x
|
|
|
|
genConst :: StateT VarMap Gen (GenEqItems, FlattenedExp)
|
|
genConst = do val <- lift $ choose (1, 10)
|
|
let exp = intLiteral val
|
|
return ((exp, [(0,val)]), Const val)
|
|
|
|
genNewExp :: Int -> Bool -> Bool -> StateT VarMap Gen (GenEqItems, [FlattenedExp])
|
|
genNewExp exprDepth specialAllowed constAllowed
|
|
= do num <- lift $ oneof $ map return [1,1,1,1,2,2,3] -- bias towards low numbers of items
|
|
items <- replicateM num $ frequency' [(if constAllowed then 20 else 0, maybeMult genConst),
|
|
(80, maybeMult $ genNewItem (exprDepth - 1) specialAllowed)]
|
|
return $ fromJust $ foldl join Nothing items
|
|
where
|
|
maybeMult :: StateT VarMap Gen (GenEqItems, FlattenedExp) -> StateT VarMap Gen (GenEqItems, FlattenedExp)
|
|
maybeMult x = do multOrNot <- lift $ oneof $ map return [-1,0,0,0,0,1] -- bias towards not multiplying (represented by zero)
|
|
unmult <- x
|
|
case multOrNot of
|
|
0 -> return unmult
|
|
sign -> do mult' <- lift $ choose (1 :: Integer,10)
|
|
let mult = sign * mult'
|
|
return $ transformPair
|
|
(transformPair (mulExprsInt (intLiteral mult)) (map (transformPair id (* mult))))
|
|
(scaleEq mult) unmult
|
|
scaleEq :: Integer -> FlattenedExp -> FlattenedExp
|
|
scaleEq k (Const n) = Const (k * n)
|
|
scaleEq k (Scale n v) = Scale (k * n) v
|
|
scaleEq k (Modulo n t b) = Modulo (k * n) t b
|
|
scaleEq k (Divide n t b) = Divide (k * n) t b
|
|
|
|
join :: Maybe (GenEqItems, [FlattenedExp]) -> (GenEqItems,FlattenedExp) -> Maybe (GenEqItems, [FlattenedExp])
|
|
join Nothing (e,f) = Just (e,[f])
|
|
join (Just ((ex,ix),fxs)) ((ey,iy),fy) = Just ((addExprsInt ex ey, ix ++ iy),fxs ++ [fy])
|
|
|
|
generateEquationInput :: Gen ([(((A.Expression,[ModuloCase]), (A.Expression,[ModuloCase])),VarMap,[HandyEq],[HandyIneq])],ParItems [A.Expression],A.Expression)
|
|
generateEquationInput
|
|
= do ((items, upper),vm) <- flip runStateT Map.empty
|
|
(do upper <- frequency' [(80, genConst >>* fst), (20, genNewExp 4 False True >>* fst)]
|
|
itemCount <- lift $ choose (1,5)
|
|
items <- replicateM itemCount (genNewExp 2 True True)
|
|
return (items, upper)
|
|
)
|
|
return (makeResults vm items upper, ParItems $ map (\((x,_),_) -> SeqItems [[x]]) items, fst upper)
|
|
where
|
|
makeResults :: VarMap ->
|
|
[(GenEqItems, [FlattenedExp])] ->
|
|
GenEqItems ->
|
|
[(((A.Expression,[ModuloCase]), (A.Expression,[ModuloCase])),VarMap,[HandyEq],[HandyIneq])]
|
|
makeResults vm items upper = concatMap (flip (makeResult vm) upper) (allPairs items)
|
|
|
|
makeResult :: VarMap -> ((GenEqItems, [FlattenedExp]), (GenEqItems, [FlattenedExp])) -> GenEqItems ->
|
|
[(((A.Expression,[ModuloCase]), (A.Expression,[ModuloCase])),VarMap,[HandyEq],[HandyIneq])]
|
|
makeResult vm (((ex,x),fx),((ey,y),fy)) (_,u) = mkItem (ex, moduloEq vm fx) (ey, moduloEq vm fy)
|
|
where
|
|
mkItem :: (A.Expression, [([ModuloCase], [(CoeffIndex, Integer)], [HandyEq], [HandyIneq])]) ->
|
|
(A.Expression, [([ModuloCase], [(CoeffIndex, Integer)], [HandyEq], [HandyIneq])]) ->
|
|
[(((A.Expression,[ModuloCase]), (A.Expression,[ModuloCase])),VarMap,[HandyEq],[HandyIneq])]
|
|
mkItem (ex, xinfo) (ey, yinfo) = map (\(mx,my,eq,ineq) -> (((ex,mx),(ey,my)),vm,eq,ineq)) $ map (uncurry joinItems) (product2 (xinfo, yinfo))
|
|
|
|
joinItems :: ([ModuloCase],[(CoeffIndex, Integer)], [HandyEq], [HandyIneq]) ->
|
|
([ModuloCase],[(CoeffIndex, Integer)], [HandyEq], [HandyIneq]) ->
|
|
([ModuloCase], [ModuloCase], [HandyEq],[HandyIneq])
|
|
joinItems (mx, x, xEq, xIneq) (my, y, yEq, yIneq) = (mx, my, [x === y] &&& xEq &&& yEq, xIneq &&& yIneq &&& arrayBound x u &&& arrayBound y u)
|
|
|
|
arrayBound :: [(CoeffIndex, Integer)] -> [(CoeffIndex, Integer)] -> [HandyIneq]
|
|
arrayBound x u = leq [con 0, x, u ++ con (-1)]
|
|
|
|
moduloEq :: VarMap -> [FlattenedExp] -> [([ModuloCase], [(CoeffIndex, Integer)], [HandyEq], [HandyIneq])]
|
|
moduloEq vm es = foldl join [([],[],[],[])] (map (moduloEq' vm) es)
|
|
where
|
|
join :: [([ModuloCase], [(CoeffIndex, Integer)], [HandyEq], [HandyIneq])] ->
|
|
[([ModuloCase], [(CoeffIndex, Integer)], [HandyEq], [HandyIneq])] ->
|
|
[([ModuloCase], [(CoeffIndex, Integer)], [HandyEq], [HandyIneq])]
|
|
join xs ys = map (uncurry join') $ product2 (xs,ys)
|
|
|
|
join' :: ([ModuloCase], [(CoeffIndex, Integer)], [HandyEq], [HandyIneq]) ->
|
|
([ModuloCase], [(CoeffIndex, Integer)], [HandyEq], [HandyIneq]) ->
|
|
([ModuloCase], [(CoeffIndex, Integer)], [HandyEq], [HandyIneq])
|
|
join' (msx, isx, eqsx, ineqsx) (msy, isy, eqsy, ineqsy) = (msx ++ msy, isx ++ isy, eqsx ++ eqsy, ineqsx ++ ineqsy)
|
|
|
|
moduloEq' :: VarMap -> FlattenedExp -> [([ModuloCase], [(CoeffIndex, Integer)], [HandyEq], [HandyIneq])]
|
|
moduloEq' vm m@(Modulo n top bottom) =
|
|
let topVar = lookupFS (Set.toList top) vm
|
|
botVar = lookupFS (Set.toList bottom) vm
|
|
modVar = lookupF m vm
|
|
in case onlyConst (Set.toList bottom) of
|
|
Just c -> let v = topVar ++ (abs c)**modVar in
|
|
[ ([XZero], [(0,0)], [topVar === con 0], [])
|
|
, ([XPos], n**v, [], [topVar >== con 1, modVar <== con 0] &&& leq [con 0, v, con (abs c - 1)])
|
|
, ([XNeg], n**v, [], [topVar <== con (-1), modVar >== con 0] &&& leq [con (1 - abs c), v, con 0])
|
|
]
|
|
Nothing -> let v = topVar ++ modVar in
|
|
[ ([XZero], [(0,0)], [topVar === con 0], []) -- TODO stop the divisor being zero
|
|
|
|
, ([XPosYPosAZero], n**topVar, [], [topVar >== con 1] &&& leq [con 0, topVar, botVar ++ con (-1)])
|
|
, ([XPosYNegAZero], n**topVar, [], [topVar >== con 1] &&& leq [con 0, topVar, (-1)**botVar ++ con (-1)])
|
|
, ([XNegYPosAZero], n**topVar, [], [topVar <== con (-1)] &&& leq [(-1)**botVar ++ con 1, topVar, con 0])
|
|
, ([XNegYNegAZero], n**topVar, [], [topVar <== con (-1)] &&& leq [botVar ++ con 1, topVar, con 0])
|
|
|
|
, ([XPosYPosANonZero], n**v, [], [topVar >== con 1, modVar <== (-1)**botVar] &&& leq [con 0, v, botVar ++ con (-1)])
|
|
, ([XPosYNegANonZero], n**v, [], [topVar >== con 1, modVar <== botVar] &&& leq [con 0, v, (-1)**botVar ++ con (-1)])
|
|
|
|
, ([XNegYPosANonZero], n**v, [], [topVar <== con (-1), modVar >== botVar] &&& leq [(-1)**botVar ++ con 1, v, con 0])
|
|
, ([XNegYNegANonZero], n**v, [], [topVar <== con (-1), modVar >== (-1)**botVar] &&& leq [botVar ++ con 1, v, con 0])
|
|
]
|
|
moduloEq' vm m@(Divide n top bottom) =
|
|
[ ([XZero], [(0,0)], [topVar === con 0], [])
|
|
, ([XPos], n**divVar, [], [topVar >== con 1] &&& eqs (resultSignum True))
|
|
, ([XNeg], n**divVar, [], [topVar <== con (-1)] &&& eqs (resultSignum False))
|
|
]
|
|
where
|
|
topVar = lookupFS (Set.toList top) vm
|
|
divVar = lookupF m vm
|
|
c = fromJust $ onlyConst (Set.toList bottom)
|
|
v = topVar ++ (-c)**divVar
|
|
|
|
resultSignum xpos = signum c * (if xpos then 1 else -1)
|
|
|
|
-- TopSign BottomSign Bounds:
|
|
-- +++ +++ (0, c - 1)
|
|
-- +++ --- (c + 1, 0) (or: 1 - abs c, 0)
|
|
-- --- +++ (1 - c, 0)
|
|
-- --- --- (0, -1 - c) (or: (0, abs c - 1)
|
|
eqs sign = [sign**divVar >== con 0] &&& leq
|
|
(if signum c == sign
|
|
then [con 0, v, con (abs c - 1)]
|
|
else [con (1 - abs c), v, con 0])
|
|
moduloEq' vm exp = [([], lookupF exp vm, [], [])]
|
|
|
|
lookupFS :: [FlattenedExp] -> VarMap -> [(CoeffIndex, Integer)]
|
|
lookupFS es vm = concatMap (flip lookupF vm) es
|
|
|
|
lookupF :: FlattenedExp -> VarMap -> [(CoeffIndex, Integer)]
|
|
lookupF (Const c) _ = con c
|
|
lookupF f@(Scale a v) vm = [(fromJust $ Map.lookup f vm, a)]
|
|
-- We don't scale modulo directly here because the modulo variable is a or m,
|
|
-- which shouldn't be scaled
|
|
lookupF f@(Modulo a t b) vm = [(fromJust $ Map.lookup f vm, 1)]
|
|
lookupF f@(Divide a t b) vm = [(fromJust $ Map.lookup f vm, 1)]
|
|
|
|
--TODO deal with this counter-example (related to canonical form of expressions, I think):
|
|
--Keys in variable mapping [((9 * x9) + (-9 * x10)),(x7 + x8),(-10 * x6),(((8 * x3) + (y4 * y4)) / 2)]
|
|
--expected: [(y1 * ((x1 + (y2 * y2)) REM x3)),(y4 * y4),x10,x2,x3,x6,x7,x8,x9,((y4 * y4) + 8*x3 / 2)]
|
|
-- but got: [(y1 * (((y2 * y2) + x1) REM x3)),(y4 * y4),x10,x2,x3,x6,x7,x8,x9,((y4 * y4) + 8*x3 / 2)]
|
|
|
|
qcTestMakeEquations :: [LabelledQuickCheckTest]
|
|
qcTestMakeEquations = [("Turning Code Into Equations", scaleQC (20,100,400,1000) (runQCTest . prop))]
|
|
where
|
|
prop :: MakeEquationInput -> QCProp
|
|
prop (MEI mei) = testMakeEquation mei
|
|
|
|
testIndexes :: Test
|
|
testIndexes = TestList
|
|
[
|
|
|
|
check (SolveEq $ answers [(i,7)]) (0, [i === con 7], [])
|
|
,check (SolveEq $ answers [(i,6)]) (1, [2 ** i === con 12], [])
|
|
,check ImpossibleEq (2, [i === con 7],[i <== con 5])
|
|
|
|
-- Can i = j?
|
|
,check ImpossibleEq (3, [i === j], i_j_constraint 0 9)
|
|
|
|
-- Can (j + 1 % 10 == i + 1 % 10)?
|
|
,check ImpossibleIneq $ withKIsMod (i ++ con 1) 10 $ withNIsMod (j ++ con 1) 10 $ (4, [k === n], i_j_constraint 0 9)
|
|
-- Off by one (i + 1 % 9)
|
|
,check SolveIneq $ withKIsMod (i ++ con 1) 9 $ withNIsMod (j ++ con 1) 9 $ (5, [k === n], i_j_constraint 0 9)
|
|
|
|
-- The "nightmare" example from the Omega Test paper:
|
|
,check ImpossibleIneq (6,[],leq [con 27, 11 ** i ++ 13 ** j, con 45] &&& leq [con (-10), 7 ** i ++ (-9) ** j, con 4])
|
|
|
|
-- Solution is: i = 0, j = 0, k = 0
|
|
,check (SolveEq $ answers [(i,0),(j,0),(k,0)])
|
|
(7, [con 0 === i ++ j ++ k,
|
|
con 0 === 5 ** i ++ 4 ** j ++ 3 ** k,
|
|
con 0 === i ++ 6 ** j ++ 2 ** k]
|
|
, [con 1 >== i ++ 3 ** j ++ k,
|
|
con (-4) <== (-5) ** i ++ 2 ** j ++ k,
|
|
con 0 >== 4 ** i ++ (-7) ** j ++ (-13) ** k])
|
|
|
|
-- Solution is i = 0, j = 0, k = 4
|
|
,check (SolveEq $ answers [(i,0),(j,0),(k,4)])
|
|
(8, [con 4 === i ++ j ++ k,
|
|
con 12 === 5 ** i ++ 4 ** j ++ 3 ** k,
|
|
con 8 === i ++ 6 ** j ++ 2 ** k]
|
|
, [con 5 >== i ++ 3 ** j ++ k,
|
|
con 3 <== (-5) ** i ++ 2 ** j ++ k,
|
|
con (-52) >== 4 ** i ++ (-7) ** j ++ (-13) ** k])
|
|
|
|
-- Solution is: i = 0, j = 5, k = 4, but
|
|
-- this can't be determined from the equalities alone.
|
|
,check SolveIneq (9, [con 32 === 4 ** i ++ 4 ** j ++ 3 ** k,
|
|
con 17 === i ++ j ++ 3 ** k,
|
|
con 54 === 10 ** i ++ 10 ** j ++ k]
|
|
, [3 ** i ++ 8 ** j ++ 5 ** k >== con 60,
|
|
i ++ j ++ 3 ** k >== con 17,
|
|
5 ** i ++ j ++ 5 ** k >== con 25])
|
|
|
|
-- If we have (solution: 1,2):
|
|
-- 5 <= 5y - 4x <= 7
|
|
-- 9 <= 3y + 4x <= 11
|
|
-- Bounds on x:
|
|
-- Upper: 4x <= 5y - 5, 4x <= 11 - 3y
|
|
-- Lower: 5y - 7 <= 4x, 9 - 3y <= 4x
|
|
-- Dark shadow of x includes:
|
|
-- 4(11 - 3y) - 4(9 - 3y) >= 9, gives 8 >= 9.
|
|
-- Bounds on y:
|
|
-- Upper: 5y <= 7 + 4x, 3y <= 11 - 4x
|
|
-- Lower: 5 + 4x <= 5y, 9 - 4x <= 3y
|
|
-- Dark shadow of y includes:
|
|
-- 5(7 + 4x) - 5(5 + 4x) >= 16, gives 10 >= 16
|
|
-- So no solution to dark shadow, either way!
|
|
,check SolveIneq (10, [], leq [con 5, 5 ** i ++ (-4) ** j, con 7] &&& leq [con 9, 3 ** i ++ 4 ** j, con 11])
|
|
|
|
|
|
,safeParTest 100 True (0,10) [i]
|
|
,safeParTest 120 False (0,10) [i,i ++ con 1]
|
|
,safeParTest 140 True (0,10) [2 ** i, 2 ** i ++ con 1]
|
|
]
|
|
where
|
|
-- Given some indexes using "i", this function checks whether these can
|
|
-- ever overlap within the bounds given, and matches this against
|
|
-- the expected value; True for safe, False for unsafe.
|
|
safeParTest :: Int -> Bool -> (Integer,Integer) -> [[(Int,Integer)]] -> Test
|
|
safeParTest ind expSafe (low, high) usesI = TestCase $
|
|
(if expSafe
|
|
then assertEqual ("testIndexes " ++ show ind ++ " should be safe (unsolveable)") []
|
|
else assertNotEqual ("testIndexes " ++ show ind ++ " should be solveable") []
|
|
)
|
|
$ findSolveable $ zip3 [ind..] (equalityCombinations) (repeat constraint)
|
|
where
|
|
changeItoJ (1,n) = (2,n)
|
|
changeItoJ x = x
|
|
|
|
usesJ = map (map changeItoJ) usesI
|
|
|
|
constraint = i_j_constraint low high
|
|
|
|
equalityCombinations :: [[HandyEq]]
|
|
equalityCombinations = map (\(lhs,rhs) -> [lhs === rhs]) $ product2 (usesI,usesJ)
|
|
|
|
|
|
findSolveable :: [(Int, [HandyEq], [HandyIneq])] -> [(Int, [HandyEq], [HandyIneq])]
|
|
findSolveable = filter isSolveable
|
|
|
|
isSolveable :: (Int, [HandyEq], [HandyIneq]) -> Bool
|
|
isSolveable (ind, eq, ineq) = isJust $ (uncurry solveProblem) (makeConsistent eq ineq)
|
|
|
|
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 :: [(Int, Integer)]
|
|
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')
|
|
|
|
-- | Given one mapping and a second mapping, gives a function that converts the indexes
|
|
-- from one to the indexes of the next. If any of the keys in the map don't match
|
|
-- (i.e. if (keys m0 /= keys m1)) Nothing will be returned
|
|
|
|
generateMapping :: TestMonad m r => String -> VarMap -> VarMap -> m [(CoeffIndex,CoeffIndex)]
|
|
generateMapping msg m0 m1
|
|
= do testEqual ("Keys in variable mapping " ++ msg) (Map.keys m0') (Map.keys m1')
|
|
return $ Map.elems $ zipMap mergeMaybe m0' m1'
|
|
where
|
|
m0' = Map.mapKeys (fmapFlattenedExp (fromRight . rr . canonicalise)) m0
|
|
m1' = Map.mapKeys (fmapFlattenedExp (fromRight . rr . canonicalise)) m1
|
|
|
|
fromRight :: Either String a -> a
|
|
fromRight (Right s) = s
|
|
fromRight (Left _) = error "fromRight found Left"
|
|
|
|
-- | Given a forward mapping list, translates equations across
|
|
translateEquations :: forall m r. TestMonad m r =>
|
|
[(CoeffIndex,CoeffIndex)] -> (EqualityProblem, InequalityProblem) -> m (EqualityProblem, InequalityProblem)
|
|
translateEquations mp (eq,ineq)
|
|
= do testEqual "translateEquations mapping not one-to-one" (sort $ map fst mp) (sort $ map snd mp)
|
|
testCompareCustom "translateEquations input not square" (>=) 1 $ length $ nub $ map (snd . bounds) $ eq ++ ineq
|
|
eq' <- mapM swapColumns eq
|
|
ineq' <- mapM swapColumns ineq
|
|
return (eq', ineq')
|
|
where
|
|
swapColumns :: Array CoeffIndex Integer -> m (Array CoeffIndex Integer)
|
|
swapColumns arr
|
|
= do swapped <- mapM swapColumns' $ assocs arr
|
|
check arr swapped
|
|
return $ simpleArray swapped
|
|
where
|
|
swapColumns' :: (CoeffIndex,Integer) -> m (CoeffIndex,Integer)
|
|
swapColumns' (0,v) = return (0,v) -- Never swap the units column
|
|
swapColumns' (x,v)
|
|
= case find ((== x) . fst) mp of
|
|
Just (_,y) -> return (y,v)
|
|
Nothing -> testFailure "Could not find column to swap to" >> return undefined
|
|
|
|
check :: Show a => a -> [(CoeffIndex,Integer)] -> m ()
|
|
check x ies = if length ies == 1 + maximum (map fst ies) then return () else
|
|
testFailure $ "Error in translateEquations, not all indexes present after swap: " ++ show ies
|
|
++ " value beforehand was: " ++ show x ++ " mapping was: " ++ show mp
|
|
|
|
instance (ShowOccam a, Show b) => ShowOccam (a,b) where
|
|
showOccamM (x,y) = showOccamM x >> tell [show y]
|
|
|
|
type Problem = (((A.Expression, [ModuloCase]), (A.Expression, [ModuloCase])), VarMap, (EqualityProblem, InequalityProblem))
|
|
|
|
-- | Asserts that the two problems are equivalent, once you take into account the potentially different variable mappings
|
|
assertEquivalentProblems :: forall m r. (TestMonad m r) => String -> [Problem] -> [Problem] -> m ()
|
|
assertEquivalentProblems title exp act
|
|
= do testEqualCustomShow (showListCustom $ showPairCustom showLabel showLabel) "Label sets not equal"
|
|
(map fst3 $ sortByLabels exp) (map fst3 $ sortByLabels act)
|
|
transformed <- mapM (uncurry $ transform $ showPairCustom showLabel showLabel) $ zip (sortByLabels exp) (sortByLabels act)
|
|
-- let transformedSortedZipped = map (transformPair id (zip . transformPair sortProblem sortProblem . unzip)) $ transformed
|
|
-- To give a more useful error on large problems we compare each item individually:
|
|
mapM_ test $ zip [0..] $ map (transformPair (\(e,a) -> showOccam e ++ " = " ++ showOccam a) id) transformed
|
|
testEqual (title ++ " Problems were not the same size") (length exp) (length act)
|
|
where
|
|
test :: (Int, (String, ((EqualityProblem, InequalityProblem), (EqualityProblem, InequalityProblem)))) -> m ()
|
|
test (n, (l, (eps, aps))) = testEqualCustomShow showProblem (title ++ " " ++ l ++ " #" ++ show n) eps aps
|
|
|
|
showLabel :: (A.Expression, [ModuloCase]) -> String
|
|
showLabel = showPairCustom showOccam show
|
|
|
|
showFunc :: (Int, [(EqualityProblem, InequalityProblem)]) -> String
|
|
showFunc = showPairCustom show $ showListCustom $ showProblem
|
|
|
|
fst3 :: (a,b,c) -> a
|
|
fst3 (a,_,_) = a
|
|
|
|
sortByLabels :: [Problem] -> [Problem]
|
|
sortByLabels = sortBy (comparing fst3) . map (\(es,b,c) -> (sortPair es, b, c))
|
|
|
|
sortPair :: Ord a => (a,a) -> (a, a)
|
|
sortPair (x,y) | x <= y = (x,y)
|
|
| otherwise = (y,x)
|
|
|
|
sortP :: (EqualityProblem, InequalityProblem) -> (EqualityProblem, InequalityProblem)
|
|
sortP (eq,ineq) = (sort $ map normaliseEquality eq, sort ineq)
|
|
|
|
transform :: Eq label => (label -> String) ->
|
|
(label, VarMap, (EqualityProblem, InequalityProblem)) ->
|
|
(label, VarMap, (EqualityProblem, InequalityProblem)) ->
|
|
m ( label, ((EqualityProblem, InequalityProblem), (EqualityProblem, InequalityProblem)))
|
|
transform s (el, vmexp, (e_eq, e_ineq)) (al, vmact, (a_eq, a_ineq))
|
|
= do testEqualCustomShow s "Labels did not match" el al
|
|
mapping <- generateMapping (showListCustom showOccam $ sort . nub $ map (fst . fst . fst3) exp ++ map (fst . snd . fst3) exp) (vmexp) (vmact)
|
|
translatedExp <- translateEquations mapping (resize e_eq, resize e_ineq)
|
|
return (el, (sortP translatedExp, sortP (resize a_eq, resize a_ineq)))
|
|
where
|
|
size = maximum $ map (snd . bounds) $ concat [e_eq, e_ineq, a_eq, a_ineq]
|
|
|
|
resize :: [Array CoeffIndex Integer] -> [Array CoeffIndex Integer]
|
|
resize = map (makeArraySize (0, size) 0)
|
|
|
|
|
|
|
|
pairPairs (xa,ya) (xb,yb) = ((xa,xb), (ya,yb))
|
|
|
|
sortProblem :: [(EqualityProblem, InequalityProblem)] -> [(EqualityProblem, InequalityProblem)]
|
|
sortProblem = sort
|
|
|
|
-- QuickCheck tests for Omega Test:
|
|
-- The idea is to begin with a random list of integers, representing answers.
|
|
-- Combine this with a randomly generated matrix of coefficients for equalities
|
|
-- and the similar for inequalities. Correct all the unit coefficients such that
|
|
-- the equalities are true, and the inequalities should all resolve such that
|
|
-- LHS = RHS (and therefore they will be pruned out)
|
|
|
|
-- | We want to generate a solveable equation. Expressing our N equations as a matrix A (size: NxN),
|
|
-- we get: A . x = b, where b is our solution. The equations are solveable iff x = inv(A) . b
|
|
-- Or expressed another way, the equations are solveable iff A is nonsingular;
|
|
-- see http://mathworld.wolfram.com/LinearSystemofEquations.html A is singular if it
|
|
-- has determinant zero, therefore A is non-singular if the determinant is non-zero.
|
|
-- See http://mathworld.wolfram.com/Determinant.html for this.
|
|
--
|
|
-- At first I tried to simply check the determinant of a randomly generated matrix.
|
|
-- I implemented the standard naive algorithm, which is O(N!). Eeek! Reading the maths
|
|
-- more, a quicker way to do the determinant of a matrix M is to decompose it into
|
|
-- M = LU (where L is lower triangular, and U is upper triangular). Once you have
|
|
-- done this, you can use det M = det (LU) = (det L) . (det U) (from the Determinant page)
|
|
-- This is easier because det (A) where A is triangular, is simply the product
|
|
-- of its diagonal elements (see http://planetmath.org/encyclopedia/TriangularMatrix.html).
|
|
--
|
|
-- However, we don't need to do this the hard way. We just want to generate a matrix M
|
|
-- where its determinant is non-zero. If we imagine M = LU, then (det M) is non-zero
|
|
-- as long as (det L) is non-zero AND (det U) is non-zero. In turn, det L and det U are
|
|
-- non-zero as long as all their diagonal elements are non-zero. Therefore we just
|
|
-- need to randomly generate L and U (such that the diagonal elements are all non-zero)
|
|
-- and do M = LU.
|
|
--
|
|
-- Note that we should not take the shortcut of using just L or just U. This would
|
|
-- lead to trivially solveable linear equations, which would not test our algorithm well!
|
|
generateInvertibleMatrix :: Int -> Gen [[Integer]]
|
|
generateInvertibleMatrix size
|
|
= do u <- genUpper
|
|
l <- genLower
|
|
return $ l `multMatrix` u
|
|
where
|
|
ns = [0 .. size - 1]
|
|
|
|
-- | From http://mathworld.wolfram.com/MatrixMultiplication.html:
|
|
-- To multiply two square matrices of size N:
|
|
-- c_ik = sum (j in 0 .. N-1) (a_ij . b_jk)
|
|
-- Note that we begin our indexing at zero, because that's how !! works.
|
|
multMatrix a b = [[sum [((a !! i) !! j) * ((b !! j) !! k) | j <- ns] | k <- ns] | i <- ns]
|
|
|
|
genUpper :: Gen [[Integer]]
|
|
genUpper = mapM sequence [[
|
|
case i `compare` j of
|
|
EQ -> oneof [choose (-10,-1),choose (1,10)]
|
|
LT -> return 0
|
|
GT -> choose (-10,10)
|
|
| i <- ns] |j <- ns]
|
|
|
|
genLower :: Gen [[Integer]]
|
|
genLower = mapM sequence [[
|
|
case i `compare` j of
|
|
EQ -> oneof [choose (-10,-1),choose (1,10)]
|
|
GT -> return 0
|
|
LT -> choose (-10,10)
|
|
| i <- ns] |j <- ns]
|
|
|
|
-- | Given a solution, and the coefficients, work out the result.
|
|
-- Effectively the dot-product of the two lists.
|
|
calcUnits :: [Integer] -> [Integer] -> Integer
|
|
calcUnits a b = sum $ zipWith (*) a b
|
|
|
|
-- | Given the solution for an equation (values of x_1 .. x_n), generates
|
|
-- equalities and inequalities. The equalities will all be true and consistent,
|
|
-- the inequalities will all turn out to be equal. That is, when the inequalities
|
|
-- are resolved, the LHS will equal 0. Therefore we can generate the inequalities
|
|
-- using the same method as equalities. Also, the equalities are assured to be
|
|
-- distinct. If they were not distinct (one could be transformed into another by scaling)
|
|
-- then the equation set would be unsolveable.
|
|
generateEqualities :: [Integer] -> Gen (EqualityProblem, InequalityProblem)
|
|
generateEqualities solution = do eqCoeffs <- generateInvertibleMatrix num_vars
|
|
ineqCoeffs <- generateInvertibleMatrix num_vars
|
|
return (map mkCoeffArray eqCoeffs, map mkCoeffArray ineqCoeffs)
|
|
where
|
|
num_vars = length solution
|
|
mkCoeffArray coeffs = arrayise $ (negate $ calcUnits solution coeffs) : coeffs
|
|
|
|
-- | The input to a test that will have an exact solution after the equality problems have been
|
|
-- solved. All the inequalities will be simplified to 0 = 0. The answers to the equation are
|
|
-- in the map.
|
|
newtype OmegaTestInput = OMI (Map.Map CoeffIndex Integer,(EqualityProblem, InequalityProblem)) deriving (Show)
|
|
|
|
-- | Generates an Omega test problem with between 1 and 10 variables (incl), where the solutions
|
|
-- are numbers between -20 and + 20 (incl).
|
|
generateProblem :: Gen (Map.Map CoeffIndex Integer,(EqualityProblem, InequalityProblem))
|
|
generateProblem = choose (1,10) >>= (\n -> replicateM n $ choose (-20,20)) >>=
|
|
(\ans -> seqPair (return $ makeAns (zip [1..] ans),generateEqualities ans))
|
|
where
|
|
makeAns :: [(Int, Integer)] -> Map.Map CoeffIndex Integer
|
|
makeAns = Map.fromList
|
|
|
|
instance Arbitrary OmegaTestInput where
|
|
arbitrary = generateProblem >>* OMI
|
|
|
|
qcOmegaEquality :: [LabelledQuickCheckTest]
|
|
qcOmegaEquality = [("Omega Test Equality Solving", scaleQC (40,200,2000,10000) (runQCTest . prop))]
|
|
where
|
|
prop :: OmegaTestInput -> QCProp
|
|
prop (OMI (ans,(eq,ineq))) = omegaCheck actAnswer
|
|
where
|
|
actAnswer = solveConstraints (defaultMapping $ Map.size ans) eq ineq
|
|
-- We use Map.assocs because pshow doesn't work on Maps
|
|
omegaCheck (Just (vm,ineqs)) = (True *==* all (all (== 0) . elems) ineqs)
|
|
*&&* ((Map.assocs $ fmap Right ans) *==* (Map.assocs $ getCounterEqs vm))
|
|
omegaCheck Nothing = testFailure ("Found Nothing while expecting answer: " ++ show (eq,ineq))
|
|
|
|
-- | A randomly mutated problem ready for testing the inequality pruning.
|
|
-- The first part is the input to the pruning, and the second part is the expected result;
|
|
-- the remaining inequalities, preceding by a list of equalities.
|
|
type MutatedProblem =
|
|
(InequalityProblem
|
|
,Maybe ([EqualityConstraintEquation],InequalityProblem))
|
|
|
|
-- | The type for inside the function; easier to work with since it can't be
|
|
-- inconsistent until the end.
|
|
type MutatedProblem' =
|
|
(InequalityProblem
|
|
,[EqualityConstraintEquation]
|
|
,InequalityProblem)
|
|
|
|
-- | Given a distinct inequality list, mutates each one at random using one of these mutations:
|
|
-- * Unchanged
|
|
-- * Generates similar but redundant equations
|
|
-- * Generates its dual (to be transformed into an equality equation)
|
|
-- * Generates an inconsistent partner (rare - 20% chance of existing in the returned problem).
|
|
-- The equations passed in do not have to be consistent, merely unique and normalised.
|
|
-- Returns the input, and the expected output.
|
|
mutateEquations :: InequalityProblem -> Gen MutatedProblem
|
|
mutateEquations ineq = do (a,b,c) <- mapM mutate ineq >>*
|
|
foldl (\(a,b,c) (x,y,z) -> (a++x,b++y,c++z)) ([],[],[])
|
|
frequency
|
|
[
|
|
(80,return (a,Just (b,c)))
|
|
,(20,addInconsistent a >>* (\x -> (x,Nothing)))
|
|
]
|
|
where
|
|
-- We take an equation like 5 + 3x - y >=0 (i.e. 3x - y >= -5)
|
|
-- and add -6 -3x + y >= 0 (i.e. -6 >= 3x - y)
|
|
-- This works for all cases, even where the unit coeff is zero;
|
|
-- 3x - y >= 0 becomes -1 -3x + y >= 0 (i.e. -1 >= 3x - y)
|
|
addInconsistent :: InequalityProblem -> Gen InequalityProblem
|
|
addInconsistent inpIneq
|
|
= do randEq <- oneof (map return inpIneq)
|
|
let negEq = amap negate randEq
|
|
let modRandEq = (negEq) // [(0, (negEq ! 0) - 1)]
|
|
return (modRandEq : inpIneq)
|
|
|
|
mutate :: InequalityConstraintEquation -> Gen MutatedProblem'
|
|
mutate ineq = oneof
|
|
[
|
|
return ([ineq],[],[ineq])
|
|
,addRedundant ineq
|
|
,return $ addDual ineq
|
|
]
|
|
|
|
addDual :: InequalityConstraintEquation -> MutatedProblem'
|
|
addDual eq = ([eq,neg],[eq],[]) where neg = amap negate eq
|
|
|
|
addRedundant :: InequalityConstraintEquation -> Gen MutatedProblem'
|
|
addRedundant ineq = do i <- choose (1,5) -- number of redundant equations to add
|
|
newIneqs <- replicateM i addRedundant'
|
|
return (ineq : newIneqs, [], [ineq])
|
|
where
|
|
-- A redundant equation is one with a bigger unit coefficient:
|
|
addRedundant' = do n <- choose (1,100)
|
|
return $ ineq // [(0,n + (ineq ! 0))]
|
|
|
|
-- | Puts an equality into normal form. This is where the first non-zero coefficient is positive.
|
|
-- If all coefficients are zero, it doesn't matter (it will be equal to its negation)
|
|
normaliseEquality :: EqualityConstraintEquation -> EqualityConstraintEquation
|
|
normaliseEquality eq = case listToMaybe $ filter (/= 0) $ elems eq of
|
|
Nothing -> eq -- all zeroes
|
|
Just x -> amap (* (signum x)) eq
|
|
|
|
newtype OmegaPruneInput = OPI MutatedProblem deriving (Show)
|
|
|
|
instance Arbitrary OmegaPruneInput where
|
|
arbitrary = ((generateProblem >>* snd) >>= (return . snd) >>= mutateEquations) >>* OPI
|
|
|
|
qcOmegaPrune :: [LabelledQuickCheckTest]
|
|
qcOmegaPrune = [("Omega Test Pruning", scaleQC (100,1000,10000,50000) prop)]
|
|
where
|
|
--We perform the map assocs because we can't compare arrays using *==*
|
|
-- (toConstr fails in the pretty-printing!).
|
|
prop (OPI (inp,out)) = True
|
|
{-
|
|
case out of
|
|
Nothing -> Nothing *==* result
|
|
Just (expEq,expIneq) ->
|
|
case result of
|
|
Nothing -> mkFailResult $ "Expected success but got failure: " ++ pshow (inp,out)
|
|
Just (actEq,actIneq) ->
|
|
(sort (map assocs expIneq) *==* sort (map assocs actIneq))
|
|
*&&* ((sort $ map normaliseEquality expEq) *==* (sort $ map normaliseEquality actEq))
|
|
where
|
|
result = undefined -- TODO replace solveAndPrune: solveProblem [] inp
|
|
-}
|
|
|
|
vioqcTests :: Int -> IO (Test, [LabelledQuickCheckTest])
|
|
vioqcTests v
|
|
= seqPair
|
|
(liftM (TestLabel "ArrayUsageCheckTest" . TestList) $ sequence $
|
|
map return [
|
|
testArrayCheck
|
|
,testIndexes
|
|
,testMakeEquations
|
|
]
|
|
++ map (automaticTest FrontendOccam v)
|
|
["testcases/automatic/usage-check-1.occ.test"
|
|
,"testcases/automatic/usage-check-2.occ.test"
|
|
,"testcases/automatic/usage-check-3.occ.test"
|
|
,"testcases/automatic/usage-check-4.occ.test"
|
|
,"testcases/automatic/usage-check-5.occ.test"
|
|
,"testcases/automatic/usage-check-6.occ.test"
|
|
,"testcases/automatic/usage-check-7.occ.test"
|
|
,"testcases/automatic/usage-check-8.occ.test"
|
|
,"testcases/automatic/usage-check-9.occ.test"
|
|
,"testcases/automatic/usage-check-10.occ.test"
|
|
]
|
|
,return $ qcOmegaEquality ++ qcOmegaPrune ++ qcTestMakeEquations)
|
|
|
|
|
|
|