hasmtlib 2.3.0 → 2.3.1

raw patch · 4 files changed

+61/−15 lines, 4 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.md +5/−0
• hasmtlib.cabal +1/−1
• src/Language/Hasmtlib/Internal/Expr.hs +12/−4
• src/Language/Hasmtlib/Internal/Expr/Num.hs +43/−10

@@ -6,6 +6,11 @@ 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

@@ -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.

@@ -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 @@ 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

@@ -12,11 +12,21 @@ 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 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 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 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