smart constructors for Int/Bool expressions

bruderj15 · Aug 16, 2024 · 83f6b25 · 83f6b25
1 parent e732ffb
commit 83f6b25
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 7 deletions.
diff --git 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
@@ -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 #-}