cexp simplifications and extended heuristics

src/Data/PWhile/CostExpression.hs

@@ -53,11 +53,14 @@ data CExp c =
 -- fromExp :: (Eq c, Num c) => E.Exp -> CExp c
 -- fromExp = E . fmap fromIntegral
 
+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
+
 traverseCoeff :: (Num c', Ord c', Applicative f) => (c -> f c') -> CExp c -> f (CExp c')
 traverseCoeff f = walk where
-  walk (N k n)      = nm <$> f k where
-    nm 0 = zero
-    nm k' = N k' n
+  walk (N k n)      = nm <$> f k <*> pure n where
   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
@@ -79,7 +82,10 @@ plus :: (Eq c, Num c, Ord 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   = N k1 (n1 `plusN` n2)
+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
@@ -216,5 +222,8 @@ gNorms = walk B.Top 1 where
   walk b k (Sup c d)    = walk b k c ++ walk b k d
   walk b k (Cond g c d) = walk (b .&& g) k c ++ walk (b .&& neg g) k d
 
+norms :: (Eq c, Num c) => CExp c -> S.Set Norm
+norms c = S.fromList [n | GNorm _ _ n <- gNorms c]
+
 instance (PP.Pretty c, Eq c, Ord c, Num c) => PP.Pretty (GNorm c) where
   pretty = PP.pretty . fromGNorm

src/PWhile/InferEt.hs

@@ -268,7 +268,9 @@ extractRanking body i c g f = do
     <|> (logMsg "squared-optimistic" >> pure (squared (ranksFromBExpWith optimistic)))
   gRanks <- combine rankFromBExp (c .&& i) (varGNorms g)
   fRanks <- pure (sum (fromGNorm `map` C.gNorms f))
-  return (toNormList (norm 1 + fRanks + gRanks)) --  ++ fRanks'
+  fRanks' <- (*) <$> rankFromBExp c
+                 <*> P.fromPolynomialM (fmap P.variable . delta) (pure . P.coefficient) 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]
@@ -276,7 +278,8 @@ extractRanking body i c g f = do
       norm e = P.variable (C.Norm (e .>= 0) e)
       fromGNorm (C.GNorm _ _ n) = P.variable n
 
-      ranksFromBExpWith sel bexp = sum <$> mapM sel (S.toList (literals bexp))
+      maxE [] = 0
+      maxE es = foldl1 (P.zipCoefficientsWith (max 0) (max 0) max) es
 
       additive fromBExp b gexps =
         (+) (sum (fromGNorm `map` gexps))
@@ -287,22 +290,22 @@ extractRanking body i c g f = do
             <*> (sum <$> sequence [ (*) (P.variable n) <$> fromBExp (b .&& b')
                                   | C.GNorm b' _ n <- gexps])
 
+
+      ranksFromBExpWith sel bexp = sum <$> mapM sel (S.toList (literals bexp))
+
       optimistic (a :>=: b) = pure $ norm (a - b + 1)
-      -- optimistic' i (a :>=: b) = pure $ guarded (a .>= b) (a - b + i)
 
       squared m x = sq <$> m x where sq n = n * n
 
-      -- delta (C.Norm e) = do
-      --   ns <- S.toList <$> C.norms <$> evt body (C.fromNorm (C.norm e) :: C.NormPoly Rational)
-      --   return $ C.Norm $ maxE [ ne | C.Norm ne <- ns ] - e
+      delta n@(C.Norm _ e) = do
+        ns <- S.toList <$> C.norms <$> evt body (C.nm 1 n)
+        let f = maxE [ ne | C.Norm _ ne <- ns ] - e
+        return (C.norm (f .>= 0) f)
 
-      shift l@(a :>=: b) = do
+      shift l@(a :>=: b) =
         -- TODO: this is a mess; maybe define wp for non-recursive language?
         mkNorm <$> maxE <$> concatMap diffs <$> C.gNorms <$> evt body (C.pred (a .>= b))
           where
-            maxE [] = 0
-            maxE es = foldl1 (P.zipCoefficientsWith (max 0) (max 0) max) es
-
             diffs (C.GNorm gd _ n)
               | not (C.isZeroN n)  = [ (a' - b') - (a - b) | a' :>=: b' <- S.toList (literals gd) ]
               | otherwise          = []

src/PWhile/InvariantSolver/Naive.hs

@@ -31,8 +31,8 @@ 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 "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)