yices 0.0.0.6 → 0.0.0.7

raw patch · 5 files changed

+14/−4 lines, 5 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• ChangeLog +8/−0
• Main.hs +1/−0
• Math/SMT/Yices/Parser.hs +1/−1
• Math/SMT/Yices/Pipe.hs +3/−2
• yices.cabal +1/−1

@@ -1,3 +1,11 @@+2010-02-04 Ahn, Ki Yung kya@pdx.edu+	* Math/SMT/Yices/Parser.hs: fixed a bug in the parser which was not+	parsing fractional literals properly++2010-01-20 Tom Howkins tomahawkins@gmail.com+	* Math/SMT/Yices/Pipe.hs (quickCheckY'): filter out carriage return+	character to make it work for windows+ 2010-01-01 José Iborra pepeiborra@gmail.com 	* Math/SMT/Yices/Syntax.hs: Avoided quadratic complexity in the pretty 	printer and fixed a bug in the pretty printer

@@ -5,6 +5,7 @@ -- example of generating three test cases of 6 integer variables -- l1, u1, i, l2, u2, j sush that l1 < i <= u1 and l2 < j <= u2. +import Math.SMT.Yices.Parser import Math.SMT.Yices.Syntax import Math.SMT.Yices.Pipe import List

@@ -129,7 +129,7 @@  -- | parsec parser for yices expressions expY :: GenParser Char st ExpY-expY = litb <|> liti <|> litr <|> vare <|> paren expYinParen+expY = litb <|> try litr <|> liti <|> vare <|> paren expYinParen  expYinParen = and_ <|> or_ <|> not_ <|> try (=>:) <|> (=:) <|> (/=:)           <|> try (<:) <|> (<=:) <|> try (>:) <|> (>=:)

@@ -72,7 +72,7 @@ checkY yp@(_, Just hout, _, _) =   do runCmdsY yp [ECHO('\n':_BEGIN_OUTPUT), CHECK, ECHO('\n':_END_OUTPUT)]      (s:ss) <- hGetOutLines hout-     hPutStrLn stderr s+     -- hPutStrLn stderr s -- for debugging      return $        case s of          "sat"    -> Sat (map parseExpY ss)@@ -90,7 +90,8 @@ --   It can be useful if you intend to  quickCheckY' :: String -> [String] -> [CmdY] -> IO ResY quickCheckY' yPath yOpts cmds = do-     (code, out, err) <- readProcessWithExitCode yPath ("-e" : yOpts) (unlines $ map show cmds)+     (code, out', err) <- readProcessWithExitCode yPath ("-e" : yOpts) (unlines $ map show cmds)+     let out = filter (/= '\r') out'      when (not $ null err) $ hPutStrLn stderr err      return $        case lines out of

@@ -1,5 +1,5 @@ name:                yices-version:             0.0.0.6+version:             0.0.0.7 synopsis:            Haskell programming interface to Yices SMT solver description:         Incomplete (no bitvectors) syntax, parser, and inter                      process communication to Yices from Haskell through pipe.