hasmtlib 2.5.1 → 2.6.0

raw patch · 12 files changed

+452/−424 lines, 12 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +14/−0
• README.md +12/−15
• hasmtlib.cabal +2/−2
• src/Language/Hasmtlib.hs +2/−0
• src/Language/Hasmtlib/Codec.hs +27/−9
• src/Language/Hasmtlib/Internal/Bitvec.hs +0/−124
• src/Language/Hasmtlib/Internal/Parser.hs +19/−15
• src/Language/Hasmtlib/Internal/Sharing.hs +2/−3
• src/Language/Hasmtlib/Type/Bitvec.hs +150/−0
• src/Language/Hasmtlib/Type/Expr.hs +160/−239
• src/Language/Hasmtlib/Type/SMTSort.hs +16/−11
• src/Language/Hasmtlib/Type/Value.hs +48/−6

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

@@ -17,7 +17,7 @@ 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,26 +63,28 @@         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@@ -90,11 +92,6 @@     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

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

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

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

@@ -1,124 +0,0 @@-{-# LANGUAGE DerivingStrategies #-}-{-# LANGUAGE ViewPatterns #-}--module Language.Hasmtlib.Internal.Bitvec where--import Prelude hiding ((&&), (||), not)-import Language.Hasmtlib.Boolean-import Language.Hasmtlib.Internal.Render-import Data.ByteString.Builder-import Data.Bit-import Data.Bits-import Data.Coerce-import Data.Finite hiding (shift)-import Data.Proxy-import Data.Ratio ((%))-import Data.Bifunctor-import qualified Data.Vector.Unboxed.Sized as V-import GHC.TypeNats---- | Unsigned and length-indexed bitvector with MSB first.-newtype Bitvec (n :: Nat) = Bitvec { unBitvec :: V.Vector n Bit }-  deriving newtype (Eq, Ord, Boolean)--instance KnownNat n => Bits (Bitvec n) where-  (.&.) = (&&)-  (.|.) = (||)-  xor = Language.Hasmtlib.Boolean.xor-  complement = not-  shift bv i  = coerce $ shift (coerce @_ @(V.Vector n Bit) bv) (negate i)-  rotate bv i = coerce $ rotate (coerce @_ @(V.Vector n Bit) bv) (negate i)-  bitSize _ = fromIntegral $ natVal (Proxy @n)-  bitSizeMaybe _ = Just $ fromIntegral $ natVal (Proxy @n)-  isSigned _ = false-  testBit bv = testBit (V.reverse (coerce @_ @(V.Vector n Bit) bv))-  bit (toInteger -> i) = coerce $ V.reverse $ V.replicate @n (Bit False) V.// [(finite i, Bit True)]-  popCount = coerce . popCount . coerce @_ @(V.Vector n Bit)--instance Show (Bitvec n) where-  show = V.toList . V.map (\b -> if coerce b then '1' else '0') . coerce @_ @(V.Vector n Bit)--instance Render (Bitvec n) where-  render = stringUtf8 . show-  {-# INLINEABLE render #-}--instance KnownNat n => Num (Bitvec n) where-   fromInteger x = coerce . V.reverse $ V.generate @n (coerce . testBit x . fromInteger . getFinite)-   negate        = id-   abs           = id-   signum _      = 0-   (coerce -> x) + (coerce -> y) = coerce @(V.Vector n Bit) $ x + y-   (coerce -> x) - (coerce -> y) = coerce @(V.Vector n Bit) $ x - y-   (coerce -> x) * (coerce -> y) = coerce @(V.Vector n Bit) $ x * y--instance KnownNat n => Bounded (Bitvec n) where-  minBound = coerce $ V.replicate @n false-  maxBound = coerce $ V.replicate @n true--instance KnownNat n => Enum (Bitvec n) where-  succ x   = x + 1-  pred x   = x - 1-  toEnum   = fromInteger . toInteger-  fromEnum = V.sum . V.imap (\i b -> if coerce b then 2 ^ getFinite i else 0) . V.reverse . coerce @_ @(V.Vector n Bit)--instance KnownNat n => Real (Bitvec n) where-  toRational x = toInteger (fromEnum x) % 1--instance KnownNat n => Integral (Bitvec n) where-  toInteger = fromIntegral . fromEnum-  quotRem x y = bimap fromInteger fromInteger $ quotRem (toInteger x) (toInteger y)--bvReverse :: Bitvec n -> Bitvec n-bvReverse = coerce . V.reverse . coerce--bvReplicate :: forall n. KnownNat n => Bit -> Bitvec n-bvReplicate = coerce . V.replicate @n--bvReplicate' :: forall n proxy. KnownNat n => proxy n -> Bit -> Bitvec n-bvReplicate' _ = bvReplicate--bvGenerate :: forall n. KnownNat n => (Finite n -> Bit) -> Bitvec n-bvGenerate = coerce . V.generate @n . coerce--bvConcat :: Bitvec n -> Bitvec m -> Bitvec (n + m)-bvConcat (coerce -> x) (coerce -> y) = coerce $ x V.++ y--bvTake' :: forall n m proxy . KnownNat n => proxy n -> Bitvec (n+m) -> Bitvec n-bvTake' p = coerce . V.take' p . coerce--bvDrop' :: forall n m proxy . KnownNat n => proxy n -> Bitvec (n+m) -> Bitvec m-bvDrop' p = coerce . V.drop' p . coerce--bvSplitAt' :: forall n m proxy. KnownNat n => proxy n -> Bitvec (n+m) -> (Bitvec n, Bitvec m)-bvSplitAt' p = coerce . V.splitAt' p . coerce--bvToList :: Bitvec n -> [Bit]-bvToList = V.toList . coerce--bvFromListN :: forall n. KnownNat n => [Bit] -> Maybe (Bitvec n)-bvFromListN = coerce . V.fromListN @n--bvFromListN' :: forall n. KnownNat n => Proxy n -> [Bit] -> Maybe (Bitvec n)-bvFromListN' _ = bvFromListN--bvShL :: KnownNat n => Bitvec n -> Bitvec n -> Maybe (Bitvec n)-bvShL x y = bvFromListN $ (++ replicate i false) $ drop i $ bvToList x-  where-    i = fromIntegral y--bvLShR :: KnownNat n => Bitvec n -> Bitvec n -> Maybe (Bitvec n)-bvLShR x y = fmap bvReverse $ bvFromListN $ (++ replicate i false) $ drop i $ bvToList $ bvReverse x-  where-    i = fromIntegral y--bvZeroExtend :: KnownNat i => Proxy i -> Bitvec n -> Bitvec (n+i)-bvZeroExtend p x = bvConcat x $ bvReplicate' p false--bvExtract :: forall n i j.-  ( KnownNat i, KnownNat ((j - i) + 1)-  , (i+(n-i)) ~ n-  , (((j - i) + 1) + ((n - i)-((j - i) + 1))) ~ (n - i)-  ) => Proxy i -> Proxy j -> Bitvec n -> Bitvec (( j - i ) + 1)-bvExtract pri _ x = bvTake' @_ @((n-i)-((j-i)+1)) (Proxy @((j-i)+1)) x'-  where-    x' :: Bitvec (n-i) = bvDrop' pri x

@@ -4,10 +4,10 @@ module Language.Hasmtlib.Internal.Parser where  import Prelude hiding (not, (&&), (||), and , or)-import Language.Hasmtlib.Internal.Bitvec import Language.Hasmtlib.Internal.Render import Language.Hasmtlib.Boolean import Language.Hasmtlib.Codec+import Language.Hasmtlib.Type.Bitvec import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Solution import Language.Hasmtlib.Type.ArrayMap@@ -16,7 +16,7 @@ import Data.Coerce import Data.Proxy import Data.Ratio ((%))-import Data.ByteString+import Data.ByteString hiding (filter, foldl) import Data.ByteString.Builder import Data.Attoparsec.ByteString hiding (Result, skipWhile, takeTill) import Data.Attoparsec.ByteString.Char8 hiding (Result)@@ -91,7 +91,10 @@   n <- decimal   _ <- skipSpace >> char ')'   case someNatVal $ fromInteger n of-    SomeNat pn -> return $ SomeSMTSort $ SBvSort pn+    -- SMTLib does not differentiate between signed and unsigned BitVec on the type-level+    -- We do. So we always just put Unsigned here and in Codec (Expr t)+    -- if (t ~ BvSort Signed _) we retrieve unsigned solution and flip type-level encoding+    SomeNat pn -> return $ SomeSMTSort $ SBvSort (Proxy @Unsigned) pn {-# INLINEABLE parseSomeBitVecSort #-}  parseSomeArraySort :: Parser (SomeKnownOrdSMTSort SSMTSort)@@ -140,12 +143,13 @@                       <|> binary "str.prefixof" strPrefixOf <|> binary "str.suffixof" strSuffixOf                       <|> binary "str.contains" strContains                       -- TODO: Add compare ops for all (?) bv-sorts-              SBvSort _ -> unary "bvnot" not+              SBvSort enc _ -> unary "bvnot" not                       <|> binary "bvand" (&&)  <|> binary "bvor" (||) <|> binary "bvxor" xor <|> binary "bvnand" BvNand <|> binary "bvnor" BvNor                       <|> unary  "bvneg" negate                       <|> binary "bvadd" (+)  <|> binary "bvsub" (-) <|> binary "bvmul" (*)                       <|> binary "bvudiv" div <|> binary "bvurem" rem-                      <|> binary "bvshl" BvShL <|> binary "bvlshr" BvLShR+                      <|> binary "bvshl" BvShL+                      <|> case bvEncSing' enc of SUnsigned -> binary "bvlshr" BvLShR ; SSigned -> binary "bvashr" BvAShR               SArraySort _ _ -> ternary "store" ArrStore                       -- TODO: Add compare ops for all (?) array-sorts               SStringSort -> binary "str.++" (<>) <|> binary "str.at" strAt <|> ternary "str.substr" StrSubstring@@ -160,39 +164,39 @@  constant :: forall t. KnownSMTSort t => Parser (HaskellType t) constant = case sortSing @t of-  SIntSort  -> anyValue decimal-  SRealSort -> anyValue parseRatioDouble <|> parseToRealDouble <|> anyValue rational-  SBoolSort -> parseBool-  SBvSort p -> anyBitvector p+  SIntSort       -> anyValue decimal+  SRealSort      -> anyValue parseRatioDouble <|> parseToRealDouble <|> anyValue rational+  SBoolSort      -> parseBool+  SBvSort _ p    -> anyBitvector p   SArraySort k v -> constArray k v-  SStringSort -> parseSmtString+  SStringSort    -> parseSmtString {-# INLINEABLE constant #-}  constantExpr :: forall t. KnownSMTSort t => Parser (Expr t) constantExpr = Constant . wrapValue <$> constant @t {-# INLINE constantExpr #-} -anyBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n)+anyBitvector :: (KnownBvEnc enc, KnownNat n) => Proxy n -> Parser (Bitvec enc n) anyBitvector p = binBitvector p <|> hexBitvector p <|> literalBitvector p {-# INLINE anyBitvector #-} -binBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n)+binBitvector :: KnownNat n => Proxy n -> Parser (Bitvec enc n) binBitvector p = do   _  <- string "#b" >> skipSpace   bs <- many $ char '0' <|> char '1'   let bs' :: [Bit] = fmap (\b -> ite (b == '1') true false) bs-  case bvFromListN' p bs' of+  case bitvecFromListN' p bs' of     Nothing -> fail $ "Expected BitVector of length" <> show (natVal p) <> ", but got a different one"     Just v  -> return v {-# INLINEABLE binBitvector #-} -hexBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n)+hexBitvector :: (KnownBvEnc enc, KnownNat n) => Proxy n -> Parser (Bitvec enc n) hexBitvector _ = do   _ <- string "#x" >> skipSpace   fromInteger <$> hexadecimal {-# INLINE hexBitvector #-} -literalBitvector :: KnownNat n => Proxy n -> Parser (Bitvec n)+literalBitvector :: (KnownBvEnc enc, KnownNat n) => Proxy n -> Parser (Bitvec enc n) literalBitvector _ = do   _ <- char '(' >> skipSpace   _ <- char '_' >> skipSpace

@@ -14,14 +14,13 @@ import Data.GADT.Compare import Data.HashMap.Lazy import Data.Default+import Data.Kind import Control.Monad.State import Control.Lens import System.Mem.StableName import System.IO.Unsafe import Unsafe.Coerce -import Data.Kind- -- | Mode used for sharing. data SharingMode =     None            -- ^ Common expressions are not shared at all@@ -60,7 +59,7 @@         SBoolSort      -> share origExpr expr         SIntSort       -> share origExpr expr         SRealSort      -> share origExpr expr-        SBvSort _      -> share origExpr expr+        SBvSort _ _    -> share origExpr expr         SArraySort _ _ -> share origExpr expr         SStringSort    -> share origExpr expr) 

@@ -0,0 +1,150 @@+{-# LANGUAGE DerivingStrategies #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE RoleAnnotations #-}++module Language.Hasmtlib.Type.Bitvec+( BvEnc(..), SBvEnc(..), KnownBvEnc(..)+, bvEncSing', bvEncSing''+, Bitvec(..)+, asUnsigned, asSigned+, bitvecConcat, bitvecFromListN, bitvecFromListN'+)+where++import Prelude hiding ((&&), (||), not)+import Language.Hasmtlib.Boolean+import Language.Hasmtlib.Internal.Render+import Data.GADT.Compare+import Data.ByteString.Builder+import Data.Bit+import Data.Bits+import Data.Coerce+import Data.Finite hiding (shift)+import Data.Proxy+import Data.Bifunctor+import Data.Type.Equality+import qualified Data.Vector.Unboxed.Sized as V+import GHC.TypeNats++-- | Type of Bitvector encoding - used as promoted type (data-kind).+data BvEnc = Unsigned | Signed deriving (Show, Eq, Ord)++-- | Singleton for 'BvEnc'.+data SBvEnc (enc :: BvEnc) where+  SUnsigned :: SBvEnc Unsigned+  SSigned   :: SBvEnc Signed++deriving instance Show (SBvEnc enc)+deriving instance Eq   (SBvEnc enc)+deriving instance Ord  (SBvEnc enc)++-- | Compute singleton 'SBvEnc' from it's promoted type 'BvEnc'.+class KnownBvEnc (enc :: BvEnc) where bvEncSing :: SBvEnc enc+instance KnownBvEnc Unsigned    where bvEncSing = SUnsigned+instance KnownBvEnc Signed      where bvEncSing = SSigned++-- | Wrapper for 'bvEncSing' which takes a 'Proxy'.+bvEncSing' :: forall enc prxy. KnownBvEnc enc => prxy enc -> SBvEnc enc+bvEncSing' _ = bvEncSing @enc++-- | Wrapper for 'bvEncSing' which takes a 'Proxy' and some ballast.+--   This is helpful for singing on values of type 'Bitvec' where the ballst is a 'Nat'.+bvEncSing'' :: forall enc a prxy. KnownBvEnc enc => prxy enc a -> SBvEnc enc+bvEncSing'' _ = bvEncSing @enc++instance GEq SBvEnc where+  geq SUnsigned SUnsigned = Just Refl+  geq SSigned SSigned = Just Refl+  geq _ _ = Nothing++instance GCompare SBvEnc where+  gcompare SUnsigned SUnsigned = GEQ+  gcompare SUnsigned _  = GLT+  gcompare _ SUnsigned  = GGT+  gcompare SSigned SSigned = GEQ+  -- gcompare SSigned _  = GLT+  -- gcompare _ SSigned  = GGT++-- | Length-indexed bitvector ('V.Vector') carrying a phantom type-level 'BvEnc'.+--   Most significant bit is first (index 0) for unsigned bitvectors.+--   Signed bitvectors have their sign bit first (index 0) and their most significant bit second (index 1).+type role Bitvec phantom phantom+newtype Bitvec (enc :: BvEnc) (n :: Nat) = Bitvec { unBitvec :: V.Vector n Bit }+  deriving newtype (Eq, Ord, Boolean)++-- | Convert 'Bitvec' with any encoding 'BvEnc' to 'Unsigned'.+asUnsigned :: forall enc n. Bitvec enc n -> Bitvec Unsigned n+asUnsigned = coerce . coerce @(Bitvec enc n) @(V.Vector n Bit)++-- | Convert 'Bitvec' with any encoding 'BvEnc' to 'Signed'.+asSigned :: forall enc n. Bitvec enc n -> Bitvec Signed n+asSigned = coerce . coerce @(Bitvec enc n) @(V.Vector n Bit)++instance Show (Bitvec enc n) where+  show = V.toList . V.map (\b -> if coerce b then '1' else '0') . coerce @_ @(V.Vector n Bit)+  {-# INLINEABLE show #-}++instance Render (Bitvec enc n) where+  render = stringUtf8 . show+  {-# INLINE render #-}++instance (KnownBvEnc enc, KnownNat n) => Bits (Bitvec enc n) where+  (.&.) = (&&)+  (.|.) = (||)+  xor = Language.Hasmtlib.Boolean.xor+  complement = not+  shift bv i  = coerce $ shift (coerce @_ @(V.Vector n Bit) bv) (negate i)+  rotate bv i = coerce $ rotate (coerce @_ @(V.Vector n Bit) bv) (negate i)+  bitSize _ = fromIntegral $ natVal (Proxy @n)+  bitSizeMaybe _ = Just $ fromIntegral $ natVal (Proxy @n)+  isSigned _ = case bvEncSing @enc of+    SUnsigned -> False+    SSigned -> True+  testBit bv = testBit (V.reverse (coerce @_ @(V.Vector n Bit) bv))+  bit (toInteger -> i) = coerce $ V.reverse $ V.replicate @n (Bit False) V.// [(finite i, Bit True)]+  popCount = coerce . popCount . coerce @_ @(V.Vector n Bit)++instance (KnownBvEnc enc, KnownNat n) => Num (Bitvec enc n) where+   fromInteger x = coerce . V.reverse $ V.generate @n (coerce . testBit x . fromInteger . getFinite)+   negate        = case bvEncSing @enc of+    SUnsigned -> id+    SSigned -> (+1) . not+   abs x         = if signum x < 0 then negate x else x+   signum x      = case bvEncSing @enc of+    SUnsigned -> 0+    SSigned -> if testBit x 0 then -1 else 1+   x + y = fromInteger $ toInteger x + toInteger y+   x - y = fromInteger $ toInteger x - toInteger y+   x * y = fromInteger $ toInteger x * toInteger y++instance (KnownBvEnc enc, KnownNat n) => Bounded (Bitvec enc n) where+  minBound = case bvEncSing @enc of+    SUnsigned -> coerce $ V.replicate @n false+    SSigned -> coerce $ setBit (V.replicate @n false) 0+  maxBound = case bvEncSing @enc of+    SUnsigned -> coerce $ V.replicate @n true+    SSigned -> coerce $ clearBit (V.replicate @n true) 0++instance (KnownBvEnc enc, KnownNat n) => Enum (Bitvec enc n) where+  toEnum     = fromInteger . toInteger+  fromEnum x = case bvEncSing @enc of+    SUnsigned -> V.sum . V.imap (\i b -> if coerce b then 2 ^ getFinite i else 0) . V.reverse $ coerce @_ @(V.Vector n Bit) x+    SSigned -> if testBit x 0+          then negate . (+1) . V.sum . V.imap (\i b -> if coerce b then 2 ^ getFinite i else 0) . V.reverse $ coerce @_ @(V.Vector n Bit) $ not x+          else V.sum . V.imap (\i b -> if coerce b then 2 ^ getFinite i else 0) . V.reverse $ coerce @_ @(V.Vector n Bit) x++instance (KnownBvEnc enc, KnownNat n) => Real (Bitvec enc n) where+  toRational = toRational . fromEnum++instance (KnownBvEnc enc, KnownNat n) => Integral (Bitvec enc n) where+  toInteger = fromIntegral . fromEnum+  quotRem x y = bimap fromInteger fromInteger $ quotRem (toInteger x) (toInteger y)++bitvecConcat :: Bitvec enc n -> Bitvec enc m -> Bitvec enc (n + m)+bitvecConcat (coerce -> x) (coerce -> y) = coerce $ x V.++ y++bitvecFromListN :: forall n enc. KnownNat n => [Bit] -> Maybe (Bitvec enc n)+bitvecFromListN = coerce . V.fromListN @n++bitvecFromListN' :: KnownNat n => Proxy n -> [Bit] -> Maybe (Bitvec enc n)+bitvecFromListN' _ = bitvecFromListN

@@ -13,7 +13,7 @@   , equal, distinct   , for_all, exists   , select, store-  , bvShL, bvLShR, bvConcat+  , bvShL, bvLShR, bvAShR, bvConcat   , toRealSort, toIntSort, isIntSort   , strLength, strAt, strSubstring, strPrefixOf, strSuffixOf, strContains, strIndexOf, strReplace, strReplaceAll   )@@ -22,6 +22,7 @@ import Prelude hiding (not, and, or, any, all, (&&), (||)) import Language.Hasmtlib.Internal.Uniplate1 import Language.Hasmtlib.Internal.Render+import Language.Hasmtlib.Type.Bitvec (BvEnc(..), KnownBvEnc(..), SBvEnc(..), bvEncSing') import Language.Hasmtlib.Type.ArrayMap import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Value@@ -71,6 +72,7 @@   Mul       :: Num (HaskellType t) => Expr t -> Expr t -> Expr t   Abs       :: Num (HaskellType t) => Expr t -> Expr t   Mod       :: Integral (HaskellType t) => Expr t -> Expr t  -> Expr t+  Rem       :: Integral (HaskellType t) => Expr t -> Expr t  -> Expr t   IDiv      :: Integral (HaskellType t) => Expr t -> Expr t  -> Expr t   Div       :: Expr RealSort -> Expr RealSort -> Expr RealSort   LTH       :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort@@ -97,19 +99,18 @@   ToInt     :: Expr RealSort -> Expr IntSort   IsInt     :: Expr RealSort -> Expr BoolSort   Ite       :: Expr BoolSort -> Expr t -> Expr t -> Expr t-  BvNand    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)-  BvNor     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)-  BvShL     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)-  BvLShR    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)-  BvConcat  :: (KnownNat n, KnownNat m) => Expr (BvSort n) -> Expr (BvSort m) -> Expr (BvSort (n + m))-  BvRotL    :: (KnownNat n, Integral a) => a -> Expr (BvSort n) -> Expr (BvSort n)-  BvRotR    :: (KnownNat n, Integral a) => a -> Expr (BvSort n) -> Expr (BvSort n)+  BvNand    :: (KnownBvEnc enc, KnownNat n) => Expr (BvSort enc n) -> Expr (BvSort enc n) -> Expr (BvSort enc n)+  BvNor     :: (KnownBvEnc enc, KnownNat n) => Expr (BvSort enc n) -> Expr (BvSort enc n) -> Expr (BvSort enc n)+  BvShL     :: (KnownBvEnc enc, KnownNat n) => Expr (BvSort enc n) -> Expr (BvSort enc n) -> Expr (BvSort enc n)+  BvLShR    :: KnownNat n => Expr (BvSort Unsigned n) -> Expr (BvSort Unsigned n) -> Expr (BvSort Unsigned n)+  BvAShR    :: KnownNat n => Expr (BvSort Signed n) -> Expr (BvSort Signed n) -> Expr (BvSort Signed n)+  BvConcat  :: (KnownBvEnc enc , KnownNat n, KnownNat m) => Expr (BvSort enc n) -> Expr (BvSort enc m) -> Expr (BvSort enc (n + m))+  BvRotL    :: (KnownBvEnc enc, KnownNat n, Integral a) => a -> Expr (BvSort enc n) -> Expr (BvSort enc n)+  BvRotR    :: (KnownBvEnc enc, KnownNat n, Integral a) => a -> Expr (BvSort enc n) -> Expr (BvSort enc n)   ArrSelect :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => Expr (ArraySort k v) -> Expr k -> Expr v   ArrStore  :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v -> Expr (ArraySort k v)   StrConcat     :: Expr StringSort -> Expr StringSort -> Expr StringSort   StrLength     :: Expr StringSort -> Expr IntSort-  StrLT         :: Expr StringSort -> Expr StringSort -> Expr BoolSort-  StrLTHE       :: Expr StringSort -> Expr StringSort -> Expr BoolSort   StrAt         :: Expr StringSort -> Expr IntSort -> Expr StringSort   StrSubstring  :: Expr StringSort -> Expr IntSort -> Expr IntSort -> Expr StringSort   StrPrefixOf   :: Expr StringSort -> Expr StringSort -> Expr BoolSort@@ -118,14 +119,13 @@   StrIndexOf    :: Expr StringSort -> Expr StringSort -> Expr IntSort -> Expr IntSort   StrReplace    :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort   StrReplaceAll :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort-   -- | Just v if quantified var has been created already, Nothing otherwise   ForAll    :: KnownSMTSort t => Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Expr BoolSort   -- | Just v if quantified var has been created already, Nothing otherwise   Exists    :: KnownSMTSort t => Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Expr BoolSort -  -- | Indicates whether an expression is a leaf.-  --   All non-recursive contructors form leafs.+-- | Indicates whether an expression is a leaf.+--   All non-recursive contructors form leafs. isLeaf :: Expr t -> Bool isLeaf (Var _) = True isLeaf (Constant _) = True@@ -310,27 +310,7 @@ max' :: (Orderable a, Iteable (Expr BoolSort) a) => a -> a -> a max' x y = ite (y <=? x) x y -instance Orderable (Expr IntSort) where-  (<?)     = LTH-  {-# INLINE (<?) #-}-  (<=?)    = LTHE-  {-# INLINE (<=?) #-}-  (>=?)    = GTHE-  {-# INLINE (>=?) #-}-  (>?)     = GTH-  {-# INLINE (>?) #-}--instance Orderable (Expr RealSort) where-  (<?)     = LTH-  {-# INLINE (<?) #-}-  (<=?)    = LTHE-  {-# INLINE (<=?) #-}-  (>=?)    = GTHE-  {-# INLINE (>=?) #-}-  (>?)     = GTH-  {-# INLINE (>?) #-}--instance KnownNat n => Orderable (Expr (BvSort n)) where+instance (KnownSMTSort t, Ord (HaskellType t)) => Orderable (Expr t) where   (<?)     = LTH   {-# INLINE (<?) #-}   (<=?)    = LTHE@@ -340,13 +320,6 @@   (>?)     = GTH   {-# INLINE (>?) #-} --- | Lexicographic ordering for '(<?)' and reflexive closure of lexicographic ordering for '(<=?)'-instance Orderable (Expr StringSort) where-  (<?)     = StrLT-  {-# INLINE (<?) #-}-  (<=?)    = StrLTHE-  {-# INLINE (<=?) #-}- class GEquatable f => GOrderable f where   (<?#)  :: f a -> f a -> Expr BoolSort   (<=?#) :: f a -> f a -> Expr BoolSort@@ -504,18 +477,23 @@ store = ArrStore {-# INLINE store #-} --- | Bitvector shift left-bvShL    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)+-- | Logically shift left the first expression by the second expression.+bvShL    :: (KnownBvEnc enc, KnownNat n) => Expr (BvSort enc n) -> Expr (BvSort enc n) -> Expr (BvSort enc n) bvShL    = BvShL {-# INLINE bvShL #-} --- | Bitvector logical shift right-bvLShR   :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)+-- | Logically shift right the first expression by the second expression.+bvLShR   :: KnownNat n => Expr (BvSort Unsigned n) -> Expr (BvSort Unsigned n) -> Expr (BvSort Unsigned n) bvLShR   = BvLShR {-# INLINE bvLShR #-} --- | Concat two bitvectors-bvConcat :: (KnownNat n, KnownNat m) => Expr (BvSort n) -> Expr (BvSort m) -> Expr (BvSort (n + m))+-- | Arithmetically shift right the first expression by the second expression.+bvAShR   :: KnownNat n => Expr (BvSort Signed n) -> Expr (BvSort Signed n) -> Expr (BvSort Signed n)+bvAShR   = BvAShR+{-# INLINE bvAShR #-}++-- | Concats two bitvectors.+bvConcat :: (KnownBvEnc enc, KnownNat n, KnownNat m) => Expr (BvSort enc n) -> Expr (BvSort enc m) -> Expr (BvSort enc (n + m)) bvConcat = BvConcat {-# INLINE bvConcat #-} @@ -596,92 +574,50 @@ strReplaceAll = StrReplaceAll {-# INLINE strReplaceAll #-} -instance Num (Expr IntSort) where-   fromInteger = Constant . IntValue-   {-# INLINE fromInteger #-}-   (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 - (Constant (IntValue 0)) = x-   (Constant (IntValue x)) - (Constant (IntValue y)) = Constant (IntValue (x - y))-   x - y = Minus x y-   {-# INLINE (-) #-}-   (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 #-}-   abs         = Abs-   {-# INLINE abs #-}-   signum x    = ite (x === 0) 0 $ ite (x <? 0) (-1) 1-   {-# INLINE signum #-}--instance Num (Expr RealSort) where-   fromInteger = Constant . RealValue . fromIntegral+instance (KnownSMTSort t, Num (HaskellType t), Ord (HaskellType t)) => Num (Expr t) where+   fromInteger = Constant . wrapValue . fromInteger    {-# INLINE fromInteger #-}-   (Constant (RealValue 0)) + y = y-   x + (Constant (RealValue 0)) = x-   (Constant (RealValue x)) + (Constant (RealValue y)) = Constant (RealValue (x + y))+   (Constant 0) + y = y+   x + (Constant 0) = x+   (Constant x) + (Constant y) = Constant (x + y)    x + y = Plus x y    {-# INLINE (+) #-}-   x - (Constant (RealValue 0)) = x-   (Constant (RealValue x)) - (Constant (RealValue y)) = Constant (RealValue (x - y))+   x - (Constant 0) = x+   (Constant x) - (Constant y) = Constant (x - y)+   (Constant 0) - x = negate x    x - y = Minus x y    {-# INLINE (-) #-}-   (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))+   (Constant 0) * _ = 0+   _ * (Constant 0) = 0+   (Constant 1) * y = y+   x * (Constant 1) = x+   (Constant (-1)) * x = negate x+   x * (Constant (-1)) = negate x+   (Constant x) * (Constant y) = Constant (x * y)    x * y = Mul x y    {-# INLINE (*) #-}-   negate      = Neg+   negate (Constant x) = Constant $ negate x+   negate (Neg x)      = x+   negate x            = Neg x    {-# INLINE negate #-}-   abs         = Abs-   {-# INLINE abs #-}-   signum x    = ite (x === 0) 0 $ ite (x <? 0) (-1) 1-   {-# INLINE signum #-}--instance KnownNat n => Num (Expr (BvSort n)) where-   fromInteger = Constant . BvValue . fromInteger-   {-# INLINE fromInteger #-}-   (Constant (BvValue 0)) + y = y-   x + (Constant (BvValue 0)) = x-   (Constant (BvValue x)) + (Constant (BvValue y)) = Constant (BvValue (x + y))-   x + y = Plus x y-   {-# INLINE (+) #-}-   x - (Constant (BvValue 0)) = x-   (Constant (BvValue x)) - (Constant (BvValue y)) = Constant (BvValue (x - y))-   x - y = Minus x y-   {-# INLINE (-) #-}-   (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 = Mul x y-   {-# INLINE (*) #-}-   abs         = id+   abs (Constant x) = Constant $ abs x+   abs x            = Abs x    {-# INLINE abs #-}-   signum _    = 0+   signum (Constant x) = Constant $ signum x+   signum x            = ite (x === 0) 0 $ ite (x <? 0) (-1) 1    {-# INLINE signum #-}  instance Fractional (Expr RealSort) where   fromRational = Constant . RealValue . fromRational   {-# INLINE fromRational #-}-  x / (Constant (RealValue 1)) = x-  (Constant (RealValue 0)) / _ = 0-  (Constant (RealValue x)) / (Constant (RealValue y)) = Constant (RealValue (x / y))+  x / (Constant  1) = x+  (Constant 0) / _ = 0+  (Constant x) / (Constant y) = Constant (x / y)   x / y          = Div x y   {-# INLINE (/) #-} --- | Not in the SMTLib2.6-standard. Solvers like CVC5 and MathSAT support it though.+-- | Not part of the SMTLib standard Version 2.6.+--   Some solvers support it. At least valid for CVC5 and MathSAT. instance Floating (Expr RealSort) where     pi    = Pi     {-# INLINE pi #-}@@ -709,106 +645,61 @@     acosh = error "SMT-Solvers currently do not support acosh"     atanh = error "SMT-Solvers currently do not support atanh" --- | This instance is __partial__ for 'toRational', it's only intended for use with constants ('Constant').-instance Real (Expr IntSort) where-  toRational (Constant (IntValue x)) = fromIntegral x-  toRational x = error $ "Real#toRational[Expr IntSort] only supported for constants. But given: " <> show x-  {-# INLINE toRational #-}---- | This instance is __partial__ for 'fromEnum', it's only intended for use with constants ('Constant').-instance Enum (Expr IntSort) where-  fromEnum (Constant (IntValue x)) = fromIntegral x-  fromEnum x = error $ "Enum#fromEnum[Expr IntSort] only supported for constants. But given: " <> show x-  {-# INLINE fromEnum #-}-  toEnum = fromInteger . fromIntegral-  {-# INLINE toEnum #-}---- | This instance is __partial__ for 'toInteger', it's only intended for use with constants ('Constant').-instance Integral (Expr IntSort) where-  quot = IDiv-  {-# INLINE quot #-}-  rem  = Mod-  {-# INLINE rem #-}-  div  = IDiv-  {-# INLINE div #-}-  mod  = Mod-  {-# INLINE mod #-}-  quotRem x y = (quot x y, rem x y)-  {-# INLINE quotRem #-}-  divMod x y  = (div x y, mod x y)-  {-# INLINE divMod #-}-  toInteger (Constant (IntValue x)) = x-  toInteger x = error $ "Integer#toInteger[Expr IntSort] only supported for constants. But given: " <> show x-  {-# INLINE toInteger #-}---- | This instance is __partial__ for 'toRational', it's only intended for use with constants ('Constant').-instance Real (Expr RealSort) where-  toRational (Constant (RealValue x)) = toRational x-  toRational x = error $ "Real#toRational[Expr RealSort] only supported for constants. But given: " <> show x-  {-# INLINE toRational #-}---- | This instance is __partial__ for 'fromEnum', it's only intended for use with constants ('Constant').-instance Enum (Expr RealSort) where-  fromEnum (Constant (RealValue x)) = fromEnum x-  fromEnum x = error $ "Enum#fromEnum[Expr RealSort] only supported for constants. But given: " <> show x-  {-# INLINE fromEnum #-}-  toEnum = fromInteger . fromIntegral-  {-# INLINE toEnum #-}---- | This instance is __partial__ for 'toRational', it's only intended for use with constants ('Constant').-instance KnownNat n => Real (Expr (BvSort n)) where-  toRational (Constant (BvValue x)) = fromIntegral x-  toRational x = error $ "Real#toRational[Expr BvSort] only supported for constants. But given: " <> show x+-- | This instance is __partial__ for 'toRational', this method is only intended for use with constants.+instance (KnownSMTSort t, Real (HaskellType t)) => Real (Expr t) where+  toRational (Constant x) = toRational $ unwrapValue x+  toRational x = error $ "Real#toRational[Expr " <> show (sortSing @t) <> "] only supported for constants. But given: " <> show x   {-# INLINE toRational #-} --- | This instance is __partial__ for 'fromEnum', it's only intended for use with constants ('Constant').-instance KnownNat n => Enum (Expr (BvSort n)) where-  fromEnum (Constant (BvValue x)) = fromIntegral x-  fromEnum x = error $ "Enum#fromEnum[Expr BvSort] only supported for constants. But given: " <> show x+-- | This instance is __partial__ for 'fromEnum', this method is only intended for use with constants.+instance (KnownSMTSort t, Enum (HaskellType t)) => Enum (Expr t) where+  fromEnum (Constant x) = fromEnum $ unwrapValue x+  fromEnum x = error $ "Enum#fromEnum[Expr " <> show (sortSing @t) <> "] only supported for constants. But given: " <> show x   {-# INLINE fromEnum #-}-  toEnum = fromInteger . fromIntegral+  toEnum = Constant . wrapValue . toEnum   {-# INLINE toEnum #-} --- | This instance is __partial__ for 'toInteger', it's only intended for use with constants ('Constant').-instance KnownNat n => Integral (Expr (BvSort n)) where-  quot        = IDiv-  {-# INLINE quot #-}-  rem         = Mod-  {-# INLINE rem #-}-  div         = IDiv-  {-# INLINE div #-}-  mod         = Mod-  {-# INLINE mod #-}-  quotRem x y = (quot x y, rem x y)+-- | This instance is __partial__ for 'toInteger', this method is only intended for use with constants.+instance (KnownSMTSort t, Integral (HaskellType t)) => Integral (Expr t) where+  quotRem x y = (IDiv x y, Rem x y)   {-# INLINE quotRem #-}-  divMod x y  = (div x y, mod x y)+  divMod x y  = (IDiv x y, Mod x y)   {-# INLINE divMod #-}-  toInteger (Constant (BvValue x)) = fromIntegral x-  toInteger x = error $ "Integer#toInteger[Expr BvSort] only supported for constants. But given: " <> show x+  toInteger (Constant x) = toInteger $ unwrapValue x+  toInteger x = error $ "Integer#toInteger[Expr " <> show (sortSing @t) <> "] only supported for constants. But given: " <> show x   {-# INLINE toInteger #-}  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 x) = Constant $ not x+  not (Not x) = 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 #-}   (<==>) = (===)   {-# INLINE (<==>) #-} -instance KnownNat n => Boolean (Expr (BvSort n)) where+instance (KnownBvEnc enc, KnownNat n) => Boolean (Expr (BvSort enc n)) where   bool = Constant . BvValue . bool   {-# INLINE bool #-}   (&&) = And   {-# INLINE (&&) #-}   (||) = Or   {-# INLINE (||) #-}-  not  = Not+  not (Not x) = x+  not x = Not x   {-# INLINE not #-}   xor  = Xor   {-# INLINE xor #-}@@ -819,7 +710,7 @@   maxBound = true   {-# INLINE maxBound #-} -instance KnownNat n => Bounded (Expr (BvSort n)) where+instance (KnownBvEnc enc, KnownNat n) => Bounded (Expr (BvSort enc n)) where   minBound = Constant $ BvValue minBound   {-# INLINE minBound #-}   maxBound = Constant $ BvValue maxBound@@ -869,7 +760,7 @@   {-# INLINE popCount #-}  -- | This instance is __partial__ for 'testBit' and 'popCount', it's only intended for use with constants ('Constant').-instance KnownNat n => Bits.Bits (Expr (BvSort n)) where+instance (KnownBvEnc enc, KnownNat n) => Bits.Bits (Expr (BvSort enc n)) where   (.&.) = And   {-# INLINE (.&.) #-}   (.|.) = Or@@ -889,11 +780,15 @@   {-# INLINE bitSizeMaybe #-}   bitSize _ = fromIntegral $ natVal $ Proxy @n   {-# INLINE bitSize #-}-  isSigned _ = False+  isSigned _ = case bvEncSing @enc of+    SUnsigned -> False+    SSigned   -> True   {-# INLINE isSigned #-}   shiftL b i = BvShL b (fromIntegral i)   {-# INLINE shiftL #-}-  shiftR b i = BvLShR b (fromIntegral i)+  shiftR b i = case bvEncSing @enc of+    SUnsigned -> BvLShR b (fromIntegral i)+    SSigned   -> BvAShR b (fromIntegral i)   {-# INLINE shiftR #-}   rotateL b i = BvRotL i b   {-# INLINE rotateL #-}@@ -940,29 +835,68 @@ instance KnownSMTSort t => Render (Expr t) where   render (Var v)      = render v   render (Constant c) = render c--  render (Plus x y)   = renderBinary (case sortSing' x of SBvSort _ -> "bvadd" ; _ -> "+") x y-  render (Minus x y)  = renderBinary (case sortSing' x of SBvSort _ -> "bvsub" ; _ -> "-") x y-  render (Neg x)      = renderUnary  (case sortSing' x of SBvSort _ -> "bvneg" ; _ -> "-") x-  render (Mul x y)    = renderBinary (case sortSing' x of SBvSort _ -> "bvmul" ; _ -> "*") x y+  render (Plus x y)   = renderBinary (case sortSing' x of SBvSort _ _ -> "bvadd" ; _ -> "+") x y+  render (Minus x y)  = renderBinary (case sortSing' x of SBvSort _ _ -> "bvsub" ; _ -> "-") x y+  render (Neg x)      = renderUnary  (case sortSing' x of SBvSort _ _ -> "bvneg" ; _ -> "-") x+  render (Mul x y)    = renderBinary (case sortSing' x of SBvSort _ _ -> "bvmul" ; _ -> "*") x y   render (Abs x)      = renderUnary  "abs" x-  render (Mod x y)    = renderBinary (case sortSing' x of SBvSort _ -> "bvurem" ; _ -> "mod") x y-  render (IDiv x y)   = renderBinary (case sortSing' x of SBvSort _ -> "bvudiv" ; _ -> "div") x y+  render (Mod x y)    = renderBinary opStr x y+    where+      opStr = case sortSing' x of+        SBvSort enc _ -> case bvEncSing' enc of+          SUnsigned -> "bvurem"+          SSigned -> "bvsmod"+        _ -> "mod"+  render (Rem x y)    = renderBinary opStr x y+    where+      opStr = case sortSing' x of+        SBvSort enc _ -> case bvEncSing' enc of+          SUnsigned -> "bvurem"+          SSigned -> "bvsrem"+        _ -> "rem"+  render (IDiv x y)   = renderBinary opStr x y+    where+      opStr = case sortSing' x of+        SBvSort enc _ -> case bvEncSing' enc of+          SUnsigned -> "bvudiv"+          SSigned -> "bvsdiv"+        _ -> "div"   render (Div x y)    = renderBinary "/" x y--  render (LTH x y)    = renderBinary (case sortSing' x of SBvSort _ -> "bvult" ; _ -> "<") x y-  render (LTHE x y)   = renderBinary (case sortSing' x of SBvSort _ -> "bvule" ; _ -> "<=") x y+  render (LTH x y)    = renderBinary opStr x y+    where+      opStr = case sortSing' x of+        SBvSort enc _ -> case bvEncSing' enc of+          SUnsigned -> "bvult"+          SSigned -> "bvslt"+        SStringSort -> "str.<"+        _ -> "<"+  render (LTHE x y)   = renderBinary opStr x y+    where+      opStr = case sortSing' x of+        SBvSort enc _ -> case bvEncSing' enc of+          SUnsigned -> "bvule"+          SSigned -> "bvsle"+        SStringSort -> "str.<="+        _ -> "<="   render (EQU xs)     = renderNary "=" $ V.toList xs   render (Distinct xs)= renderNary "distinct" $ V.toList xs-  render (GTHE x y)   = renderBinary (case sortSing' x of SBvSort _ -> "bvuge" ; _ -> ">=") x y-  render (GTH x y)    = renderBinary (case sortSing' x of SBvSort _ -> "bvugt" ; _ -> ">") x y--  render (Not x)      = renderUnary  (case sortSing' x of SBvSort _ -> "bvnot" ; _ -> "not") x-  render (And x y)    = renderBinary (case sortSing' x of SBvSort _ -> "bvand" ; _ -> "and") x y-  render (Or x y)     = renderBinary (case sortSing' x of SBvSort _ -> "bvor" ; _ -> "or") x y+  render (GTHE x y)   = case sortSing' x of+    SBvSort enc _ -> case bvEncSing' enc of+      SUnsigned -> renderBinary "bvuge" x y+      SSigned   -> renderBinary "bvsge" x y+    SStringSort -> renderBinary "str.<=" y x+    _           -> renderBinary ">=" x y+  render (GTH x y)    = case sortSing' x of+    SBvSort enc _ -> case bvEncSing' enc of+      SUnsigned -> renderBinary "bvugt" x y+      SSigned   -> renderBinary "bvsgt" x y+    SStringSort -> renderBinary "str.<" y x+    _           -> renderBinary ">" x y+  render (Not x)      = renderUnary  (case sortSing' x of SBvSort _ _ -> "bvnot" ; _ -> "not") x+  render (And x y)    = renderBinary (case sortSing' x of SBvSort _ _ -> "bvand" ; _ -> "and") x y+  render (Or x y)     = renderBinary (case sortSing' x of SBvSort _ _ -> "bvor" ; _ -> "or") x y   render (Impl x y)   = renderBinary "=>" x y-  render (Xor x y)    = renderBinary (case sortSing' x of SBvSort _ -> "bvxor" ; _ -> "xor") x y-+  render (Xor x y)    = renderBinary (case sortSing' x of SBvSort _ _ -> "bvxor" ; _ -> "xor") x y   render Pi           = "real.pi"   render (Sqrt x)     = renderUnary "sqrt" x   render (Exp x)      = renderUnary "exp" x@@ -972,28 +906,22 @@   render (Asin x)     = renderUnary "arcsin" x   render (Acos x)     = renderUnary "arccos" x   render (Atan x)     = renderUnary "arctan" x-   render (ToReal x)   = renderUnary "to_real" x   render (ToInt x)    = renderUnary "to_int" x   render (IsInt x)    = renderUnary "is_int" x-   render (Ite p t f)  = renderTernary "ite" p t f-   render (BvNand x y)       = renderBinary "bvnand" (render x) (render y)   render (BvNor x y)        = renderBinary "bvnor"  (render x) (render y)   render (BvShL x y)        = renderBinary "bvshl"  (render x) (render y)   render (BvLShR x y)       = renderBinary "bvlshr" (render x) (render y)+  render (BvAShR x y)       = renderBinary "bvashr" (render x) (render y)   render (BvConcat x y)     = renderBinary "concat" (render x) (render y)   render (BvRotL i x)       = renderUnary (renderBinary "_" ("rotate_left"  :: Builder) (render $ toInteger i)) (render x)   render (BvRotR i x)       = renderUnary (renderBinary "_" ("rotate_right" :: Builder) (render $ toInteger i)) (render x)-   render (ArrSelect a i)    = renderBinary  "select" (render a) (render i)   render (ArrStore a i v)   = renderTernary "store"  (render a) (render i) (render v)-   render (StrConcat x y)        = renderBinary "str.++"  (render x) (render y)   render (StrLength x)          = renderUnary  "str.len" (render x)-  render (StrLT x y)            = renderBinary "str.<"   (render x) (render y)-  render (StrLTHE x y)          = renderBinary "str.<="  (render x) (render y)   render (StrAt x i)            = renderBinary "str.at"  (render x) (render i)   render (StrSubstring x i j)   = renderTernary "str.substr"  (render x) (render i) (render j)   render (StrPrefixOf x y)      = renderBinary "str.prefixof" (render x) (render y)@@ -1002,7 +930,6 @@   render (StrIndexOf x y i)     = renderTernary "str.indexof"     (render x) (render y) (render i)   render (StrReplace x y y')    = renderTernary "str.replace"     (render x) (render y) (render y')   render (StrReplaceAll x y y') = renderTernary "str.replace_all" (render x) (render y) (render y')-   render (ForAll mQvar f) = renderQuantifier "forall" mQvar f   render (Exists mQvar f) = renderQuantifier "exists" mQvar f @@ -1072,6 +999,7 @@   uniplate1 f (Mul x y)               = Mul <$> f x <*> f y   uniplate1 f (Abs x)                 = Abs <$> f x   uniplate1 f (Mod x y)               = Mod <$> f x <*> f y+  uniplate1 f (Rem x y)               = Rem <$> f x <*> f y   uniplate1 f (IDiv x y)              = IDiv <$> f x <*> f y   uniplate1 f (Div x y)               = Div <$> f x <*> f y   uniplate1 f (LTH x y)               = LTH <$> f x <*> f y@@ -1102,6 +1030,7 @@   uniplate1 f (BvNor x y)             = BvNor <$> f x <*> f y   uniplate1 f (BvShL x y)             = BvShL <$> f x <*> f y   uniplate1 f (BvLShR x y)            = BvLShR <$> f x <*> f y+  uniplate1 f (BvAShR x y)            = BvAShR <$> f x <*> f y   uniplate1 f (BvConcat x y)          = BvConcat <$> f x <*> f y   uniplate1 f (BvRotL i x)            = BvRotL i <$> f x   uniplate1 f (BvRotR i x)            = BvRotR i <$> f x@@ -1109,8 +1038,6 @@   uniplate1 f (ArrStore i x arr)      = ArrStore i <$> f x <*> f arr   uniplate1 f (StrConcat x y)         = StrConcat <$> f x <*> f y   uniplate1 f (StrLength x)           = StrLength <$> f x-  uniplate1 f (StrLT x y)             = StrLT <$> f x <*> f y-  uniplate1 f (StrLTHE x y)           = StrLTHE <$> f x <*> f y   uniplate1 f (StrAt x i)             = StrAt <$> f x <*> f i   uniplate1 f (StrSubstring x i j)    = StrSubstring <$> f x <*> f i <*> f j   uniplate1 f (StrPrefixOf x y)       = StrPrefixOf <$> f x <*> f y@@ -1140,6 +1067,7 @@           Mul x y              -> Mul  <$> tryPlate f' x <*> tryPlate f' y           Abs x                -> Abs  <$> tryPlate f' x           Mod x y              -> Mod  <$> tryPlate f' x <*> tryPlate f' y+          Rem x y              -> Mod  <$> tryPlate f' x <*> tryPlate f' y           IDiv x y             -> IDiv <$> tryPlate f' x <*> tryPlate f' y           Div x y              -> Div  <$> tryPlate f' x <*> tryPlate f' y           LTH x y              -> LTH  <$> tryPlate f' x <*> tryPlate f' y@@ -1170,6 +1098,7 @@           BvNor x y            -> BvNor  <$> tryPlate f' x <*> tryPlate f' y           BvShL x y            -> BvShL  <$> tryPlate f' x <*> tryPlate f' y           BvLShR x y           -> BvLShR <$> tryPlate f' x <*> tryPlate f' y+          BvAShR x y           -> BvAShR <$> tryPlate f' x <*> tryPlate f' y           BvConcat x y         -> BvConcat <$> tryPlate f' x <*> tryPlate f' y           BvRotL i x           -> BvRotL i <$> tryPlate f' x           BvRotR i x           -> BvRotR i <$> tryPlate f' x@@ -1177,8 +1106,6 @@           ArrStore i x arr     -> ArrStore i    <$> tryPlate f' x <*> tryPlate f' arr           StrConcat x y        -> StrConcat     <$> tryPlate f' x <*> tryPlate f' y           StrLength x          -> StrLength     <$> tryPlate f' x-          StrLT x y            -> StrLT         <$> tryPlate f' x <*> tryPlate f' y-          StrLTHE x y          -> StrLTHE       <$> tryPlate f' x <*> tryPlate f' y           StrAt x i            -> StrAt         <$> tryPlate f' x <*> tryPlate f' i           StrSubstring x i j   -> StrSubstring  <$> tryPlate f' x <*> tryPlate f' i <*> tryPlate f' j           StrPrefixOf x y      -> StrPrefixOf   <$> tryPlate f' x <*> tryPlate f' y@@ -1202,6 +1129,7 @@     Mul e1 e2            -> grnf e1 `seq` grnf e2     Abs e                -> grnf e     Mod e1 e2            -> grnf e1 `seq` grnf e2+    Rem e1 e2            -> grnf e1 `seq` grnf e2     IDiv e1 e2           -> grnf e1 `seq` grnf e2     Div e1 e2            -> grnf e1 `seq` grnf e2     LTH e1 e2            -> grnf e1 `seq` grnf e2@@ -1232,6 +1160,7 @@     BvNor e1 e2          -> grnf e1 `seq` grnf e2     BvShL e1 e2          -> grnf e1 `seq` grnf e2     BvLShR e1 e2         -> grnf e1 `seq` grnf e2+    BvAShR e1 e2         -> grnf e1 `seq` grnf e2     BvConcat e1 e2       -> grnf e1 `seq` grnf e2     BvRotL _ e           -> grnf e     BvRotR _ e           -> grnf e@@ -1239,8 +1168,6 @@     ArrStore e1 e2 e3    -> grnf e1 `seq` grnf e2 `seq` grnf e3     StrConcat e1 e2      -> grnf e1 `seq` grnf e2     StrLength e          -> grnf e-    StrLT e1 e2          -> grnf e1 `seq` grnf e2-    StrLTHE e1 e2        -> grnf e1 `seq` grnf e2     StrAt e1 e2          -> grnf e1 `seq` grnf e2     StrSubstring e1 e2 e3 -> grnf e1 `seq` grnf e2 `seq` grnf e3     StrPrefixOf e1 e2    -> grnf e1 `seq` grnf e2@@ -1300,6 +1227,9 @@   gcompare (Mod x y) (Mod x' y') = gcomparing [(x,x'), (y,y')]   gcompare (Mod _ _) _ = GLT   gcompare _ (Mod _ _) = GGT+  gcompare (Rem x y) (Rem x' y') = gcomparing [(x,x'), (y,y')]+  gcompare (Rem _ _) _ = GLT+  gcompare _ (Rem _ _) = GGT   gcompare (IDiv x y) (IDiv x' y') = gcomparing [(x,x'), (y,y')]   gcompare (IDiv _ _) _ = GLT   gcompare _ (IDiv _ _) = GGT@@ -1426,6 +1356,9 @@   gcompare (BvLShR x y)            (BvLShR x' y')          = gcomparing [(x,x'), (y,y')]   gcompare (BvLShR _ _) _ = GLT   gcompare _ (BvLShR _ _) = GGT+  gcompare (BvAShR x y)            (BvAShR x' y')          = gcomparing [(x,x'), (y,y')]+  gcompare (BvAShR _ _) _ = GLT+  gcompare _ (BvAShR _ _) = GGT   gcompare (BvConcat x y)          (BvConcat x' y')        = case gcompare (sortSing' x) (sortSing' x') of     GLT -> GLT     GEQ -> case gcompare x x' of@@ -1483,18 +1416,6 @@     GGT -> GGT   gcompare (StrLength _) _ = GLT   gcompare _ (StrLength _) = GGT-  gcompare (StrLT x y)             (StrLT x' y')           = case gcomparing [(x,x'), (y,y')] of-    GLT -> GLT-    GEQ -> GEQ-    GGT -> GGT-  gcompare (StrLT _ _) _ = GLT-  gcompare _ (StrLT _ _) = GGT-  gcompare (StrLTHE x y)           (StrLTHE x' y')         = case gcomparing [(x,x'), (y,y')] of-    GLT -> GLT-    GEQ -> GEQ-    GGT -> GGT-  gcompare (StrLTHE _ _) _ = GLT-  gcompare _ (StrLTHE _ _) = GGT   gcompare (StrAt x i)             (StrAt x' i')           = case gcompare x x' of     GLT -> GLT     GEQ -> case gcompare i i' of

@@ -5,7 +5,7 @@ module Language.Hasmtlib.Type.SMTSort where  import Language.Hasmtlib.Internal.Constraint-import Language.Hasmtlib.Internal.Bitvec+import Language.Hasmtlib.Type.Bitvec import Language.Hasmtlib.Internal.Render import Language.Hasmtlib.Type.ArrayMap import Data.GADT.Compare@@ -21,7 +21,7 @@     BoolSort                      -- ^ Sort of Bool   | IntSort                       -- ^ Sort of Int   | RealSort                      -- ^ Sort of Real-  | BvSort Nat                    -- ^ Sort of BitVec with length n+  | BvSort BvEnc Nat              -- ^ Sort of BitVec with type of encoding enc and length n   | ArraySort SMTSort SMTSort     -- ^ Sort of Array with indices k and values v   | StringSort                    -- ^ Sort of String @@ -30,7 +30,7 @@   HaskellType IntSort         = Integer   HaskellType RealSort        = Double   HaskellType BoolSort        = Bool-  HaskellType (BvSort n)      = Bitvec n+  HaskellType (BvSort enc n)  = Bitvec enc n   HaskellType (ArraySort k v) = ConstArray (HaskellType k) (HaskellType v)   HaskellType StringSort      = Text.Text @@ -39,7 +39,7 @@   SIntSort    :: SSMTSort IntSort   SRealSort   :: SSMTSort RealSort   SBoolSort   :: SSMTSort BoolSort-  SBvSort     :: KnownNat n => Proxy n -> SSMTSort (BvSort n)+  SBvSort     :: (KnownBvEnc enc, KnownNat n) => Proxy enc -> Proxy n -> SSMTSort (BvSort enc n)   SArraySort  :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => Proxy k -> Proxy v -> SSMTSort (ArraySort k v)   SStringSort :: SSMTSort StringSort @@ -51,9 +51,11 @@   geq SIntSort SIntSort       = Just Refl   geq SRealSort SRealSort     = Just Refl   geq SBoolSort SBoolSort     = Just Refl-  geq (SBvSort n) (SBvSort m) = case sameNat n m of+  geq (SBvSort enc n) (SBvSort emc m) = case sameNat n m of     Nothing   -> Nothing-    Just Refl -> Just Refl+    Just Refl -> case geq (bvEncSing' enc) (bvEncSing' emc) of+      Nothing -> Nothing+      Just Refl -> Just Refl   geq (SArraySort k v) (SArraySort k' v') = case geq (sortSing' k) (sortSing' k') of     Nothing   -> Nothing     Just Refl -> case geq (sortSing' v) (sortSing' v') of@@ -66,9 +68,12 @@   gcompare SBoolSort SBoolSort     = GEQ   gcompare SIntSort SIntSort       = GEQ   gcompare SRealSort SRealSort     = GEQ-  gcompare (SBvSort n) (SBvSort m) = case cmpNat n m of+  gcompare (SBvSort enc n) (SBvSort emc m) = case cmpNat n m of     LTI -> GLT-    EQI -> GEQ+    EQI -> case gcompare (bvEncSing' enc) (bvEncSing' emc) of+      GLT -> GLT+      GEQ -> GEQ+      GGT -> GGT     GTI -> GGT   gcompare (SArraySort k v) (SArraySort k' v') = case gcompare (sortSing' k) (sortSing' k') of     GLT -> GLT@@ -94,12 +99,12 @@ instance KnownSMTSort IntSort                  where sortSing = SIntSort instance KnownSMTSort RealSort                 where sortSing = SRealSort instance KnownSMTSort BoolSort                 where sortSing = SBoolSort-instance KnownNat n => KnownSMTSort (BvSort n) where sortSing = SBvSort (Proxy @n)+instance (KnownBvEnc enc, KnownNat n) => KnownSMTSort (BvSort enc n) where sortSing = SBvSort (Proxy @enc) (Proxy @n) instance (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => KnownSMTSort (ArraySort k v) where    sortSing = SArraySort (Proxy @k) (Proxy @v) instance KnownSMTSort StringSort                 where sortSing = SStringSort --- | Wrapper for 'sortSing' which takes a 'Proxy'+-- | Wrapper for 'sortSing' which takes a 'Proxy'. sortSing' :: forall prxy t. KnownSMTSort t => prxy t -> SSMTSort t sortSing' _ = sortSing @t @@ -116,7 +121,7 @@   render SBoolSort   = "Bool"   render SIntSort    = "Int"   render SRealSort   = "Real"-  render (SBvSort p) = renderBinary "_" ("BitVec" :: Builder) (natVal p)+  render (SBvSort _ p) = renderBinary "_" ("BitVec" :: Builder) (natVal p)   render (SArraySort k v) = renderBinary "Array" (sortSing' k) (sortSing' v)   render SStringSort   = "String"   {-# INLINEABLE render #-}

@@ -6,7 +6,10 @@ ) where +import Prelude hiding (not, (&&), (||)) import Language.Hasmtlib.Type.SMTSort+import Language.Hasmtlib.Type.Bitvec+import Language.Hasmtlib.Boolean import Data.GADT.Compare import Data.Proxy import Control.Lens@@ -18,7 +21,7 @@   IntValue    :: HaskellType IntSort    -> Value IntSort   RealValue   :: HaskellType RealSort   -> Value RealSort   BoolValue   :: HaskellType BoolSort   -> Value BoolSort-  BvValue     :: KnownNat n => HaskellType (BvSort n) -> Value (BvSort n)+  BvValue     :: (KnownBvEnc enc, KnownNat n) => HaskellType (BvSort enc n) -> Value (BvSort enc n)   ArrayValue  :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => HaskellType (ArraySort k v) -> Value (ArraySort k v)   StringValue :: HaskellType StringSort -> Value StringSort @@ -30,7 +33,9 @@   geq (IntValue x) (IntValue y)     = if x == y then Just Refl else Nothing   geq (RealValue x) (RealValue y)   = if x == y then Just Refl else Nothing   geq (BvValue x) (BvValue y)       = case cmpNat x y of-    EQI -> if x == y then Just Refl else Nothing+    EQI -> case geq (bvEncSing'' x) (bvEncSing'' y) of+      Nothing -> Nothing+      Just Refl -> if x == y then Just Refl else Nothing     _   -> Nothing   geq ax@(ArrayValue x) ay@(ArrayValue y) = case geq (sortSing' ax) (sortSing' ay) of     Nothing -> Nothing@@ -50,7 +55,10 @@   gcompare (RealValue x) (RealValue x')     = liftOrdering $ compare x x'   gcompare (BvValue x) (BvValue x')         = case cmpNat x x' of     LTI -> GLT-    EQI -> liftOrdering $ compare x x'+    EQI -> case gcompare (bvEncSing'' x) (bvEncSing'' x') of+      GLT -> GLT+      GEQ -> liftOrdering $ compare x x'+      GGT -> GGT     GTI -> GGT   gcompare (ArrayValue x) (ArrayValue x')   = case gcompare (sortSing' (pk x)) (sortSing' (pk x')) of     GLT -> GLT@@ -78,6 +86,40 @@   -- gcompare (StringValue _) _                = GLT   -- gcompare _ (StringValue _)                = GGT +instance (KnownSMTSort t, Num (HaskellType t)) => Num (Value t) where+  fromInteger = wrapValue . fromInteger+  {-# INLINE fromInteger #-}+  x + y = wrapValue $ unwrapValue x + unwrapValue y+  {-# INLINE (+) #-}+  x - y = wrapValue $ unwrapValue x - unwrapValue y+  {-# INLINE (-) #-}+  x * y = wrapValue $ unwrapValue x * unwrapValue y+  {-# INLINE (*) #-}+  negate = wrapValue . negate . unwrapValue+  {-# INLINE negate #-}+  abs = wrapValue . abs . unwrapValue+  {-# INLINE abs #-}+  signum = wrapValue . signum . unwrapValue+  {-# INLINE signum #-}++instance Fractional (Value RealSort) where+  fromRational = RealValue . fromRational+  {-# INLINE fromRational #-}+  (RealValue x) / (RealValue y) = RealValue $ x / y+  {-# INLINE (/) #-}++instance Boolean (Value BoolSort) where+  bool = BoolValue+  {-# INLINE bool #-}+  (BoolValue x) && (BoolValue y) = BoolValue $ x && y+  {-# INLINE (&&) #-}+  (BoolValue x) || (BoolValue y) = BoolValue $ x || y+  {-# INLINE (||) #-}+  not (BoolValue x) = BoolValue $ not x+  {-# INLINE not #-}+  xor (BoolValue x) (BoolValue y) = BoolValue $ x `xor` y+  {-# INLINE xor #-}+ -- | Unwraps a Haskell-value from the SMT-Context-'Value'. unwrapValue :: Value t -> HaskellType t unwrapValue (IntValue  v)   = v@@ -86,7 +128,7 @@ unwrapValue (BvValue   v)   = v unwrapValue (ArrayValue v)  = v unwrapValue (StringValue v) = v-{-# INLINEABLE unwrapValue #-}+{-# INLINE unwrapValue #-}  -- | Wraps a Haskell-value into the SMT-Context-'Value'. wrapValue :: forall t. KnownSMTSort t => HaskellType t -> Value t@@ -94,7 +136,7 @@   SIntSort       -> IntValue   SRealSort      -> RealValue   SBoolSort      -> BoolValue-  SBvSort _      -> BvValue+  SBvSort _ _    -> BvValue   SArraySort _ _ -> ArrayValue   SStringSort    -> StringValue-{-# INLINEABLE wrapValue #-}+{-# INLINE wrapValue #-}