smart constructors for booleans / integers

[niedjoh]

It would be convenient to have smart constructors for things like (&&) and (+) which directly handle constants. For example, in Language.Hasmtlib.Internal.Expr.Num you could write:

instance Num (Expr IntSort) where
   fromInteger = Constant . IntValue
   {-# INLINE fromInteger #-}
   (Constant (IntValue 0)) + y = y
   x + (Constant (IntValue 0)) = x
   x + y = Plus x y
   {-# INLINE (+) #-}
   x - (Constant (IntValue 0)) = x
   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
   x * y = Mul x y
   {-# INLINE (*) #-}
   negate      = Neg
   {-# INLINE negate #-}
   abs         = Abs
   {-# INLINE abs #-}
   signum x    = ite (x === 0) 0 $ ite (x <? 0) (-1) 1
   {-# INLINE signum #-}

and Language.Hasmtlib.Internal.Expr could look as follows:

instance Boolean (Expr BoolSort) where
  bool = Constant . BoolValue
  {-# INLINE bool #-}
  (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 (&&) #-}
  (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 (Constant (BoolValue x)) = bool . Prelude.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 x y = Xor x y
  {-# INLINE xor #-}

I saw that as of version 2.3 the constructors of Expr are exported, so I can now just write wrappers which implement this functionality, but I think it's still a useful enhancement of the library :)

[bruderj15]

It certainly is! You may drop a PR if you want. Otherwise i will add it very soon. This may actually decrease formula size by quite a lot in some use cases. Thank you!

[bruderj15]

Any specific reason why not for Real and BitVec? I will add them otherwise and publish to hackage.

[niedjoh]

no specific reason - these are just the cases which I need at the moment ^^ It also just occured to me that I forgot to add proper constant folding for the Num instance, e.g.

(Constant (IntValue x))  + (Constant (IntValue y)) = Constant (IntValue (x + y))

and also for the other functions. thanks for your quick reply!

[bruderj15]

Has been published with v2.3.1