From 83f6b25b8ef8c35965c3b862ed43eb9a46e33b60 Mon Sep 17 00:00:00 2001
From: Johannes Niederhauser <johannes.niederhauser@uibk.ac.at>
Date: Fri, 16 Aug 2024 10:26:27 +0200
Subject: [PATCH] smart constructors for Int/Bool expressions

---
 src/Language/Hasmtlib/Internal/Expr.hs     | 15 +++++++++++----
 src/Language/Hasmtlib/Internal/Expr/Num.hs | 13 ++++++++++---
 2 files changed, 21 insertions(+), 7 deletions(-)

diff --git a/src/Language/Hasmtlib/Internal/Expr.hs b/src/Language/Hasmtlib/Internal/Expr.hs
index a4932f9..13bc8ac 100644
--- a/src/Language/Hasmtlib/Internal/Expr.hs
+++ b/src/Language/Hasmtlib/Internal/Expr.hs
@@ -150,13 +150,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 . Prelude.not $ x
+  not x = Not x
   {-# INLINE not #-}
-  xor  = Xor
+  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 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
index 871f454..87bbdd9 100644
--- a/src/Language/Hasmtlib/Internal/Expr/Num.hs
+++ b/src/Language/Hasmtlib/Internal/Expr/Num.hs
@@ -12,11 +12,18 @@ import GHC.TypeNats
 instance Num (Expr IntSort) where
    fromInteger = Constant . IntValue
    {-# INLINE fromInteger #-}
-   (+)         = Plus
+   (Constant (IntValue 0)) + y = y
+   x + (Constant (IntValue 0)) = x
+   x + y = Plus x y
    {-# INLINE (+) #-}
-   (-) x y     = Plus x (Neg y)
+   x - (Constant (IntValue 0)) = x
+   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
+   x * y = Mul x y
    {-# INLINE (*) #-}
    negate      = Neg
    {-# INLINE negate #-}