Merge pull request #88 from bruderj15/develop

Publish v2.6.0

CHANGELOG.md

@@ -6,6 +6,20 @@ 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.6.0 _(2024-08-27)_
+
+### Added
+- Support for signed BitVec operations.
+- Added constructor `Rem` for `Expr t`.
+
+### Changed
+- *(breaking change)* Enhanced the type of `BvSort Nat` to `BvSort BvEnc Nat` where `BvEnc = Unsigned | Signed`.
+  Before, the API only allowed unsigned BitVec, therefore `BvSort n` now becomes `BvSort Unsigned n`.
+  The promoted type `BvEnc` is phantom and only used for differentiating instances for `Num`, ...
+- Moved `Language.Hasmtlib.Internal.Bitvec` to `Language.Hasmtlib.Type.Bitvec`, exported API with `Language.Hasmtlib`
+- Removed constructors `StrLT` and `StrLTHE` from `Expr t`.
+- Fixed wrong implementation of Num for `Bitvec`. `(+)`, `(-)` and `(*)` had invalid definitions.
+
 ## v2.5.1 _(2024-08-26)_
 
 ### Added

README.md

@@ -17,7 +17,7 @@ For instance, to define the addition of two `V3` containing Real-SMT-Expressions
 v3Add :: V3 (Expr RealSort) -> V3 (Expr RealSort) -> V3 (Expr RealSort)
 v3Add = liftA2 (+)
 ```
-Even better, the [Expr-GADT](https://github.com/bruderj15/Hasmtlib/blob/master/src/Language/Hasmtlib/Internal/Expr.hs) allows a polymorph definition:
+Even better, the [Expr-GADT](https://github.com/bruderj15/Hasmtlib/blob/master/src/Language/Hasmtlib/Type/Expr.hs) allows a polymorph definition:
 ```haskell
 v3Add :: Num (Expr t) => V3 (Expr t) -> V3 (Expr t) -> V3 (Expr t)
 v3Add = liftA2 (+)
@@ -63,38 +63,35 @@ May print: `(Sat,Just (V3 (-2.0) (-1.0) 0.0,V3 (-2.0) (-1.0) 0.0))`
         BoolSort
       | IntSort
       | RealSort
-      | BvSort Nat
+      | BvSort BvEnc Nat
       | ArraySort SMTSort SMTSort
       | StringSort
     data Expr (t :: SMTSort) where ...
 
     ite :: Expr BoolSort -> Expr t -> Expr t -> Expr t
   ```
-- [x] Full SMTLib 2.6 standard support for Sorts Int, Real, Bool, unsigned BitVec, Array & String
-- [x] Type-level length-indexed Bitvectors for BitVec
+- [x] Full SMTLib 2.6 standard support for Sorts Bool, Int, Real, BitVec, Array & String
+- [x] Type-level length-indexed Bitvectors with type-level encoding (Signed/Unsigned) for BitVec
   ```haskell
-    bvConcat :: (KnownNat n, KnownNat m) => Expr (BvSort n) -> Expr (BvSort m) -> Expr (BvSort (n + m))
+  bvConcat :: (KnownNat n, KnownNat m) => Expr (BvSort enc n) -> Expr (BvSort enc m) -> Expr (BvSort enc (n + m))
+  bvLShR :: KnownNat n => Expr (BvSort Unsigned n) -> Expr (BvSort enc n) -> Expr (BvSort Unsigned n)
+  bvAShR :: KnownNat n => Expr (BvSort Signed n) -> Expr (BvSort enc n) -> Expr (BvSort Signed n)
   ```
-- [x] Pure API with Expression-instances for Num, Floating, Bounded, ...
+- [x] Pure API with plenty common instances: `Num`, `Floating`, `Bounded`, `Bits`, `Ixed` and many more
   ```haskell
     solveWith @SMT (solver yices) $ do
       setLogic "QF_BV"
-      x <- var @(BvSort 16)
-      y <- var
-      assert $ x - (maxBound `mod` 8) === y * y
-      return (x,y)
+      x <- var @(BvSort Signed 16)
+      let f = x >? 42 && (x `div` 84 === maxBound - 100)
+      assert f
+      return x
   ```
 - [x] Add your own solvers via the [Solver type](https://github.com/bruderj15/Hasmtlib/blob/master/src/Language/Hasmtlib/Type/Solution.hs)
   ```haskell
     -- | Function that turns a state (usually SMT or OMT) into a result and a solution
     type Solver s m = s -> m (Result, Solution)
   ```
 - [x] Solvers via external processes: CVC5, Z3, Yices2-SMT, MathSAT, OptiMathSAT, OpenSMT & Bitwuzla
-  ```haskell
-    (result, solution) <- solveWith @SMT (solver mathsat) $ do
-      setLogic "QF_LIA"
-      assert $ ...
-  ```
 - [x] Incremental solving
   ```haskell
       cvc5Living <- interactiveSolver cvc5

hasmtlib.cabal

@@ -1,7 +1,7 @@
 cabal-version:         3.0
 
 name:                  hasmtlib
-version:               2.5.1
+version:               2.6.0
 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.
@@ -33,7 +33,6 @@ library
                      , Language.Hasmtlib.Variable
                      , Language.Hasmtlib.Counting
                      , Language.Hasmtlib.Internal.Parser
-                     , Language.Hasmtlib.Internal.Bitvec
                      , Language.Hasmtlib.Internal.Render
                      , Language.Hasmtlib.Internal.Sharing
                      , Language.Hasmtlib.Internal.Uniplate1
@@ -56,6 +55,7 @@ library
                      , Language.Hasmtlib.Type.Solver
                      , Language.Hasmtlib.Type.Option
                      , Language.Hasmtlib.Type.ArrayMap
+                     , Language.Hasmtlib.Type.Bitvec
 
   build-depends:       attoparsec                   >= 0.14.4 && < 1
                      , base                         >= 4.17.2 && < 5

src/Language/Hasmtlib.hs

@@ -11,6 +11,7 @@ module Language.Hasmtlib
   , module Language.Hasmtlib.Type.SMTSort
   , module Language.Hasmtlib.Type.Solution
   , module Language.Hasmtlib.Type.ArrayMap
+  , module Language.Hasmtlib.Type.Bitvec
   , module Language.Hasmtlib.Boolean
   , module Language.Hasmtlib.Codec
   , module Language.Hasmtlib.Counting
@@ -37,6 +38,7 @@ import Language.Hasmtlib.Type.Option
 import Language.Hasmtlib.Type.SMTSort
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Type.ArrayMap
+import Language.Hasmtlib.Type.Bitvec
 import Language.Hasmtlib.Boolean
 import Language.Hasmtlib.Codec
 import Language.Hasmtlib.Counting

src/Language/Hasmtlib/Codec.hs

@@ -6,13 +6,15 @@
 module Language.Hasmtlib.Codec where
 
 import Prelude hiding (not, (&&), (||), all, and)
-import Language.Hasmtlib.Internal.Bitvec
-import Language.Hasmtlib.Type.Expr (Expr(..), SMTVar(..), unwrapValue, wrapValue)
+import Language.Hasmtlib.Type.Bitvec
+import Language.Hasmtlib.Type.Expr (Expr(..), SMTVar(..))
 import Language.Hasmtlib.Type.Solution
 import Language.Hasmtlib.Type.ArrayMap
 import Language.Hasmtlib.Type.SMTSort
+import Language.Hasmtlib.Type.Value
 import Language.Hasmtlib.Boolean
 import Data.Kind
+import Data.Proxy
 import Data.Coerce
 import qualified Data.List as List
 import Data.Bits hiding (And, Xor, xor)
@@ -23,9 +25,9 @@ import Data.Dependent.Map as DMap
 import Data.Tree (Tree)
 import qualified Data.Text as Text
 import Data.Monoid (Sum, Product, First, Last, Dual)
-import Data.Functor.Identity (Identity)
 import qualified Data.Vector.Sized as V
 import Control.Monad
+import Control.Lens hiding (from, to)
 import GHC.Generics
 import GHC.TypeLits
 
@@ -70,7 +72,14 @@ class Codec a where
 instance KnownSMTSort t => Codec (Expr t) where
   type Decoded (Expr t) = HaskellType t
   decode sol (Var var)  = do
-    (IntValueMap m) <- DMap.lookup (sortSing @t) sol
+    let sungSort = sortSing @t
+    (IntValueMap m) <- case sungSort of
+      SBvSort enc n -> case bvEncSing' enc of
+      -- Solution contains all BV as unsigned, if we have a Signed one we check the Unsigned ones and flip BvEnc
+        SUnsigned -> DMap.lookup sungSort sol
+        SSigned -> DMap.lookup (SBvSort (Proxy @Unsigned) n) sol <&>
+          \case (IntValueMap ubvs) -> IntValueMap $ fmap (\case (BvValue ubv) -> BvValue $ asSigned ubv) ubvs
+      _ -> DMap.lookup sungSort sol
     val <- IM.lookup (coerce var) m
     return $ unwrapValue val
   decode _ (Constant v)         = Just $ unwrapValue v
@@ -80,6 +89,7 @@ instance KnownSMTSort t => Codec (Expr t) where
   decode sol (Mul x y)          = (*)   <$> decode sol x <*> decode sol y
   decode sol (Abs x)            = fmap abs     (decode sol x)
   decode sol (Mod x y)          = mod   <$> decode sol x <*> decode sol y
+  decode sol (Rem x y)          = rem   <$> decode sol x <*> decode sol y
   decode sol (IDiv x y)         = div   <$> decode sol x <*> decode sol y
   decode sol (Div x y)          = (/)   <$> decode sol x <*> decode sol y
   decode sol (LTH x y)          = (<)   <$> decode sol x <*> decode sol y
@@ -115,17 +125,25 @@ instance KnownSMTSort t => Codec (Expr t) where
   decode sol (Ite p t f)        = (\p' t' f' -> if p' then t' else f') <$> decode sol p <*> decode sol t <*> decode sol f
   decode sol (BvNand x y)       = nand <$> sequenceA [decode sol x, decode sol y]
   decode sol (BvNor x y)        = nor  <$> sequenceA [decode sol x, decode sol y]
-  decode sol (BvShL x y)        = join $ bvShL <$> decode sol x <*> decode sol y
-  decode sol (BvLShR x y)       = join $ bvLShR <$> decode sol x <*> decode sol y
-  decode sol (BvConcat x y)     = bvConcat <$> decode sol x <*> decode sol y
+  decode sol (BvShL x y)        = do
+    x' <- decode sol x
+    y' <- decode sol y
+    return $ shiftL x' $ fromIntegral (toInteger y')
+  decode sol (BvLShR x y)       = do
+    x' <- decode sol x
+    y' <- decode sol y
+    return $ shiftR x' $ fromIntegral (toInteger y')
+  decode sol (BvAShR x y)       = do
+    x' <- decode sol x
+    y' <- decode sol y
+    return $ shiftR x' $ fromIntegral (toInteger y')
+  decode sol (BvConcat x y)     = bitvecConcat <$> decode sol x <*> decode sol y
   decode sol (BvRotL i x)       = rotateL <$> decode sol x <*> pure (fromIntegral i)
   decode sol (BvRotR i x)       = rotateR <$> decode sol x <*> pure (fromIntegral i)
   decode sol (ArrSelect i arr)  = arrSelect <$> decode sol i <*> decode sol arr
   decode sol (ArrStore i x arr) = arrStore <$> decode sol i <*> decode sol x <*> decode sol arr
   decode sol (StrConcat x y)         = (<>) <$> decode sol x <*> decode sol y
   decode sol (StrLength x)           = toInteger . Text.length <$> decode sol x
-  decode sol (StrLT x y)             = (<) <$> decode sol x <*> decode sol y
-  decode sol (StrLTHE x y)           = (<=) <$> decode sol x <*> decode sol y
   decode sol (StrAt x i)             = (\x' i' -> Text.singleton $ Text.index x' (fromInteger i')) <$> decode sol x <*> decode sol i
   decode sol (StrSubstring x i j)    = (\x' (fromInteger -> i') (fromInteger -> j') -> Text.take (j' - i') $ Text.drop i' x') <$> decode sol x <*> decode sol i <*> decode sol j
   decode sol (StrPrefixOf x y)       = Text.isPrefixOf <$> decode sol x <*> decode sol y

src/Language/Hasmtlib/Example/Bitvector.hs

@@ -9,9 +9,9 @@ main = do
   res <- solveWith @SMT (debug bitwuzla def) $ do
     setLogic "QF_BV"
 
-    x <- var @(BvSort 8)
+    x <- var @(BvSort Unsigned 8)
 
-    assert $ x === clearBit (maxBound `div` 2) 2
+    assert $ x === clearBit (maxBound `div` 2) 1
 
     return x
 

src/Language/Hasmtlib/Example/Quantifier.hs

@@ -9,7 +9,7 @@ main = do
   res <- solveWith @SMT (debug cvc5 def) $ do
     setLogic "BV"
 
-    z <- var @(BvSort 8)
+    z <- var @(BvSort Signed 8)
 
     assert $ z === 0