diff --git a/CHANGELOG.md b/CHANGELOG.md index fb272fb..a2fbef0 100644 --- a/CHANGELOG.md +++ b/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 diff --git a/hasmtlib.cabal b/hasmtlib.cabal index a6d8e23..fed6fd9 100644 --- a/hasmtlib.cabal +++ b/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. diff --git a/src/Language/Hasmtlib/Codec.hs b/src/Language/Hasmtlib/Codec.hs index e3d62d9..914c0ea 100644 --- a/src/Language/Hasmtlib/Codec.hs +++ b/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) diff --git a/src/Language/Hasmtlib/Example/Transcendental.hs b/src/Language/Hasmtlib/Example/Transcendental.hs index 281458b..5e196bd 100644 --- a/src/Language/Hasmtlib/Example/Transcendental.hs +++ b/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 () diff --git a/src/Language/Hasmtlib/Internal/Parser.hs b/src/Language/Hasmtlib/Internal/Parser.hs index 0e8bf8c..eacd489 100644 --- a/src/Language/Hasmtlib/Internal/Parser.hs +++ b/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) diff --git a/src/Language/Hasmtlib/Internal/Render.hs b/src/Language/Hasmtlib/Internal/Render.hs index 20ef819..850c3e9 100644 --- a/src/Language/Hasmtlib/Internal/Render.hs +++ b/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 #-} diff --git a/src/Language/Hasmtlib/Type/SMTSort.hs b/src/Language/Hasmtlib/Type/SMTSort.hs index 20fc878..a3c6b7c 100644 --- a/src/Language/Hasmtlib/Type/SMTSort.hs +++ b/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)