Introduced scaling of Modulo and Divide items, and tweaked some of the parameters to make the tests a little shorter
This commit is contained in:
Neil Brown
parent
25be01cb47
commit
41ab2d6bde
|
|
@ -486,11 +486,6 @@ makeEquations otherInfo accesses bound
|
|||
|
||||
-- Note that in all these functions, the divisor should always be positive!
|
||||
|
||||
-- Takes an expression, and transforms it into an expression like:
|
||||
-- (e_0 + e_1 + e_2) / d
|
||||
-- where d is a constant (non-zero!) integer, and each e_k
|
||||
-- is either a const, a var, const * var, or (const * var) % const [TODO].
|
||||
-- If the expression cannot be transformed into such a format, an error is returned
|
||||
flatten :: A.Expression -> Either String [FlattenedExp]
|
||||
flatten (A.Literal _ _ (A.IntLiteral _ n)) = return [Const (read n)]
|
||||
flatten (A.ExprVariable _ v) = return [Scale 1 (v,0)]
|
||||
|
|
@ -525,7 +520,8 @@ flatten (A.Dyadic m op lhs rhs) | op == A.Add = combine' (flatten lhs) (flatte
|
|||
scale :: Integer -> FlattenedExp -> Either String FlattenedExp
|
||||
scale sc (Const n) = return $ Const (n * sc)
|
||||
scale sc (Scale n v) = return $ Scale (n * sc) v
|
||||
-- TODO test the other cases then write them
|
||||
scale sc (Modulo n t b) = return $ Modulo (n * sc) t b
|
||||
scale sc (Divide n t b) = return $ Divide (n * sc) t b
|
||||
|
||||
-- | An easy way of applying combine to two monadic returns
|
||||
combine' :: Either String [FlattenedExp] -> Either String [FlattenedExp] -> Either String [FlattenedExp]
|
||||
|
|
@ -696,14 +692,15 @@ makeEquation l t summedItems
|
|||
[([ModuloCase], Map.Map Int Integer,[Map.Map Int Integer], [Map.Map Int Integer])]
|
||||
makeEquation' m (Const n) = return $ add (0,n) m
|
||||
makeEquation' m sc@(Scale n v) = varIndex sc >>* (\ind -> add (ind, n) m)
|
||||
makeEquation' m mod@(Modulo _ top bottom) -- TODO use the scale properly
|
||||
makeEquation' m mod@(Modulo n top bottom)
|
||||
= do top' <- process (Set.toList top) >>* map (\(_,a,b,c) -> (a,b,c))
|
||||
top'' <- getSingleItem "Modulo or divide not allowed in the numerator of Modulo" top'
|
||||
bottom' <- process (Set.toList bottom) >>* map (\(_,a,b,c) -> (a,b,c))
|
||||
topIndex <- varIndex mod
|
||||
modIndex <- varIndex mod
|
||||
case onlyConst (Set.toList bottom) of
|
||||
Just bottomConst ->
|
||||
let add_x_plus_my = zipMap plus top'' . zipMap plus (Map.fromList [(topIndex,bottomConst)]) in
|
||||
-- Actually adds n*(x + my)
|
||||
let add_x_plus_my = zipMap plus (Map.map (*n) top'') . zipMap plus (Map.fromList [(modIndex,n * bottomConst)]) in
|
||||
return $
|
||||
-- The zero option (x = 0, x REM y = 0):
|
||||
( map (transformQuad (++ [XZero]) id (++ [top'']) id) m)
|
||||
|
|
@ -713,7 +710,7 @@ makeEquation l t summedItems
|
|||
-- x >= 1
|
||||
[zipMap plus (Map.fromList [(0,-1)]) top''
|
||||
-- m <= 0
|
||||
,Map.fromList [(topIndex,-1)]
|
||||
,Map.fromList [(modIndex,-1)]
|
||||
-- x + my + 1 - |y| <= 0
|
||||
,Map.map negate $ add_x_plus_my $ Map.fromList [(0,1 - bottomConst)]
|
||||
-- x + my >= 0
|
||||
|
|
@ -724,7 +721,7 @@ makeEquation l t summedItems
|
|||
-- x <= -1
|
||||
[add' (0,-1) $ Map.map negate top''
|
||||
-- m >= 0
|
||||
,Map.fromList [(topIndex,1)]
|
||||
,Map.fromList [(modIndex,1)]
|
||||
-- x + my - 1 + |y| >= 0
|
||||
,add_x_plus_my $ Map.fromList [(0,bottomConst - 1)]
|
||||
-- x + my <= 0
|
||||
|
|
@ -736,20 +733,20 @@ makeEquation l t summedItems
|
|||
-- The zero option (x = 0, x REM y = 0):
|
||||
(map (transformQuad (++ [XZero]) id (++ [top'']) id) m)
|
||||
-- The rest:
|
||||
++ twinItems True True (top'', topIndex) bottom''
|
||||
++ twinItems True False (top'', topIndex) bottom''
|
||||
++ twinItems False True (top'', topIndex) bottom''
|
||||
++ twinItems False False (top'', topIndex) bottom''
|
||||
++ twinItems True True n (top'', modIndex) bottom''
|
||||
++ twinItems True False n (top'', modIndex) bottom''
|
||||
++ twinItems False True n (top'', modIndex) bottom''
|
||||
++ twinItems False False n (top'', modIndex) bottom''
|
||||
where
|
||||
-- Each pair for modulo (variable divisor) depending on signs of x and y (in x REM y):
|
||||
twinItems :: Bool -> Bool -> (Map.Map Int Integer,Int) -> Map.Map Int Integer ->
|
||||
twinItems :: Bool -> Bool -> Integer -> (Map.Map Int Integer,Int) -> Map.Map Int Integer ->
|
||||
[([ModuloCase], Map.Map Int Integer,[Map.Map Int Integer], [Map.Map Int Integer])]
|
||||
twinItems xPos yPos (top,topIndex) bottom
|
||||
= (map (transformQuad (++ [findCase xPos yPos False]) (zipMap plus top) id
|
||||
twinItems xPos yPos n (top,modIndex) bottom
|
||||
= (map (transformQuad (++ [findCase xPos yPos False]) (zipMap plus $ Map.map (*n) top) id
|
||||
(++ [xEquation]
|
||||
++ [xLowerBound False]
|
||||
++ [xUpperBound False])) m)
|
||||
++ (map (transformQuad (++ [findCase xPos yPos True]) (zipMap plus top . add' (topIndex,1)) id
|
||||
++ (map (transformQuad (++ [findCase xPos yPos True]) (zipMap plus (Map.map (*n) top) . add' (modIndex, n)) id
|
||||
(++ [xEquation]
|
||||
++ [xLowerBound True]
|
||||
++ [xUpperBound True]
|
||||
|
|
@ -760,12 +757,12 @@ makeEquation l t summedItems
|
|||
-- F T | a - y >= 0
|
||||
-- F F | a + y >= 0
|
||||
-- Therefore the sign of a is (not xPos), the sign of y is (not yPos)
|
||||
++ [add' (topIndex,if xPos then -1 else 1) (signEq (not yPos) bottom)])) m)
|
||||
++ [add' (modIndex,if xPos then -1 else 1) (signEq (not yPos) bottom)])) m)
|
||||
where
|
||||
-- x >= 1 or x <= -1 (rearranged: -1 + x >= 0 or -1 - x >= 0)
|
||||
xEquation = add' (0,-1) (signEq xPos top)
|
||||
-- We include (x [+ a] >= 0 or x [+ a] <= 0) even though they are redundant in some cases (addA = False):
|
||||
xLowerBound addA = signEq xPos $ (if addA then add' (topIndex,1) else id) top
|
||||
xLowerBound addA = signEq xPos $ (if addA then add' (modIndex,1) else id) top
|
||||
-- We want to add the bounds as follows:
|
||||
-- xPos yPos | Equation
|
||||
-- T T | y - 1 - x - a >= 0
|
||||
|
|
@ -773,7 +770,7 @@ makeEquation l t summedItems
|
|||
-- F T | x + a - 1 + y >= 0
|
||||
-- F F | x + a - y - 1 >= 0
|
||||
-- Therefore the sign of y in the equation is yPos, the sign of x and a is (not xPos)
|
||||
xUpperBound addA = add' (0,-1) $ zipMap plus (signEq (not xPos) ((if addA then add' (topIndex,1) else id) top)) (signEq yPos bottom)
|
||||
xUpperBound addA = add' (0,-1) $ zipMap plus (signEq (not xPos) ((if addA then add' (modIndex,1) else id) top)) (signEq yPos bottom)
|
||||
|
||||
signEq sign eq = if sign then eq else Map.map negate eq
|
||||
|
||||
|
|
|
|||
|
|
@ -168,7 +168,7 @@ mylookup x = Map.findWithDefault "unknown" x lookupTable
|
|||
|
||||
lookupTable :: Map.Map CoeffIndex String
|
||||
lookupTable = Map.fromList $ zip [1..] ["i","j","k","m","n","p"]
|
||||
++ [ (n,"x" ++ show n) | n <- [7..100]] -- needed for showing QuickCheck failures
|
||||
++ [ (n,"y_" ++ show n) | n <- [7..100]] -- needed for showing QuickCheck failures
|
||||
|
||||
showInequality :: InequalityConstraintEquation -> String
|
||||
showInequality ineq = "0 <= " ++ zeroIfBlank (showItems ineq)
|
||||
|
|
@ -574,7 +574,7 @@ genConst = do val <- lift $ choose (1, 10)
|
|||
|
||||
genNewExp :: Bool -> StateT VarMap Gen (GenEqItems, [FlattenedExp])
|
||||
genNewExp specialAllowed
|
||||
= do num <- lift $ choose (1,4)
|
||||
= do num <- lift $ oneof $ map return [1,1,1,1,2,2,3] -- bias towards low numbers of items
|
||||
items <- replicateM num $ frequency' [(20, maybeMult genConst), (80, maybeMult $ genNewItem specialAllowed)]
|
||||
return $ fromJust $ foldl join Nothing items
|
||||
where
|
||||
|
|
@ -591,8 +591,8 @@ genNewExp specialAllowed
|
|||
scaleEq :: Integer -> FlattenedExp -> FlattenedExp
|
||||
scaleEq k (Const n) = Const (k * n)
|
||||
scaleEq k (Scale n v) = Scale (k * n) v
|
||||
scaleEq k (Modulo {}) = error "TODO allow scaling of modulo"
|
||||
scaleEq k (Divide {}) = error "TODO allow scaling of divide"
|
||||
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])
|
||||
|
|
@ -602,19 +602,19 @@ generateEquationInput :: Gen ([(((A.Expression,[ModuloCase]), (A.Expression,[Mod
|
|||
generateEquationInput
|
||||
= do ((items, upper),vm) <- flip runStateT Map.empty
|
||||
(do upper <- frequency' [(80, genConst >>* fst), (20, genNewItem False >>* fst)]
|
||||
itemCount <- lift $ choose (1,6)
|
||||
items <- replicateM itemCount (genNewItem True)
|
||||
itemCount <- lift $ choose (1,5)
|
||||
items <- replicateM itemCount (genNewExp True)
|
||||
return (items, upper)
|
||||
)
|
||||
return (makeResults vm items upper, ParItems $ map (\((x,_),_) -> SeqItems [[x]]) items, fst upper)
|
||||
where
|
||||
makeResults :: VarMap ->
|
||||
[(GenEqItems, FlattenedExp)] ->
|
||||
[(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 ->
|
||||
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
|
||||
|
|
@ -631,44 +631,61 @@ generateEquationInput
|
|||
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 m@(Modulo n top bottom) =
|
||||
let topVar = lookupF (Set.findMin top {-TODO-} ) vm
|
||||
botVar = lookupF (Set.findMin bottom {-TODO-} ) vm
|
||||
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 = n**(topVar ++ (abs c)**modVar) in
|
||||
|
||||
[ ([XZero], [(0,0)], [n**topVar === con 0], [])
|
||||
, ([XPos], v, [], [topVar >== con 1, modVar <== con 0] &&& leq [con 0, v, con (abs c - 1)])
|
||||
, ([XNeg], v, [], [topVar <== con (-1), modVar >== con 0] &&& leq [con (1 - abs c), v, con 0])
|
||||
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 = n**(topVar ++ modVar) in
|
||||
[ ([XZero], [(0,0)], [n**topVar === con 0], []) -- TODO stop the divisor being zero
|
||||
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], v, [], [topVar >== con 1, modVar <== (-1)**botVar] &&& leq [con 0, v, botVar ++ con (-1)])
|
||||
, ([XPosYNegANonZero], v, [], [topVar >== con 1, modVar <== botVar] &&& leq [con 0, v, (-1)**botVar ++ con (-1)])
|
||||
, ([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], v, [], [topVar <== con (-1), modVar >== botVar] &&& leq [(-1)**botVar ++ con 1, v, con 0])
|
||||
, ([XNegYNegANonZero], v, [], [topVar <== con (-1), modVar >== (-1)**botVar] &&& leq [botVar ++ con 1, v, con 0])
|
||||
, ([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])
|
||||
]
|
||||
-- TODO add divide here with equations
|
||||
-- (for constant divisor)
|
||||
moduloEq vm exp = [([], lookupF exp vm, [], [])]
|
||||
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)]
|
||||
lookupF f@(Modulo a t b) vm = [(fromJust $ Map.lookup f vm, a)]
|
||||
lookupF f@(Divide a t b) 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)]
|
||||
|
||||
qcTestMakeEquations :: [LabelledQuickCheckTest]
|
||||
qcTestMakeEquations = [("Turning Code Into Equations", scaleQC (100,1000,5000,10000) prop)]
|
||||
qcTestMakeEquations = [("Turning Code Into Equations", scaleQC (20,100,200,400) prop)]
|
||||
where
|
||||
prop :: MakeEquationInput -> QCProp
|
||||
prop (MEI mei) = testMakeEquation mei
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user