Merge pull request #122 from bruderj15/develop

Publish v2.8.0

CHANGELOG.md

@@ -6,6 +6,11 @@ file.
 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

hasmtlib.cabal

@@ -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.

src/Language/Hasmtlib/Codec.hs

@@ -137,15 +137,15 @@ instance KnownSMTSort t => Codec (Expr t) where
   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)

src/Language/Hasmtlib/Example/Transcendental.hs

@@ -4,15 +4,14 @@ import Language.Hasmtlib
 
 main :: IO ()
 main = do
-  res <- solveWith @SMT (solver cvc5) $ do
+  res <- solveWith @SMT (solver $ debugging verbosely cvc5) $ do
     setLogic "ALL"
 
     x <- var @RealSort
 
-    assert $ x >? sin 3
+    assert $ 0 === sin x
+    assert $ x >? 0
 
     return x
 
   print res
-
-  return ()

src/Language/Hasmtlib/Internal/Parser.hs

@@ -167,7 +167,7 @@ var = do
 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 @@ negativeValue p = do
   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)

src/Language/Hasmtlib/Internal/Render.hs

@@ -10,6 +10,7 @@ import Language.Hasmtlib.Type.Option
 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
@@ -65,6 +66,14 @@ instance Render Double where
     | 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
   {-# INLINE render #-}

src/Language/Hasmtlib/Type/SMTSort.hs

@@ -44,7 +44,7 @@ data SMTSort =
 -- | 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)