diff --git a/CHANGELOG.md b/CHANGELOG.md index dfaed67..f975869 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.3.1 _(2024-08-16)_ + +### Changed +- Instances for `Boolean`, `Num` & `Fractional` on `Expr` now use smart constructors + ## v2.3.0 _(2024-08-12)_ ### Added diff --git a/hasmtlib.cabal b/hasmtlib.cabal index 114eb9e..7999de0 100644 --- a/hasmtlib.cabal +++ b/hasmtlib.cabal @@ -1,7 +1,7 @@ cabal-version: 3.0 name: hasmtlib -version: 2.3.0 +version: 2.3.1 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/Internal/Expr.hs b/src/Language/Hasmtlib/Internal/Expr.hs index 13bc8ac..eb12ea4 100644 --- a/src/Language/Hasmtlib/Internal/Expr.hs +++ b/src/Language/Hasmtlib/Internal/Expr.hs @@ -4,6 +4,7 @@ module Language.Hasmtlib.Internal.Expr where +import Prelude hiding (not) import Language.Hasmtlib.Internal.Render import Language.Hasmtlib.Type.ArrayMap import Language.Hasmtlib.Type.SMTSort @@ -158,11 +159,11 @@ instance Boolean (Expr BoolSort) where x || (Constant (BoolValue y)) = if y then true else x x || y = Or x y {-# INLINE (||) #-} - not (Constant (BoolValue x)) = bool . Prelude.not $ x + not (Constant (BoolValue x)) = bool . not $ x not x = Not x {-# INLINE not #-} - xor (Constant (BoolValue x)) y = if x then Language.Hasmtlib.Boolean.not y else y - xor x (Constant (BoolValue y)) = if y then Language.Hasmtlib.Boolean.not x else x + xor (Constant (BoolValue x)) y = if x then not y else y + xor x (Constant (BoolValue y)) = if y then not x else x xor x y = Xor x y {-# INLINE xor #-} diff --git a/src/Language/Hasmtlib/Internal/Expr/Num.hs b/src/Language/Hasmtlib/Internal/Expr/Num.hs index 87bbdd9..6ae39d9 100644 --- a/src/Language/Hasmtlib/Internal/Expr/Num.hs +++ b/src/Language/Hasmtlib/Internal/Expr/Num.hs @@ -14,15 +14,18 @@ instance Num (Expr IntSort) where {-# INLINE fromInteger #-} (Constant (IntValue 0)) + y = y x + (Constant (IntValue 0)) = x + (Constant (IntValue x)) + (Constant (IntValue y)) = Constant (IntValue (x + y)) x + y = Plus x y {-# INLINE (+) #-} x - (Constant (IntValue 0)) = x + (Constant (IntValue x)) - (Constant (IntValue y)) = Constant (IntValue (x - y)) x - y = Plus x (Neg y) {-# INLINE (-) #-} (Constant (IntValue 0)) * _ = 0 _ * (Constant (IntValue 0)) = 0 (Constant (IntValue 1)) * y = y x * (Constant (IntValue 1)) = x + (Constant (IntValue x)) * (Constant (IntValue y)) = Constant (IntValue (x * y)) x * y = Mul x y {-# INLINE (*) #-} negate = Neg @@ -35,11 +38,21 @@ instance Num (Expr IntSort) where instance Num (Expr RealSort) where fromInteger = Constant . RealValue . fromIntegral {-# INLINE fromInteger #-} - (+) = Plus + (Constant (RealValue 0)) + y = y + x + (Constant (RealValue 0)) = x + (Constant (RealValue x)) + (Constant (RealValue y)) = Constant (RealValue (x + y)) + x + y = Plus x y {-# INLINE (+) #-} - x - y = Plus x (Neg y) + x - (Constant (RealValue 0)) = x + (Constant (RealValue x)) - (Constant (RealValue y)) = Constant (RealValue (x - y)) + x - y = Plus x (Neg y) {-# INLINE (-) #-} - (*) = Mul + (Constant (RealValue 0)) * _ = 0 + _ * (Constant (RealValue 0)) = 0 + (Constant (RealValue 1)) * y = y + x * (Constant (RealValue 1)) = x + (Constant (RealValue x)) * (Constant (RealValue y)) = Constant (RealValue (x * y)) + x * y = Mul x y {-# INLINE (*) #-} negate = Neg {-# INLINE negate #-} @@ -51,11 +64,21 @@ instance Num (Expr RealSort) where instance KnownNat n => Num (Expr (BvSort n)) where fromInteger = Constant . BvValue . fromInteger {-# INLINE fromInteger #-} - (+) = BvAdd + (Constant (BvValue 0)) + y = y + x + (Constant (BvValue 0)) = x + (Constant (BvValue x)) + (Constant (BvValue y)) = Constant (BvValue (x + y)) + x + y = BvAdd x y {-# INLINE (+) #-} - (-) = BvSub + x - (Constant (BvValue 0)) = x + (Constant (BvValue x)) - (Constant (BvValue y)) = Constant (BvValue (x - y)) + x - y = BvSub x y {-# INLINE (-) #-} - (*) = BvMul + (Constant (BvValue 0)) * _ = 0 + _ * (Constant (BvValue 0)) = 0 + (Constant (BvValue 1)) * y = y + x * (Constant (BvValue 1)) = x + (Constant (BvValue x)) * (Constant (BvValue y)) = Constant (BvValue (x * y)) + x * y = BvMul x y {-# INLINE (*) #-} abs = id {-# INLINE abs #-} @@ -65,7 +88,10 @@ instance KnownNat n => Num (Expr (BvSort n)) where instance Fractional (Expr RealSort) where fromRational = Constant . RealValue . fromRational {-# INLINE fromRational #-} - (/) = Div + x / (Constant (RealValue 1)) = x + (Constant (RealValue 0)) / _ = 0 + (Constant (RealValue x)) / (Constant (RealValue y)) = Constant (RealValue (x / y)) + x / y = Div x y {-# INLINE (/) #-} instance Floating (Expr RealSort) where