Merge pull request #73 from bruderj15/develop

Publish v2.3.1
bruderj15 · Aug 16, 2024 · 4fdab41 · 4fdab41
2 parents e732ffb + 2136891
commit 4fdab41
Show file tree

Hide file tree

Showing 4 changed files with 61 additions and 15 deletions.
diff --git 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
@@ -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
@@ -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
@@ -150,13 +151,20 @@ data Expr (t :: SMTSort) where
 instance Boolean (Expr BoolSort) where
   bool = Constant . BoolValue
   {-# INLINE bool #-}
-  (&&) = And
+  (Constant (BoolValue x)) && y = if x then y else false
+  x && (Constant (BoolValue y)) = if y then x else false
+  x && y = And x y
   {-# INLINE (&&) #-}
-  (||) = Or
+  (Constant (BoolValue x)) || y = if x then true else y
+  x || (Constant (BoolValue y)) = if y then true else x
+  x || y = Or x y
   {-# INLINE (||) #-}
-  not  = Not
+  not (Constant (BoolValue x)) = bool . not $ x
+  not x = Not x
   {-# INLINE not #-}
-  xor  = Xor
+  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 #-}
 
 instance KnownNat n => Boolean (Expr (BvSort n)) where

diff --git a/src/Language/Hasmtlib/Internal/Expr/Num.hs b/src/Language/Hasmtlib/Internal/Expr/Num.hs
@@ -12,11 +12,21 @@ import GHC.TypeNats
 instance Num (Expr IntSort) where
    fromInteger = Constant . IntValue
    {-# INLINE fromInteger #-}
-   (+)         = Plus
+   (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 y     = Plus x (Neg y)
+   x - (Constant (IntValue 0)) = x
+   (Constant (IntValue x)) - (Constant (IntValue y)) = Constant (IntValue (x - y))
+   x - y = Plus x (Neg y)
    {-# INLINE (-) #-}
-   (*)         = Mul
+   (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
    {-# INLINE negate #-}
@@ -28,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 #-}
@@ -44,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 #-}
@@ -58,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