yices 0.0.0.10 → 0.0.0.11

raw patch · 4 files changed

+24/−6 lines, 4 filesPVP: minor bump suggested

API additions: PVP suggests at least a minor version bump

API changes (from Hackage documentation)

Files

• ChangeLog +9/−0
• Math/SMT/Yices/Parser.hs +10/−1
• Math/SMT/Yices/Pipe.hs +4/−4
• yices.cabal +1/−1

@@ -1,3 +1,12 @@+2011-09-21 Scott West scott.west@inf.ethz.ch+	* Math/SMT/Yices/Parser.hs, Math/SMT/Yices/Pipe.hs: fixed a bug when+	an item of the the yices output satisfying model gets pretty printed+	into multiple lines rather than one line.++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-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

@@ -15,7 +15,7 @@    See <http://yices.csl.sri.com/language.shtml> for details.  -} module Math.SMT.Yices.Parser (- typY, expY, cmdY, parseTypY, parseExpY, parseCmdY+ typY, expY, cmdY, parseTypY, parseExpY, parseExpYs, parseCmdY  ) where  import Math.SMT.Yices.Syntax@@ -34,6 +34,12 @@ parseExpY :: String -> ExpY parseExpY s = case parse expY "parseExpY" s of Right r -> r                                                Left msg -> error $ show msg++-- | parse a string of many yices expressions+parseExpYs :: String -> [ExpY]+parseExpYs s = case parse expYs "parseExpYs" s of Right r -> r+                                                  Left msg -> error $ show msg+  -- | parse a string of yices command format parseCmdY :: String -> CmdY parseCmdY s = case parse cmdY "parseCmdY" s of Right r -> r@@ -130,6 +136,9 @@ -- | parsec parser for yices expressions expY :: GenParser Char st ExpY expY = try litb <|> try litr <|> liti <|> vare <|> paren expYinParen++expYs :: GenParser Char st [ExpY]+expYs = many expY  expYinParen = and_ <|> or_ <|> not_ <|> try (=>:) <|> (=:) <|> (/=:)           <|> try (<:) <|> (<=:) <|> try (>:) <|> (>=:)

@@ -75,8 +75,8 @@      -- hPutStrLn stderr s -- for debugging      return $        case s of-         "sat"    -> Sat (map parseExpY ss)-         "unknown"-> Unknown (map parseExpY ss)+         "sat"    -> Sat (parseExpYs $ unlines ss)+         "unknown"-> Unknown (parseExpYs $ unlines ss)          "unsat"  -> UnSat (map read.words.tail.dropWhile (/=':').head $ ss)          _        -> InCon (s:ss) @@ -95,8 +95,8 @@      when (not $ null err) $ hPutStrLn stderr err      return $        case lines out of-         "sat"     : ss -> Sat     (map parseExpY $ filter (not.null) ss)-         "unknown" : ss -> Unknown (map parseExpY $ filter (not.null) ss)+         "sat"     : ss -> Sat     (parseExpYs $ unlines $ filter (not.null) ss)+         "unknown" : ss -> Unknown (parseExpYs $ unlines $ filter (not.null) ss)          "unsat"   : ss -> UnSat   (map read.words.tail.dropWhile (/=':').head $ ss)          other          -> InCon   other 

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