some bugfixes

app/Run.hs

@@ -2,6 +2,7 @@
 
 import           System.Environment
 import qualified System.Timeout             as Timeout
+import           Data.Maybe                   (listToMaybe)
 
 import           PWhile.InferEt
 import           Data.PWhile.CostExpression
@@ -13,24 +14,24 @@ main = do
   as <- getArgs
   let ?to = 5
   case as of
-    (fp:_) -> run1 fp
-    _      -> print usage
+    (fp:i:_) -> run1 fp (read i)
+    _        -> print usage
 
   where
     usage = "<file>"
 
-ec :: Program -> IO (Maybe (Result (CExp Rational)))
-ec p = runAny (ect (fst (gen p)) (zero :: CExp Rational))
+ec :: Program -> Int -> IO (Maybe (Result (CExp Rational)))
+ec p i = listToMaybe <$> run (Pick i) (ect (fst (gen p)) zero)
 
 
 
-run1 :: (?to :: Int) => FilePath -> IO ()
-run1 fp = do
+run1 :: (?to :: Int) => FilePath -> Int -> IO ()
+run1 fp i = do
   programM <- fromFile fp
   case programM of
     Left err -> putStrLn (errorBundlePretty err)
     Right p  -> do
-      rM  <- timeout ?to (ec p)
+      rM  <- timeout ?to (ec p i)
       case rM of
         Nothing  -> putStrLn "[Timeout]"
         Just Nothing -> putStrLn "[Unknown]"

pwhile.cabal

@@ -15,7 +15,7 @@ extra-source-files:
 Flag Debug
     Description: Enable debug support
     Manual: True
-    Default: False
+    Default: True
 
 library
   hs-source-dirs: src

src/Data/PWhile/CostExpression.hs

@@ -11,10 +11,13 @@ import qualified Data.PWhile.Expression as E
 data GExp c = GExp BExp (E.Expression c)
   deriving Show
 
-norm :: (Eq c, Num c) => E.Exp -> GExp c
-norm e = GExp (e .>= 0) e' where
+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
+
 plusG :: (Eq c, Num c) => GExp c -> GExp c -> GExp c
 plusG (GExp g1 e1) (GExp g2 e2) = GExp (g1 .&& g2) (e1 + e2)
 
@@ -247,14 +250,17 @@ instance (Eq c, Num c) => E.Substitutable (CExp c) where
 
 instance (PP.Pretty c, Eq c, Num c) => PP.Pretty (CExp c) where
   pretty = pp id where
-    pp _   (E e)        = PP.text "E" PP.<> PP.tupled [PP.pretty e]
-    pp par (Div c e)    = par (infx (pp id c) "/" (PP.pretty e))
-    pp par (Plus c d)   = par (infx (pp PP.parens c) "+" (pp PP.parens d))
-    pp _   (Sup c d)    = PP.text "sup" PP.<> PP.tupled [ pp id c, pp id d ]
+    pp _   (E e)        = ppFun "E" [PP.pretty e]
+    pp _   (Div c e)    = ppFun "div" [ PP.pretty c, PP.pretty e ]
+    pp _   (Plus c d)   = ppFun "plus" [ PP.pretty c, PP.pretty d ]
+    -- pp par (Div c e)    = PP.parens (infx (pp id c) "/" (PP.pretty e))
+    -- pp par (Plus c d)   = PP.parens (infx (pp PP.parens c) "+" (pp PP.parens d))
+    pp _   (Sup c d)    = ppFun "sup" [ pp id c, pp id d ]
     pp _   (Cond g c d)
       | d == zero       = PP.brackets (PP.pretty g) PP.</> PP.parens (PP.pretty c)
       | otherwise       = PP.text "ite" PP.<> PP.tupled [ PP.pretty g, pp id c, pp id d ]
-    infx d1 s d2        = d1 PP.</> PP.text s PP.<+> d2
+    -- infx d1 s d2        = d1 PP.</> PP.text s PP.<+> d2
+    ppFun f ls          = PP.text f PP.<> PP.tupled ls
 
 instance (PP.Pretty c, Eq c, Num c) => PP.Pretty (GExp c) where
   pretty = PP.pretty . fromGExp

src/PWhile/InferEt.hs

@@ -23,6 +23,7 @@ import           Data.Tree                    (Forest)
 import qualified Data.Set                     as S
 import qualified GUBS.Polynomial as P
 
+import           Data.Ratio
 import           ListT                        (ListT)
 import qualified ListT                        as L
 import qualified Text.PrettyPrint.ANSI.Leijen as PP
@@ -161,11 +162,14 @@ rankFromCExp :: C.CExp c -> [C.GExp c]
 rankFromCExp = filter (not . isConst) . C.gExps
   where isConst (C.GExp _ e) = null (E.variables e)
 
+divBy :: CExp -> E.Expression Rational -> CExp
+divBy c (E.Constant r) = C.scale (E.constant (denominator r % numerator r)) c
+divBy c e              = C.divBy c e
 
 discreteExpectation :: [(E.Exp, e)] -> (e -> SolveM CExp) -> SolveM CExp
 discreteExpectation ls f =
-  C.divBy <$> (C.sum <$> sequence [C.scale w <$> f e | (w,e) <- ls'])
-          <*> pure (sum [e | (e,_) <- ls'])
+  divBy <$> (C.sum <$> sequence [C.scale w <$> f e | (w,e) <- ls'])
+        <*> pure (sum [e | (e,_) <- ls'])
   where ls' = [ (fmap fromIntegral w, e) | (w,e) <- ls ]
 
 boundedSum :: (E.Exp -> CExp) -> (E.Exp, E.Exp) -> SolveM CExp
@@ -217,7 +221,7 @@ expectation (E.Rand n) f =
       -- TODO!
         -- | Just g <- linFn fi vi (C.scale (1 / 2) (C.E n)) -> return g
       E.Constant n' -> discreteExpectation [(1,E.constant i) | i <- [0..n'-1]] (return . f)
-      _ | otherwise -> C.divBy <$> boundedSum f (0,n-1) <*> pure (fmap fromIntegral n)
+      _ | otherwise -> divBy <$> boundedSum f (0,n-1) <*> pure (fmap fromIntegral n)
   where
     noccur v e = v `notElem` E.variables e
 
@@ -264,10 +268,10 @@ extractRanking body i c g f = do
   rankFromBExp <-
         (logMsg "optimistic" >> pure (ranksFromBExpWith optimistic))
     <|> (logMsg "shift" >> pure (ranksFromBExpWith shift))
-    -- <|> (logMsg "squared-optimistic" >> pure (squared (ranksFromBExpWith optimistic)))
+    <|> (logMsg "squared-optimistic" >> pure (squared (ranksFromBExpWith optimistic)))
   gRanks <- combine <$> rankFromBExp (i .&& c) <*> pure (rankFromCExp g)
   fRanks <- pure (rankFromCExp f)
-  return (gRanks ++ fRanks) --TODO! frank'
+  return (C.GExp Top 1 : gRanks ++ fRanks) --TODO! frank'
     where
       ranksFromBExpWith sel bexp = mapM sel (S.toList $ literals bexp) where
 
@@ -275,7 +279,7 @@ extractRanking body i c g f = do
       additive = (++)
       multiplicative gs1 gs2 = [C.mulG g1 g2 | g1 <- gs1, g2 <- gs2]
 
-      optimistic (a :>=: b) = pure $ C.norm (a - b + 1)
+      optimistic (a :>=: b) = pure $ C.norm (a .>= b) (a - b + 1)
 
       squared m x = do
         gs <- m x
@@ -286,18 +290,17 @@ extractRanking body i c g f = do
       --   return $ C.Norm $ maxE [ ne | C.Norm ne <- ns ] - e
 
 
-      relaxed (a :>=: b) =
-        case a - b of
-          E.AddConst k _ -> pure (C.norm k)
-          _  -> empty
+      -- relaxed (a :>=: b) =
+      --   case a - b of
+      --     E.AddConst k _ -> pure (C.norm (a .>= b) k)
+      --     _  -> empty
 
       shift (a :>=: b) = do
-        diff <- ubound <$> C.sup n <$> evt body n
+        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 diff == 0 then empty else pure (C.norm (toExp diff))
+        if n - n' == 0 then empty else pure (C.GExp (a .>= b) n')
           where
-            toExp = fmap ceiling
-            n = C.E (fmap fromIntegral (a - b + 1))
+            n = fmap fromIntegral (a - b + 1)
 
             ubound (C.E e) = e
             ubound (C.Div f1 _) = ubound f1
@@ -306,7 +309,8 @@ extractRanking body i c g f = do
             ubound (C.Cond _ f1 f2) = maxE [ubound f1, ubound f2]
 
             maxE [] = 0
-            maxE es = foldl1 (P.zipCoefficientsWith id id max) es
+            maxE es = foldl1 (P.zipCoefficientsWith (max 0) (max 0) max) es
+
 
 isConstantWrt :: CExp -> C -> Bool
 f `isConstantWrt` c = C.variables f `S.disjoint` vs where
@@ -334,10 +338,12 @@ solveInvariant ui =
 data Knd = Evt | Ect deriving (Eq, Ord, Show)
 
 
+
 ect, evt :: C -> CExp -> SolveM CExp
 ect c f =
   logBlkIdM ("[ect] " ++ show (PP.pretty f)) $
   logMsg2 "Problem" c *> etM Ect c f
+
 evt c f =
   logBlkIdM ("[evt] " ++ show (PP.pretty f)) $
   logMsg2 "Problem" c *> etM Evt c f
@@ -358,7 +364,7 @@ et Evt c (C.Plus f1 f2)
 et _   Abort _             = return C.zero
 et _   Skip  f             = return f
 et Evt (Tic _) f           = return f
-et Ect (Tic e) f           = return $ C.fromGExp (C.norm e) `C.plus` f
+et Ect (Tic e) f           = return $ C.fromGExp (C.norm (e .>= 0) e) `C.plus` f
 et _   (Ass v d) f         = expectation d (\ e -> E.substitute v e f)
 et t (NonDet e1 e2) f      = C.sup <$> etM t e1 f <*> etM t e2 f
 et t (Choice ls) f         = discreteExpectation ls (\ c -> etM t c f)

src/PWhile/InvariantSolver/Naive.hs

@@ -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" []
+-- 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"]
 
 -- MS: Optimisation with OptiMathSat (version 1.6.3)
 -- there are two ways to process the output