Commit def9c133 authored by AVANZINI Martin's avatar AVANZINI Martin
Browse files

shift heuristic

parent 3d8f8383
......@@ -15,8 +15,8 @@ norm :: (Eq c, Num c) => BExp -> E.Exp -> GExp c
norm g e = GExp g e' where
e' = fmap fromIntegral e
-- fromExp :: (Eq c, Num c) => E.Exp -> CExp c
-- fromExp = E . fmap fromIntegral
fromExp :: (Eq c, Num c) => E.Exp -> CExp c
fromExp = E . fmap fromIntegral
plusG :: (Eq c, Num c) => GExp c -> GExp c -> GExp c
plusG (GExp g1 e1) (GExp g2 e2) = GExp (g1 .&& g2) (e1 + e2)
......@@ -35,6 +35,9 @@ data CExp c =
zero :: (Eq c, Num c) => CExp c
zero = E 0
one :: (Eq c, Num c) => CExp c
one = E 1
plus :: (Eq c, Num c) => CExp c -> CExp c -> CExp c
plus (E 0) c2 = c2
plus c1 (E 0) = c1
......@@ -62,6 +65,9 @@ cond g c d = Cond g c d
guarded :: (Eq c, Num c) => BExp -> CExp c -> CExp c
guarded g c = cond g c zero
pred :: (Eq c, Num c) => BExp -> CExp c
pred g = cond g one zero
divBy :: (Eq c, Num c) => CExp c -> E.Expression c -> CExp c
divBy c 1 = c
divBy (Div c e) f = Div c (e * f)
......
......@@ -269,14 +269,14 @@ extractRanking body i c g f = do
(logMsg "optimistic" >> pure (ranksFromBExpWith optimistic))
-- MS: not a solution, but shift is not working as intended
-- before we could compare norms; now we have reduced expression
<|> (logMsg "optimistic2" >> pure (ranksFromBExpWith (optimistic' 2)))
<|> (logMsg "optimistic4" >> pure (ranksFromBExpWith (optimistic' 4)))
<|> (logMsg "optimistic8" >> pure (ranksFromBExpWith (optimistic' 8)))
-- <|> (logMsg "optimistic2" >> pure (ranksFromBExpWith (optimistic' 2)))
-- <|> (logMsg "optimistic4" >> pure (ranksFromBExpWith (optimistic' 4)))
-- <|> (logMsg "optimistic8" >> pure (ranksFromBExpWith (optimistic' 8)))
<|> (logMsg "shift" >> pure (ranksFromBExpWith shift))
<|> (logMsg "squared-optimistic" >> pure (squared (ranksFromBExpWith optimistic)))
gRanks <- combine <$> rankFromBExp (i .&& c) <*> pure (rankFromCExp g)
fRanks <- pure (rankFromCExp f)
return (C.GExp Top 1 : gRanks ++ fRanks) --TODO! frank'
return (C.GExp Top 1 : gRanks ++ fRanks) -- ++ fRanks'
where
ranksFromBExpWith sel bexp = mapM sel (S.toList $ literals bexp) where
......@@ -301,22 +301,32 @@ extractRanking body i c g f = do
-- E.AddConst k _ -> pure (C.norm (a .>= b) k)
-- _ -> empty
shift (a :>=: b) = do
n' <- debugM "diff" =<< (ubound <$> (debugM "diffSub" =<< (C.sup (C.E n) <$> evt body (C.E n))))
-- TODO, macht das sinn or if n - evt body n > 0 besser...
if n - n' == 0 then empty else pure (C.GExp (a .>= b) n')
shift l@(a :>=: b) = do
mkNorm <$> maxE <$> concatMap diffs <$> C.gExps <$> evt body (C.pred (a .>= b))
where
n = fmap fromIntegral (a - b + 1)
ubound (C.E e) = e
ubound (C.Div f1 _) = ubound f1
ubound (C.Plus f1 f2) = ubound f1 + ubound f2
ubound (C.Sup f1 f2) = maxE [ubound f1, ubound f2]
ubound (C.Cond _ f1 f2) = maxE [ubound f1, ubound f2]
maxE [] = 0
maxE es = foldl1 (P.zipCoefficientsWith (max 0) (max 0) max) es
diffs (C.GExp gd e)
| e /= 0 = [ (a' - b') - (a - b) | a' :>=: b' <- S.toList (literals gd) ]
| otherwise = []
mkNorm (E.AddConst _ df) = C.norm (e .>= 0) e
where e = a - b + 1 + (E.constant df)
-- n' <- debugM "diff" =<< (ubound <$> (debugM "diffSub" =<< (C.sup (C.E n) <$> evt body (C.E n))))
-- -- TODO, macht das sinn or if n - evt body n > 0 besser...
-- if n - n' == 0 then empty else pure (C.GExp (a .>= b) n')
-- where
-- n = fmap fromIntegral (a - b + 1)
-- ubound (C.E e) = e
-- ubound (C.Div f1 _) = ubound f1
-- ubound (C.Plus f1 f2) = ubound f1 + ubound f2
-- ubound (C.Sup f1 f2) = maxE [ubound f1, ubound f2]
-- ubound (C.Cond _ f1 f2) = maxE [ubound f1, ubound f2]
isConstantWrt :: CExp -> C -> Bool
f `isConstantWrt` c = C.variables f `S.disjoint` vs where
......
......@@ -33,9 +33,9 @@ type SmtFormula = SMT.SMTFormula SMT.SMTLib2
type SmtExpression = SMT.SMTExpression SMT.SMTLib2
runSmtM :: SmtM a -> a
-- runSmtM = unsafePerformIO . SMT.runSMTLib2 "z3" ["-smt2", "-in"]
runSmtM = unsafePerformIO . SMT.runSMTLib2Using "QF_LIRA" "yices-smt2" ["--incremental"]
-- runSmtM = unsafePerformIO . SMT.runSMTLib2 "yices-smt2" ["&2>/tmp/yices.err"]
runSmtM = unsafePerformIO . SMT.runSMTLib2 "z3" ["-smt2", "-in"]
-- runSmtM = unsafePerformIO . SMT.runSMTLib2Using "QF_LIRA" "yices-smt2" ["--incremental"]
-- runSmtM = unsafePerformIO . SMT.runSMTLib2 "yices-smt2" []
-- MS: Optimisation with OptiMathSat (version 1.6.3)
-- there are two ways to process the output
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment