hasmtlib 2.7.2 → 2.8.0

raw patch · 6 files changed

+34/−20 lines, 6 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +5/−0
• hasmtlib.cabal +1/−1
• src/Language/Hasmtlib/Codec.hs +9/−9
• src/Language/Hasmtlib/Internal/Parser.hs +9/−9
• src/Language/Hasmtlib/Internal/Render.hs +9/−0
• src/Language/Hasmtlib/Type/SMTSort.hs +1/−1

@@ -6,6 +6,11 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [PVP versioning](https://pvp.haskell.org/). +## v2.8.0 _(2024-11-28)_++### Changed+- Replaced representation of `RealSort` values in Haskell with `Rational` instead of `Double`+ ## v2.7.2 _(2024-11-27)_  ### Added

@@ -1,7 +1,7 @@ cabal-version:         3.0  name:                  hasmtlib-version:               2.7.2+version:               2.8.0 synopsis:              A monad for interfacing with external SMT solvers description:           Hasmtlib is a library for generating SMTLib2-problems using a monad.   It takes care of encoding your problem, marshaling the data to an external solver and parsing and interpreting the result into Haskell types.

@@ -137,15 +137,15 @@   decode sol (Or x y)           = (||) <$> decode sol x <*> decode sol y   decode sol (Impl x y)         = (==>) <$> decode sol x <*> decode sol y   decode sol (Xor x y)          = xor   <$> decode sol x <*> decode sol y-  decode _ Pi                   = Just pi-  decode sol (Sqrt x)           = fmap sqrt  (decode sol x)-  decode sol (Exp x)            = fmap exp   (decode sol x)-  decode sol (Sin x)            = fmap sin   (decode sol x)-  decode sol (Cos x)            = fmap cos   (decode sol x)-  decode sol (Tan x)            = fmap tan   (decode sol x)-  decode sol (Asin x)           = fmap asin  (decode sol x)-  decode sol (Acos x)           = fmap acos  (decode sol x)-  decode sol (Atan x)           = fmap atan  (decode sol x)+  decode _ Pi                   = Just $ toRational pi+  decode sol (Sqrt x)           = fmap (toRational . sqrt . fromRational @Double)  (decode sol x)+  decode sol (Exp x)            = fmap (toRational . exp . fromRational @Double)   (decode sol x)+  decode sol (Sin x)            = fmap (toRational . sin . fromRational @Double)   (decode sol x)+  decode sol (Cos x)            = fmap (toRational . cos . fromRational @Double)   (decode sol x)+  decode sol (Tan x)            = fmap (toRational . tan . fromRational @Double)   (decode sol x)+  decode sol (Asin x)           = fmap (toRational . asin . fromRational @Double)  (decode sol x)+  decode sol (Acos x)           = fmap (toRational . acos . fromRational @Double)  (decode sol x)+  decode sol (Atan x)           = fmap (toRational . atan . fromRational @Double)  (decode sol x)   decode sol (ToReal x)         = fmap realToFrac (decode sol x)   decode sol (ToInt x)          = fmap truncate   (decode sol x)   decode sol (IsInt x)          = fmap ((0 ==) . snd . properFraction) (decode sol x)

@@ -167,7 +167,7 @@ constant :: forall t. KnownSMTSort t => Parser (HaskellType t) constant = case sortSing @t of   SIntSort       -> anyValue decimal-  SRealSort      -> anyValue parseRatioDouble <|> parseToRealDouble <|> anyValue rational+  SRealSort      -> anyValue parseRational <|> parseToRealRational <|> anyValue rational   SBoolSort      -> parseBool   SBvSort _ p    -> anyBitvector p   SArraySort k v -> constArray k v@@ -288,25 +288,25 @@   return $ negate val {-# INLINE negativeValue #-} -parseRatioDouble :: Parser Double-parseRatioDouble = do+parseRational :: Parser Rational+parseRational = do   _           <- char '(' >> skipSpace >> char '/' >> skipSpace   numerator   <- decimal   _           <- skipSpace   denominator <- decimal   _           <- skipSpace >> char ')' -  return $ fromRational $ numerator % denominator-{-# INLINEABLE parseRatioDouble #-}+  return $ numerator % denominator+{-# INLINEABLE parseRational #-} -parseToRealDouble :: Parser Double-parseToRealDouble = do+parseToRealRational :: Parser Rational+parseToRealRational = do   _   <- char '(' >> skipSpace >> string "to_real" >> skipSpace   dec <- anyValue decimal   _   <- skipSpace >> char ')' -  return $ fromInteger dec-{-# INLINEABLE parseToRealDouble #-}+  return $ toRational dec+{-# INLINEABLE parseToRealRational #-}  parseBool :: Parser Bool parseBool = (string "true" *> pure True) <|> (string "false" *> pure False)

@@ -10,6 +10,7 @@ import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Bitvec import Language.Hasmtlib.Type.ArrayMap+import Data.Ratio import Data.Coerce import Data.Some.Constraint import Data.Sequence@@ -64,6 +65,14 @@     | x < 0     = "(- " <> formatDouble standardDefaultPrecision (abs x) <> ")"     | otherwise = formatDouble standardDefaultPrecision x   {-# INLINE render #-}++instance Render Rational where+  render x = if num < 0+             then "(/ " <> "(- " <> render (abs num) <> ") " <> render denom <> ")"+             else "(/ " <> render num <> " " <> render denom <> ")"+    where+      num = numerator x+      denom = denominator x  instance Render Char where   render = char8

@@ -44,7 +44,7 @@ -- | Injective type-family that computes the Haskell 'Type' of an 'SMTSort'. type family HaskellType (t :: SMTSort) = (r :: Type) | r -> t where   HaskellType IntSort         = Integer-  HaskellType RealSort        = Double+  HaskellType RealSort        = Rational   HaskellType BoolSort        = Bool   HaskellType (BvSort enc n)  = Bitvec enc n   HaskellType (ArraySort k v) = ConstArray (HaskellType k) (HaskellType v)