fixed parser of bernoulli distribution

app/Run.hs

@@ -12,7 +12,7 @@ import           PWhile.Parser
 main :: IO ()
 main = do
   as <- getArgs
-  let ?to = 5
+  let ?to = 60
   case as of
     [fp] -> run1 fp Nothing
     (fp:i:_) -> run1 fp (Just (read i))

src/PWhile/InvariantSolver/Naive.hs

@@ -243,6 +243,8 @@ data Constraint e = GEQ Context e e
 
 assertEntailSmt :: Int -> DNF SmtLit -> SmtLit -> SmtM ()
 assertEntailSmt i (Disj cs) p = forM_ cs $ \c -> SMT.assert =<< handelman i c p
+-- assertEntailSmt i ctx@(Disj cs) p = forM_ (conjs (d ctx)) $ \c -> SMT.assert =<< handelman i c p
+--   where d cs = debug (show (PP.pretty cs PP.<> PP.text "|-" PP.<> PP.pretty p)) cs
 
 assertConstraintSmt :: Int -> Constraint SmtPoly -> SmtM ()
 assertConstraintSmt i (GEQ g l r) = assertEntailSmt i g (l `geqLit` r)
@@ -330,8 +332,8 @@ reduce (GEQ c (toFrac -> (lhs,f1)) (toFrac -> (rhs,f2))) = do
 debug :: PP.Pretty e => String -> e -> e
 debug = debugMsg "SmtSolver"
 
--- debugPA :: (Applicative f, PP.Pretty msg, PP.Pretty e) => msg -> e -> f e
--- debugPA = debugMsgA "SmtSolver" . renderPretty
+debugPA :: (Applicative f, PP.Pretty msg, PP.Pretty e) => msg -> e -> f e
+debugPA = debugMsgA "SmtSolver" . renderPretty
 
 upperInvariant :: NaiveSolver -> UpperInvariant -> SmtM (Maybe CExp)
 upperInvariant s UpperInvariant{..} = do

src/PWhile/Parser.hs

@@ -199,7 +199,7 @@ pUnif v = do
 pBer :: Exp -> Parser Program
 pBer v = do
   (a,b) <- symbol "ber" *> pTuple integer
-  return $ (v .~) $ bernoulli (1,1) (E.constant a) (E.constant b)
+  return $ (v .~) $ bernoulli (a, b-1) (fromIntegral 1) (fromIntegral 0)
 
 pHyper :: Exp -> Parser Program
 pHyper v = do