Merge pull request #72 from bruderj15/publish-70

Publish 70

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

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.

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 #-}
 

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