simple-smt 0.9.1 → 0.9.3

raw patch · 3 files changed

+43/−6 lines, 3 filesdep ~basePVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: base

API changes (from Hackage documentation)

+ SimpleSMT: ppSExpr :: SExpr -> ShowS

- SimpleSMT: Logger :: (String -> IO ()) -> IO Int -> (Int -> IO ()) -> IO () -> IO () -> Logger

+ SimpleSMT: Logger :: String -> IO () -> IO Int -> Int -> IO () -> IO () -> IO () -> Logger

- SimpleSMT: Solver :: (SExpr -> IO SExpr) -> IO ExitCode -> Solver

+ SimpleSMT: Solver :: SExpr -> IO SExpr -> IO ExitCode -> Solver

Files

CHANGES +2/−0
SimpleSMT.hs +40/−5
simple-smt.cabal +1/−1

CHANGES view

@@ -1,3 +1,5 @@+0.9.3: Fix incorrect rendering or `real` literals+0.9.2: add ppSExpr 0.9:   Support for working with unsat-cores 0.8:   Support for declare; loading of strings/files; more sugar for SMT commands 0.6.0: Allow finer-grained logging

SimpleSMT.hs view

@@ -14,7 +14,7 @@      -- ** S-Expressions   , SExpr(..)-  , showsSExpr, readSExpr+  , showsSExpr, ppSExpr, readSExpr      -- ** Logging and Debugging   , Logger(..)@@ -130,7 +130,7 @@ import Prelude hiding (not, and, or, abs, div, mod, concat, const) import qualified Prelude as P import Data.Char(isSpace)-import Data.List(unfoldr)+import Data.List(unfoldr,intersperse) import Data.Bits(testBit) import Data.IORef(newIORef, atomicModifyIORef, modifyIORef', readIORef,                   writeIORef)@@ -142,7 +142,7 @@ import Control.Monad(forever,when) import Text.Read(readMaybe) import Data.Ratio((%), numerator, denominator)-import Numeric(showHex, readHex)+import Numeric(showHex, readHex, showFFloat)   -- | Results of checking for satisfiability.@@ -173,6 +173,38 @@                 foldr (\e m -> showsSExpr e . showChar ' ' . m)                 (showChar ')') es ++-- | Show an S-expression in a somewhat readbale fashion.+ppSExpr :: SExpr -> ShowS+ppSExpr = go 0+  where+  tab n = showString (replicate n ' ')+  many  = foldr (.) id++  new n e = showChar '\n' . tab n . go n e++  small n es =+    case es of+      [] -> Just []+      e : more+        | n <= 0 -> Nothing+        | otherwise -> case e of+                         Atom x -> (showString x :) <$> small (n-1) more+                         _      -> Nothing++  go :: Int -> SExpr -> ShowS+  go n ex =+    case ex of+      Atom x        -> showString x+      List es+        | Just fs <- small 5 es ->+          showChar '(' . many (intersperse (showChar ' ') fs) . showChar ')'++      List (Atom x : es) -> showString "(" . showString x .+                                many (map (new (n+3)) es) . showString ")"++      List es -> showString "(" . many (map (new (n+2)) es) . showString ")"+ -- | Parse an s-expression. readSExpr :: String -> Maybe (SExpr, String) readSExpr (c : more) | isSpace c = readSExpr more@@ -578,11 +610,14 @@ -- | Integer literals. int :: Integer -> SExpr int x | x < 0     = neg (int (negate x))-         | otherwise = Atom (show x)+      | otherwise = Atom (show x)  -- | Real (well, rational) literals. real :: Rational -> SExpr-real x = realDiv (int (denominator x)) (int (numerator x))+real x+  | toRational y == x = Atom (showFFloat Nothing y "")+  | otherwise = realDiv (int (numerator x)) (int (denominator x))+  where y = fromRational x :: Double  -- | A bit vector represented in binary. --

simple-smt.cabal view

@@ -1,5 +1,5 @@ name:                simple-smt-version:             0.9.1+version:             0.9.3 synopsis:            A simple way to interact with an SMT solver process. description:         A simple way to interact with an SMT solver process. license:             BSD3