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

more simplifications when dividing/scaling

parent a1a9ed33
{-# LANGUAGE ConstraintKinds #-}
module Data.PWhile.CostExpression where
import Data.Ratio
import Data.Functor.Identity (runIdentity)
import qualified Text.PrettyPrint.ANSI.Leijen as PP
import qualified Data.Set as S
......@@ -9,6 +12,9 @@ import qualified Data.PWhile.BoolExpression as B
import qualified Data.PWhile.Expression as E
-- norms
----------------------------------------------------------------------
data Norm = Norm BExp E.Exp
deriving (Eq, Ord, Read, Show)
......@@ -41,6 +47,16 @@ isZeroN (Norm _ e) = e == 0
isConstN :: Norm -> Bool
isConstN (Norm _ e) = null (E.variables e)
-- cost expressions
----------------------------------------------------------------------
class FromRatio c where fromRatio :: Rational -> c
type Coeff c = (Eq c, Num c, Ord c, FromRatio c)
instance FromRatio Rational where fromRatio = id
data CExp c =
N c Norm
| Div (CExp c) E.Exp
......@@ -56,36 +72,35 @@ data CExp c =
nm :: (Eq c, Num c) => c -> Norm -> CExp c
nm 0 _ = zero
nm c (Norm _ (E.Constant i)) = N (c * fromIntegral i) (norm Top 1)
nm c n = N c n
nm c (Norm b e) = N (c * fromIntegral k) (norm b e')
where (k,e') = E.cfactor e
traverseCoeff :: (Num c', Ord c', Applicative f) => (c -> f c') -> CExp c -> f (CExp c')
traverseCoeff :: (Coeff c', Applicative f) => (c -> f c') -> CExp c -> f (CExp c')
traverseCoeff f = walk where
walk (N k n) = nm <$> f k <*> pure n where
walk (N k n) = nm <$> f k <*> pure n
walk (Div c e) = divBy <$> walk c <*> pure e
walk (Plus c d) = plus <$> walk c <*> walk d
walk (Sup c d) = sup <$> walk c <*> walk d
walk (Cond b c d) = cond <$> pure b <*> walk c <*> walk d
mapCoeff :: (Num c', Ord c') => (c -> c') -> CExp c -> CExp c'
mapCoeff :: Coeff c' => (c -> c') -> CExp c -> CExp c'
mapCoeff f = runIdentity . traverseCoeff (pure . f)
fromNorm :: Num c => Norm -> CExp c
fromNorm = N 1
zero :: (Eq c, Num c) => CExp c
zero :: (Num c) => CExp c
zero = N 1 (Norm Top 0)
one :: (Eq c, Num c) => CExp c
one :: (Num c) => CExp c
one = N 1 (Norm Top 1)
plus :: (Eq c, Num c, Ord c) => CExp c -> CExp c -> CExp c
plus :: Coeff c => CExp c -> CExp c -> CExp c
plus (Cond g c1 c2) (Cond g' c1' c2')
| g == g' = Cond g (c1 `plus` c1') (c2 `plus` c2')
plus (Div c1 e1) (Div c2 e2) | e1 == e2 = (c1 `plus` c2) `divBy` e1
plus (N k1 n1) (N k2 n2) | k1 == k2 = nm k1 (n1 `plusN` n2)
| n1 == n2 = nm (k1 + k2) n1
-- plus (N k1 (Norm _ (E.Constant i1))) (N k2 (Norm _ (E.Constant i2)))
-- = nm (k1 * fromIntegral i1 + k1 * fromIntegral i2) oneN
plus c1 c2 | c1 == zero = c2
| c2 == zero = c1
| otherwise = Plus c1 c2
......@@ -93,7 +108,7 @@ plus c1 c2 | c1 == zero = c2
ramp :: Num c => E.Exp -> CExp c
ramp e = N 1 (norm (e .>= 0) e)
sum :: (Eq c, Num c, Ord c) => [CExp c] -> CExp c
sum :: Coeff c => [CExp c] -> CExp c
sum = foldl plus zero
sup :: (Eq c, Num c) => CExp c -> CExp c -> CExp c
......@@ -120,24 +135,12 @@ oneV = N 1 (Norm Top "@@ONE@@")
pred :: (Eq c, Num c) => BExp -> CExp c
pred g = cond g oneV zero
divBy :: (Eq c, Ord c, Num c) => CExp c -> E.Exp -> CExp c
divBy c _
| c == zero = zero
divBy c 1 = c
divBy (Div c e) f = Div c (e * f)
divBy c f = Div c f
-- simplify :: (Eq c, Ord c, Num c) => CExp c -> CExp c
-- simplify (E e) = E (E.norm e)
-- simplify (Coeff k c)
-- | k == 0 = zero
-- | otherwise = Coeff k (simplify c)
-- simplify (Div c e) = simplify c `divBy` E.norm e
-- simplify (Plus c d) = simplify c `plus` simplify d
-- simplify (Sup c d) = simplify c `sup` simplify d
-- simplify (Cond g c d) = cond g (simplify c) (simplify d)
scale :: (Eq c, Ord c, Num c) => E.Exp -> CExp c -> CExp c
-- class RatioFactor a where rfactor :: a -> (Rational, a)
-- instance RatioFactor Rational where rfactor r = (r,1)
-- instance RatioFactor Int where rfactor i = (fromIntegral i,1)
scale :: Coeff c => E.Exp -> CExp c -> CExp c
scale 0 _ = zero
scale 1 c = c
scale (E.Constant k) c = scaleC (fromIntegral k) c
......@@ -147,15 +150,20 @@ scale e (Plus d1 d2) = scale e d1 `plus` scale e d2
scale e (Sup d1 d2) = scale e d1 `sup` scale e d2
scale e (Cond g d1 d2) = cond g (scale e d1) (scale e d2)
scaleC :: (Eq c, Ord c, Num c) => c -> CExp c -> CExp c
scaleC :: Coeff c => c -> CExp c -> CExp c
scaleC 0 _ = zero
scaleC 1 c = c
scaleC k c = mapCoeff (*k) c
-- toExp :: (Eq c, Num c) => CExp c -> Maybe (E.Expression c)
-- toExp (E f) = Just f
-- toExp (Plus d1 d2) = (+) <$> toExp d1 <*> toExp d2
-- toExp _ = Nothing
scaleC k c = mapCoeff (* k) c
divBy :: Coeff c => CExp c -> E.Exp -> CExp c
divBy c _ | c == zero = zero
divBy c 1 = c
divBy (Div c e) f = c `divBy` (e * f)
divBy c f | f' == 1 = c'
| otherwise = Div c' f'
where
(k,f') = E.cfactor f
c' = scaleC (fromRatio (1 % fromIntegral k)) c
variables :: CExp c -> S.Set E.Var
variables (N _ (Norm _ e)) = E.variables e
......@@ -167,7 +175,7 @@ variables (Cond g c d) = B.variables g `S.union` variables c `S.union` varia
instance E.Substitutable Norm where
substitute s e (Norm g f) = norm (E.substitute s e g) (E.substitute s e f)
instance (Eq c, Ord c, Num c) => E.Substitutable (CExp c) where
instance Coeff c => E.Substitutable (CExp c) where
substitute s e (N k n) = N k (E.substitute s e n)
substitute s e (Div c f) = E.substitute s e c `divBy` E.substitute s e f
substitute s e (Plus c d) = E.substitute s e c `plus` E.substitute s e d
......
......@@ -12,6 +12,7 @@ module Data.PWhile.Expression
, constant
, variables
, factor
, cfactor
, P.norm
, Substitutable (..)
-- distributions
......@@ -24,6 +25,7 @@ where
import qualified Data.Set as S
import Data.Data
import Data.String
import Data.List (foldl1')
import qualified GUBS.Polynomial as P
import qualified Text.PrettyPrint.ANSI.Leijen as PP
......@@ -46,18 +48,21 @@ variable = P.variable
variables :: Expression c -> S.Set Var
variables = S.fromList . P.variables
-- factor :: (Eq c, Num c) => Expression c -> Expression c -> (Expression c, (Expression c, Expression c))
-- factor e1 e2 =
-- case P.factoriseMono [e1,e2] of
-- Just (m,[e1',e2']) -> (P.fromMono m, (e1',e2'))
-- _ -> (1,(e1,e2))
factor :: Exp -> Exp -> (Exp, (Exp, Exp))
factor e1 e2 =
case P.factorise [P.norm e1,P.norm e2] of
Just ((c,m),[e1',e2']) -> (P.coefficient c * P.fromMono m, (e1',e2'))
_ -> (1,(e1,e2))
cfactor :: Exp -> (Int, Exp)
cfactor e = case monos of
[] -> (1,e)
[(c,m)] -> (c, P.fromMonos [(1,m)])
_ -> (f, P.fromMonos [(c `div` f, m) | (c,m) <- monos ])
where
monos = P.toMonos e
f = foldl1' gcd [ c | (c,_) <- monos]
-- patterns
const_ :: (Ord v, Eq c, Num c) => P.Polynomial v c -> Maybe c
......
......@@ -270,7 +270,7 @@ extractRanking body i c g f = do
fRanks <- pure (sum (fromGNorm `map` C.gNorms f))
fRanks' <- (*) <$> rankFromBExp c
<*> P.fromPolynomialM (fmap P.variable . delta) (pure . P.coefficient) fRanks
return (toNormList (norm 1 + fRanks + gRanks + fRanks'))
return (toNormList (norm 1 + fRanks + gRanks + fRanks')) --
where
toNormList p = filter (not . zeroN) [ C.prodN [ C.expN n i | (n,i) <- P.toPowers m ]
| (_,m) <- P.toMonos p]
......
......@@ -88,7 +88,7 @@ freshACoeff = bounded (Just 0) Nothing freshReal
type SmtPoly = P.Polynomial E.Var SmtExpression
data SmtLit = Geq0 SmtPoly | TT | FF deriving (Eq, Ord, Show) -- TODO: remove TT,FF?
data SmtLit = Geq0 SmtPoly | TT | FF deriving (Eq, Ord, Show)
instance {-# OVERLAPPING #-} PP.Pretty SmtPoly where
pretty = P.ppPoly PP.pretty (PP.parens . PP.pretty)
......@@ -145,7 +145,6 @@ _ .&! Bot = Bot
Bot .&! _ = Bot
Top .&! g = g
g .&! Top = g
-- TQDO: better?
Disj cs .&! dnf2 = walk (S.toList cs) where
walk [c1] = bigOr [litsSet c1 `cand` litsSet c2 | c2 <- conjs dnf2]
walk (c:cs') = disj [c] .&! dnf2 .|| disj cs' .&! dnf2
......@@ -188,6 +187,9 @@ fromBExp bexp = bigOr [ bigAnd' [ literal (fromBLit l) | l <- lits c ]
type CExp = C.CExp Rational
type AExp = C.CExp SmtExpression
instance C.FromRatio SmtExpression where
fromRatio = P.coefficient . fromRational
decode :: AExp -> SmtM CExp
decode = C.traverseCoeff decodeCoeff where
decodeCoeff = fmap SMT.ratio . P.evalWithM SMT.getValue
......@@ -195,13 +197,6 @@ decode = C.traverseCoeff decodeCoeff where
encode :: CExp -> AExp
encode = C.mapCoeff acoeff
-- encodeExp :: E.Expression Rational -> E.Expression SmtExpression
-- encodeExp = fmap acoeff
-- encodeBExp :: BExp Rational -> BExp SmtExpression
-- encodeBExp = mapLiterals (\ (l :>=: r) -> encodeExp l :>=: encodeExp r)
-- implication elimination
----------------------------------------------------------------------
......@@ -266,16 +261,10 @@ entailsSmtK i p c k =
-- TODO: add syntactic checks and possibly assert
ent = assertEntailSmt i
applyTemplate :: (Num c, Ord c, Eq c) => [c] -> [C.CExp c] -> C.CExp c
applyTemplate qs cs = C.sum (zipWith C.scaleC qs cs)
-- elimination of cost expression
----------------------------------------------------------------------
-- toFrac :: AExp -> (AExp, Exp)
toFrac :: (Eq c, Ord c, Num c) => C.CExp c -> (C.CExp c, E.Exp)
toFrac :: C.Coeff c => C.CExp c -> (C.CExp c, E.Exp)
toFrac c@C.N{} = (c,1)
toFrac (C.Div c e) = (d,e*f) where
(d,f) = toFrac c
......@@ -357,6 +346,9 @@ upperInvariant s UpperInvariant{..} = do
-- checkWithOptSolver qs s
(\ i -> assertConstraintSmt i `mapM_` cs)
(\ _ -> C.guarded inv <$> decode f)
where
applyTemplate qs cs = C.sum (zipWith C.scaleC qs cs)
instance InvariantSolver NaiveSolver where
entails s (fromBExp -> dnf) (fromBLit -> c) =
......
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