summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorIavorDiatchki <>2018-10-24 22:31:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2018-10-24 22:31:00 (GMT)
commit3d87ddcb0b91ee8fc93ec138d53954262614f576 (patch)
tree6028fa4c431c2bbc1f8f30da07d9ad80c9d9e99a
parentec6529f2ef65b8a367d2b56590e8b03440de5534 (diff)
version 0.9.30.9.3
-rw-r--r--CHANGES2
-rw-r--r--SimpleSMT.hs45
-rw-r--r--simple-smt.cabal2
3 files changed, 43 insertions, 6 deletions
diff --git a/CHANGES b/CHANGES
index a962fd9..a6c4e94 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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
diff --git a/SimpleSMT.hs b/SimpleSMT.hs
index fa685e3..d484ec6 100644
--- a/SimpleSMT.hs
+++ b/SimpleSMT.hs
@@ -14,7 +14,7 @@ module SimpleSMT
-- ** S-Expressions
, SExpr(..)
- , showsSExpr, readSExpr
+ , showsSExpr, ppSExpr, readSExpr
-- ** Logging and Debugging
, Logger(..)
@@ -130,7 +130,7 @@ module SimpleSMT
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.Concurrent(forkIO)
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 @@ showsSExpr ex =
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 @@ bool b = const (if b then "true" else "false")
-- | 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.
--
diff --git a/simple-smt.cabal b/simple-smt.cabal
index 647de0a..d812e9c 100644
--- a/simple-smt.cabal
+++ b/simple-smt.cabal
@@ -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