hasmtlib 2.4.0 → 2.5.0

raw patch · 10 files changed

+663/−282 lines, 10 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +17/−0
• hasmtlib.cabal +2/−2
• src/Language/Hasmtlib.hs +2/−2
• src/Language/Hasmtlib/Codec.hs +4/−16
• src/Language/Hasmtlib/Integraled.hs +0/−43
• src/Language/Hasmtlib/Internal/Bitvec.hs +31/−25
• src/Language/Hasmtlib/Internal/Parser.hs +2/−2
• src/Language/Hasmtlib/Type/Expr.hs +500/−190
• src/Language/Hasmtlib/Type/SMTSort.hs +5/−2
• src/Language/Hasmtlib/Type/Value.hs +100/−0

@@ -6,6 +6,23 @@ 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.5.0 _(2024-08-25)_++### Added+- added instances `Eq`, `Ord`, `GEq` and `GCompare` for `Expr t`+- added instances `Real` and `Enum` for `Expr IntSort`, `Expr RealSort` and `Expr (BvSort n)`+- added instance `Integral` for `Expr IntSort` and `Expr (BvSort n)`+- added instance `Bits` for `Expr BoolSort` and `Expr (BvSort n)`++### Changed+- Removed `Language.Hasmtlib.Integraled`: use the added `Integral` instance instead+- Removed redundant BitVec constructors from `Expr` and replaced usage in instances with the more generic existing ones.+For example: Where `BvNot` was used previously, we now use `Not` which is already used for Expr BoolSort.+Differentiation between such operations now takes place in `Language.Hasmtlib.Internal.Render#render` when rendering expressions,+e.g. rendering `bvnot` for `BvSort` and `not` for `BoolSort`.+Therefore there is no behavioral change for the solver.+- Removed functions `bvRotL` and `bvRotR` from `Language.Hasmtlib.Type.Expr`: use the added `Bits` instance instead with `rotateL` and `rotateR`+ ## v2.4.0 _(2024-08-21)_  ### Added

@@ -1,7 +1,7 @@ cabal-version:         3.0  name:                  hasmtlib-version:               2.4.0+version:               2.5.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.@@ -32,7 +32,6 @@                      , Language.Hasmtlib.Boolean                      , Language.Hasmtlib.Variable                      , Language.Hasmtlib.Counting-                     , Language.Hasmtlib.Integraled                      , Language.Hasmtlib.Internal.Parser                      , Language.Hasmtlib.Internal.Bitvec                      , Language.Hasmtlib.Internal.Render@@ -47,6 +46,7 @@                      , Language.Hasmtlib.Solver.Yices                      , Language.Hasmtlib.Solver.Z3                      , Language.Hasmtlib.Type.Expr+                     , Language.Hasmtlib.Type.Value                      , Language.Hasmtlib.Type.MonadSMT                      , Language.Hasmtlib.Type.SMT                      , Language.Hasmtlib.Type.OMT

@@ -5,12 +5,12 @@   , module Language.Hasmtlib.Type.OMT   , module Language.Hasmtlib.Type.Pipe   , module Language.Hasmtlib.Type.Expr+  , module Language.Hasmtlib.Type.Value   , module Language.Hasmtlib.Type.Solver   , module Language.Hasmtlib.Type.Option   , module Language.Hasmtlib.Type.SMTSort   , module Language.Hasmtlib.Type.Solution   , module Language.Hasmtlib.Type.ArrayMap-  , module Language.Hasmtlib.Integraled   , module Language.Hasmtlib.Boolean   , module Language.Hasmtlib.Codec   , module Language.Hasmtlib.Counting@@ -30,12 +30,12 @@ import Language.Hasmtlib.Type.OMT import Language.Hasmtlib.Type.Pipe import Language.Hasmtlib.Type.Expr+import Language.Hasmtlib.Type.Value import Language.Hasmtlib.Type.Solver import Language.Hasmtlib.Type.Option import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Solution import Language.Hasmtlib.Type.ArrayMap-import Language.Hasmtlib.Integraled import Language.Hasmtlib.Boolean import Language.Hasmtlib.Codec import Language.Hasmtlib.Counting

@@ -15,6 +15,7 @@ import Data.Kind import Data.Coerce import qualified Data.List as List+import Data.Bits hiding (And, Xor, xor) import Data.Map (Map) import Data.Sequence (Seq) import Data.IntMap as IM hiding (foldl)@@ -74,6 +75,7 @@     return $ unwrapValue val   decode _ (Constant v)         = Just $ unwrapValue v   decode sol (Plus x y)         = (+)   <$> decode sol x <*> decode sol y+  decode sol (Minus x y)        = (-)   <$> decode sol x <*> decode sol y   decode sol (Neg x)            = fmap negate  (decode sol x)   decode sol (Mul x y)          = (*)   <$> decode sol x <*> decode sol y   decode sol (Abs x)            = fmap abs     (decode sol x)@@ -111,27 +113,13 @@   decode sol (ToInt x)          = fmap truncate   (decode sol x)   decode sol (IsInt x)          = fmap ((0 ==) . snd . properFraction) (decode sol x)   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 (BvNot x)          = fmap not (decode sol x)-  decode sol (BvAnd x y)        = (&&) <$> decode sol x <*> decode sol y-  decode sol (BvOr x y)         = (||) <$> decode sol x <*> decode sol y-  decode sol (BvXor x y)        = xor <$> decode sol x <*> decode sol y   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 (BvNeg x)          = fmap negate (decode sol x)-  decode sol (BvAdd x y)        = (+) <$> decode sol x <*> decode sol y-  decode sol (BvSub x y)        = (-) <$> decode sol x <*> decode sol y-  decode sol (BvMul x y)        = (*) <$> decode sol x <*> decode sol y-  decode sol (BvuDiv x y)       = div <$> decode sol x <*> decode sol y-  decode sol (BvuRem x y)       = rem <$> 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 (BvRotL i x)       = bvRotL i <$> decode sol x-  decode sol (BvRotR i x)       = bvRotR i <$> decode sol x-  decode sol (BvuLT x y)        = (<) <$> decode sol x <*> decode sol y-  decode sol (BvuLTHE x y)      = (<=) <$> decode sol x <*> decode sol y-  decode sol (BvuGTHE x y)      = (>=) <$> decode sol x <*> decode sol y-  decode sol (BvuGT x y)        = (>) <$> 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

@@ -1,43 +0,0 @@-{-# LANGUAGE DefaultSignatures #-}--module Language.Hasmtlib.Integraled where--import qualified Prelude as P-import Numeric.Natural  -import Data.Word-import Data.Functor.Identity-import Data.Functor.Const---- | 'P.Integral'-like class for clean API.---    In context hide the Preludes 'P.Integral'.  -class Integraled a where-  quot :: a -> a -> a-  n `quot` d          =  q  where (q,_) = quotRem n d-  -  rem :: a -> a -> a-  n `rem` d           =  r  where (_,r) = quotRem n d--  div :: a -> a -> a-  n `div` d           =  q  where (q,_) = divMod n d--  mod :: a -> a -> a-  n `mod` d           =  r  where (_,r) = divMod n d  --  quotRem :: a -> a -> (a, a)-  default quotRem :: P.Integral a => a -> a -> (a, a)-  quotRem = P.quotRem-  -  divMod  :: a -> a -> (a, a)-  default divMod  :: P.Integral a => a -> a -> (a, a)-  divMod = P.quotRem-  -instance Integraled P.Int-instance Integraled P.Integer-instance Integraled P.Word-instance Integraled Natural-instance Integraled Word8-instance Integraled Word16-instance Integraled Word32-instance Integraled Word64-instance P.Integral a => Integraled (Identity a)-instance P.Integral a => Integraled (Const a b)

@@ -3,13 +3,14 @@  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+import Data.Finite hiding (shift) import Data.Proxy import Data.Ratio ((%)) import Data.Bifunctor@@ -18,9 +19,22 @@  -- | Unsigned and length-indexed bitvector with MSB first. newtype Bitvec (n :: Nat) = Bitvec { unBitvec :: V.Vector n Bit }-  deriving stock (Eq, Ord)-  deriving newtype (Boolean)+  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) @@ -29,17 +43,17 @@   {-# INLINEABLE render #-}  instance KnownNat n => Num (Bitvec n) where-   fromInteger x = coerce . V.reverse $ V.generate @n (coerce . testBit x . fromInteger . getFinite) +   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     -     +   (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     +  minBound = coerce $ V.replicate @n false+  maxBound = coerce $ V.replicate @n true  instance KnownNat n => Enum (Bitvec n) where   succ x   = x + 1@@ -87,28 +101,20 @@ bvFromListN' :: forall n. KnownNat n => Proxy n -> [Bit] -> Maybe (Bitvec n) bvFromListN' _ = bvFromListN -bvRotL :: forall n i. KnownNat (Mod i n) => Proxy i -> Bitvec n -> Bitvec n-bvRotL _ (coerce -> x) = coerce $ r V.++ l-  where-    (l, r) = V.splitAt' (Proxy @(Mod i n)) x--bvRotR :: forall n i. KnownNat (Mod i n) => Proxy i -> Bitvec n -> Bitvec n-bvRotR p = bvReverse . bvRotL p . bvReverse- 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 -    +  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 -  +  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. +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)

@@ -144,14 +144,14 @@                       <|> binary "bvand" (&&)  <|> binary "bvor" (||) <|> binary "bvxor" xor <|> binary "bvnand" BvNand <|> binary "bvnor" BvNor                       <|> unary  "bvneg" negate                       <|> binary "bvadd" (+)  <|> binary "bvsub" (-) <|> binary "bvmul" (*)-                      <|> binary "bvudiv" BvuDiv <|> binary "bvurem" BvuRem+                      <|> binary "bvudiv" div <|> binary "bvurem" rem                       <|> binary "bvshl" BvShL <|> binary "bvlshr" BvLShR               SArraySort _ _ -> ternary "store" ArrStore                       -- TODO: Add compare ops for all (?) array-sorts               SStringSort -> binary "str.++" (<>) <|> binary "str.at" strAt <|> ternary "str.substr" StrSubstring                       <|> ternary "str.replace" strReplace <|> ternary "str.replace_all" strReplaceAll -var :: Parser (Expr t)+var :: KnownSMTSort t => Parser (Expr t) var = do   _     <- string "var_"   vId <- decimal @Int

@@ -5,23 +5,36 @@ {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE DerivingStrategies #-} -module Language.Hasmtlib.Type.Expr where+module Language.Hasmtlib.Type.Expr+  ( SMTVar(..), varId+  , Value(..) , unwrapValue, wrapValue+  , Expr(..), isLeaf+  , Iteable(..), Equatable(..), Orderable(..), min', max'+  , equal, distinct+  , for_all, exists+  , select, store+  , bvShL, bvLShR, bvConcat+  , toRealSort, toIntSort, isIntSort+  , strLength, strAt, strSubstring, strPrefixOf, strSuffixOf, strContains, strIndexOf, strReplace, strReplaceAll+  )+where -import Prelude hiding (Integral(..), not, and, or, any, all, (&&), (||))-import Language.Hasmtlib.Internal.Render+import Prelude hiding (not, and, or, any, all, (&&), (||)) import Language.Hasmtlib.Internal.Uniplate1+import Language.Hasmtlib.Internal.Render import Language.Hasmtlib.Type.ArrayMap import Language.Hasmtlib.Type.SMTSort-import Language.Hasmtlib.Integraled+import Language.Hasmtlib.Type.Value import Language.Hasmtlib.Boolean import Data.GADT.Compare import Data.GADT.DeepSeq import Data.Map hiding (toList)-import Data.Proxy import Data.Coerce+import Data.Proxy import Data.Int import Data.Word import Data.Void+import qualified Data.Bits as Bits import Data.Sequence (Seq) import Data.Tree (Tree) import Data.Monoid (Sum, Product, First, Last, Dual)@@ -44,83 +57,33 @@   deriving newtype (Eq, Ord) $(makeLenses ''SMTVar) --- | A wrapper for values of 'SMTSort's.-data Value (t :: SMTSort) where-  IntValue    :: HaskellType IntSort    -> Value IntSort-  RealValue   :: HaskellType RealSort   -> Value RealSort-  BoolValue   :: HaskellType BoolSort   -> Value BoolSort-  BvValue     :: KnownNat n => HaskellType (BvSort n) -> Value (BvSort n)-  ArrayValue  :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Eq (HaskellType v)) => HaskellType (ArraySort k v) -> Value (ArraySort k v)-  StringValue :: HaskellType StringSort -> Value StringSort--deriving instance Eq (HaskellType t) => Eq (Value t)-deriving instance Ord (HaskellType t) => Ord (Value t)--instance GEq Value where-  geq (BoolValue x) (BoolValue y)   = if x == y then Just Refl else Nothing-  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-    _   -> Nothing-  geq ax@(ArrayValue x) ay@(ArrayValue y) = case geq (sortSing' ax) (sortSing' ay) of-    Nothing -> Nothing-    Just Refl -> if x == y then Just Refl else Nothing-  geq (StringValue x) (StringValue y) = if x == y then Just Refl else Nothing-  geq _ _ = Nothing---- | Unwrap a value from 'Value'.-unwrapValue :: Value t -> HaskellType t-unwrapValue (IntValue  v)   = v-unwrapValue (RealValue v)   = v-unwrapValue (BoolValue v)   = v-unwrapValue (BvValue   v)   = v-unwrapValue (ArrayValue v)  = v-unwrapValue (StringValue v) = v-{-# INLINEABLE unwrapValue #-}---- | Wrap a value into 'Value'.-wrapValue :: forall t. KnownSMTSort t => HaskellType t -> Value t-wrapValue = case sortSing @t of-  SIntSort       -> IntValue-  SRealSort      -> RealValue-  SBoolSort      -> BoolValue-  SBvSort _      -> BvValue-  SArraySort _ _ -> ArrayValue-  SStringSort    -> StringValue-{-# INLINEABLE wrapValue #-}---- | An existential wrapper that hides some known 'SMTSort'.-type SomeKnownSMTSort f = SomeSMTSort '[KnownSMTSort] f---- | Am SMT expression.---   For internal use only.---   For building expressions use the corresponding instances (Num, Boolean, ...).+-- | An SMT-Expression.+--   For building expressions use the corresponding instances: 'Boolean', 'Num', 'Equatable', ...+--+--   With a lot of criminal energy you may build invalid expressions regarding the SMTLib Version 2.6 - Specification.+--   Therefore it is highly recommended to rely on the instances. data Expr (t :: SMTSort) where-  Var       :: SMTVar t -> Expr t-  Constant  :: Value  t -> Expr t-+  Var       :: KnownSMTSort t => SMTVar t -> Expr t+  Constant  :: Value t -> Expr t   Plus      :: Num (HaskellType t) => Expr t -> Expr t -> Expr t+  Minus     :: Num (HaskellType t) => Expr t -> Expr t -> Expr t   Neg       :: Num (HaskellType t) => Expr t -> Expr t   Mul       :: Num (HaskellType t) => Expr t -> Expr t -> Expr t   Abs       :: Num (HaskellType t) => Expr t -> Expr t-  Mod       :: Expr IntSort  -> Expr IntSort  -> Expr IntSort-  IDiv      :: Expr IntSort  -> Expr IntSort  -> Expr IntSort+  Mod       :: 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   LTHE      :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort   EQU       :: (Eq (HaskellType t), KnownSMTSort t, KnownNat n) => V.Vector (n + 2) (Expr t) -> Expr BoolSort   Distinct  :: (Eq (HaskellType t), KnownSMTSort t, KnownNat n) => V.Vector (n + 2) (Expr t) -> Expr BoolSort   GTHE      :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort   GTH       :: (Ord (HaskellType t), KnownSMTSort t) => Expr t -> Expr t -> Expr BoolSort-   Not       :: Boolean (HaskellType t) => Expr t -> Expr t   And       :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t   Or        :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t   Impl      :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t   Xor       :: Boolean (HaskellType t) => Expr t -> Expr t -> Expr t-   Pi        :: Expr RealSort   Sqrt      :: Expr RealSort -> Expr RealSort   Exp       :: Expr RealSort -> Expr RealSort@@ -130,38 +93,19 @@   Asin      :: Expr RealSort -> Expr RealSort   Acos      :: Expr RealSort -> Expr RealSort   Atan      :: Expr RealSort -> Expr RealSort-   ToReal    :: Expr IntSort  -> Expr RealSort   ToInt     :: Expr RealSort -> Expr IntSort   IsInt     :: Expr RealSort -> Expr BoolSort-   Ite       :: Expr BoolSort -> Expr t -> Expr t -> Expr t--  BvNot     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n)-  BvAnd     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)-  BvOr      :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)-  BvXor     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)   BvNand    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)   BvNor     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)-  BvNeg     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n)-  BvAdd     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)-  BvSub     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)-  BvMul     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)-  BvuDiv    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)-  BvuRem    :: 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, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)-  BvRotR    :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)-  BvuLT     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort-  BvuLTHE   :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort-  BvuGTHE   :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort-  BvuGT     :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr BoolSort--  ArrSelect :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Eq (HaskellType v)) => Expr (ArraySort k v) -> Expr k -> Expr v+  BvRotL    :: (KnownNat n, Integral a) => a -> Expr (BvSort n) -> Expr (BvSort n)+  BvRotR    :: (KnownNat n, Integral a) => a -> Expr (BvSort n) -> Expr (BvSort 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@@ -387,13 +331,13 @@   {-# INLINE (>?) #-}  instance KnownNat n => Orderable (Expr (BvSort n)) where-  (<?)     = BvuLT+  (<?)     = LTH   {-# INLINE (<?) #-}-  (<=?)    = BvuLTHE+  (<=?)    = LTHE   {-# INLINE (<=?) #-}-  (>=?)    = BvuGTHE+  (>=?)    = GTHE   {-# INLINE (>=?) #-}-  (>?)     = BvuGT+  (>?)     = GTH   {-# INLINE (>?) #-}  -- | Lexicographic ordering for '(<?)' and reflexive closure of lexicographic ordering for '(<=?)'@@ -551,7 +495,7 @@ {-# INLINE exists #-}  -- | Select a value from an array.-select :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Eq (HaskellType v)) => Expr (ArraySort k v) -> Expr k -> Expr v+select :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => Expr (ArraySort k v) -> Expr k -> Expr v select = ArrSelect {-# INLINE select #-} @@ -575,16 +519,6 @@ bvConcat = BvConcat {-# INLINE bvConcat #-} --- | Rotate bitvector left-bvRotL   :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)-bvRotL   = BvRotL-{-# INLINE bvRotL #-}---- | Rotate bitvector right-bvRotR   :: (KnownNat n, KnownNat i, KnownNat (Mod i n)) => Proxy i -> Expr (BvSort n) -> Expr (BvSort n)-bvRotR   = BvRotR-{-# INLINE bvRotR #-}- -- | Converts an expression of type 'IntSort' to type 'RealSort'. toRealSort :: Expr IntSort  -> Expr RealSort toRealSort = ToReal@@ -672,7 +606,7 @@    {-# INLINE (+) #-}    x - (Constant (IntValue 0)) = x    (Constant (IntValue x)) - (Constant (IntValue y)) = Constant (IntValue (x - y))-   x - y = Plus x (Neg y)+   x - y = Minus x y    {-# INLINE (-) #-}    (Constant (IntValue 0)) * _ = 0    _ * (Constant (IntValue 0)) = 0@@ -698,7 +632,7 @@    {-# INLINE (+) #-}    x - (Constant (RealValue 0)) = x    (Constant (RealValue x)) - (Constant (RealValue y)) = Constant (RealValue (x - y))-   x - y = Plus x (Neg y)+   x - y = Minus x y    {-# INLINE (-) #-}    (Constant (RealValue 0)) * _ = 0    _ * (Constant (RealValue 0)) = 0@@ -720,18 +654,18 @@    (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+   x + y = Plus x y    {-# INLINE (+) #-}    x - (Constant (BvValue 0)) = x    (Constant (BvValue x)) - (Constant (BvValue y)) = Constant (BvValue (x - y))-   x - y = BvSub 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 = BvMul x y+   x * y = Mul x y    {-# INLINE (*) #-}    abs         = id    {-# INLINE abs #-}@@ -775,7 +709,22 @@     acosh = error "SMT-Solvers currently do not support acosh"     atanh = error "SMT-Solvers currently do not support atanh" -instance Integraled (Expr IntSort) where+-- | 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 'toEnum', 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@@ -788,20 +737,55 @@   {-# 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 #-} -instance KnownNat n => Integraled (Expr (BvSort n)) where-  quot        = BvuDiv+-- | 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 'toEnum', 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+  {-# INLINE toRational #-}++-- | This instance is __partial__ for 'toEnum', 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+  {-# INLINE fromEnum #-}+  toEnum = fromInteger . fromIntegral+  {-# 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         = BvuRem+  rem         = Mod   {-# INLINE rem #-}-  div         = BvuDiv+  div         = IDiv   {-# INLINE div #-}-  mod         = BvuRem+  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 (BvValue x)) = fromIntegral x+  toInteger x = error $ "Integer#toInteger[Expr BvSort] only supported for constants. But given: " <> show x+  {-# INLINE toInteger #-}  instance Boolean (Expr BoolSort) where   bool = Constant . BoolValue@@ -820,23 +804,105 @@ instance KnownNat n => Boolean (Expr (BvSort n)) where   bool = Constant . BvValue . bool   {-# INLINE bool #-}-  (&&) = BvAnd+  (&&) = And   {-# INLINE (&&) #-}-  (||) = BvOr+  (||) = Or   {-# INLINE (||) #-}-  not  = BvNot+  not  = Not   {-# INLINE not #-}-  xor  = BvXor+  xor  = Xor   {-# INLINE xor #-}  instance Bounded (Expr BoolSort) where   minBound = false+  {-# INLINE minBound #-}   maxBound = true+  {-# INLINE maxBound #-}  instance KnownNat n => Bounded (Expr (BvSort n)) where   minBound = Constant $ BvValue minBound+  {-# INLINE minBound #-}   maxBound = Constant $ BvValue maxBound+  {-# INLINE maxBound #-} +-- | This instance is __partial__ for 'testBit' and 'popCount', it's only intended for use with constants ('Constant').+instance Bits.Bits (Expr BoolSort) where+  (.&.) = And+  {-# INLINE (.&.) #-}+  (.|.) = Or+  {-# INLINE (.|.) #-}+  xor = Xor+  {-# INLINE xor #-}+  complement = Not+  {-# INLINE complement #-}+  zeroBits = false+  {-# INLINE zeroBits #-}+  bit _ = true+  {-# INLINE bit #-}+  setBit _ _ = true+  {-# INLINE setBit #-}+  clearBit _ _ = false+  {-# INLINE clearBit #-}+  complementBit b _ = Not b+  {-# INLINE complementBit #-}+  testBit (Constant (BoolValue b)) _ = b+  testBit sb _ = error $ "Bits#testBit[Expr BoolSort] is only supported for constants. Given: " <> show sb+  {-# INLINE testBit #-}+  bitSizeMaybe _ = Just 1+  {-# INLINE bitSizeMaybe #-}+  bitSize _ = 1+  {-# INLINE bitSize #-}+  isSigned _ = False+  {-# INLINE isSigned #-}+  shiftL b 0 = b+  shiftL _ _ = false+  {-# INLINE shiftL #-}+  shiftR b 0 = b+  shiftR _ _ = false+  {-# INLINE shiftR #-}+  rotateL b _ = b+  {-# INLINE rotateL #-}+  rotateR b _ = b+  {-# INLINE rotateR #-}+  popCount (Constant (BoolValue b)) = if b then 1 else 0+  popCount sb = error $ "Bits#popCount[Expr BoolSort] is only supported for constants. Given: " <> show sb+  {-# 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+  (.&.) = And+  {-# INLINE (.&.) #-}+  (.|.) = Or+  {-# INLINE (.|.) #-}+  xor = Xor+  {-# INLINE xor #-}+  complement = Not+  {-# INLINE complement #-}+  zeroBits = false+  {-# INLINE zeroBits #-}+  bit = Constant . BvValue . Bits.bit+  {-# INLINE bit #-}+  testBit (Constant (BvValue b)) i = Bits.testBit b i+  testBit sb _ = error $ "Bits#testBit[Expr BvSort] is only supported for constants. Given: " <> show sb+  {-# INLINE testBit #-}+  bitSizeMaybe _ = Just $ fromIntegral $ natVal $ Proxy @n+  {-# INLINE bitSizeMaybe #-}+  bitSize _ = fromIntegral $ natVal $ Proxy @n+  {-# INLINE bitSize #-}+  isSigned _ = False+  {-# INLINE isSigned #-}+  shiftL b i = BvShL b (fromIntegral i)+  {-# INLINE shiftL #-}+  shiftR b i = BvLShR b (fromIntegral i)+  {-# INLINE shiftR #-}+  rotateL b i = BvRotL i b+  {-# INLINE rotateL #-}+  rotateR b i = BvRotR i b+  {-# INLINE rotateR #-}+  popCount (Constant (BvValue b)) = Bits.popCount b+  popCount sb = error $ "Bits#popCount[Expr BvSort] is only supported for constants. Given: " <> show sb+  {-# INLINE popCount #-}+ instance Semigroup (Expr StringSort) where   (<>) = StrConcat   {-# INLINE (<>) #-}@@ -867,7 +933,7 @@       | otherwise  -> constRender v     where       constRender v = "((as const " <> render (goSing arr) <> ") " <> render (wrapValue v) <> ")"-      goSing :: forall k v. (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Eq (HaskellType v)) => ConstArray (HaskellType k) (HaskellType v) -> SSMTSort (ArraySort k v)+      goSing :: forall k v. (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => ConstArray (HaskellType k) (HaskellType v) -> SSMTSort (ArraySort k v)       goSing _ = sortSing @(ArraySort k v)   render (StringValue x) = "\"" <> render x <> "\"" @@ -875,26 +941,27 @@   render (Var v)      = render v   render (Constant c) = render c -  render (Plus x y)   = renderBinary "+" x y-  render (Neg x)      = renderUnary  "-" x-  render (Mul x y)    = renderBinary "*" 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 "mod" x y-  render (IDiv x y)   = renderBinary "div" x y+  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 (Div x y)    = renderBinary "/" x y -  render (LTH x y)    = renderBinary "<" x y-  render (LTHE 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 (EQU xs)     = renderNary "=" $ V.toList xs   render (Distinct xs)= renderNary "distinct" $ V.toList xs-  render (GTHE x y)   = renderBinary ">=" x y-  render (GTH x y)    = renderBinary ">" x y+  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  "not" x-  render (And x y)    = renderBinary "and" x y-  render (Or x y)     = renderBinary "or" 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 "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@@ -912,27 +979,13 @@    render (Ite p t f)  = renderTernary "ite" p t f -  render (BvNot x)          = renderUnary  "bvnot"  (render x)-  render (BvAnd x y)        = renderBinary "bvand"  (render x) (render y)-  render (BvOr x y)         = renderBinary "bvor"   (render x) (render y)-  render (BvXor x y)        = renderBinary "bvxor"  (render x) (render y)   render (BvNand x y)       = renderBinary "bvnand" (render x) (render y)   render (BvNor x y)        = renderBinary "bvnor"  (render x) (render y)-  render (BvNeg x)          = renderUnary  "bvneg"  (render x)-  render (BvAdd x y)        = renderBinary "bvadd"  (render x) (render y)-  render (BvSub x y)        = renderBinary "bvsub"  (render x) (render y)-  render (BvMul x y)        = renderBinary "bvmul"  (render x) (render y)-  render (BvuDiv x y)       = renderBinary "bvudiv" (render x) (render y)-  render (BvuRem x y)       = renderBinary "bvurem" (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 (BvConcat x y)     = renderBinary "concat" (render x) (render y)-  render (BvRotL i x)       = renderUnary (renderBinary "_" ("rotate_left"  :: Builder) (render (natVal i))) (render x)-  render (BvRotR i x)       = renderUnary (renderBinary "_" ("rotate_right" :: Builder) (render (natVal i))) (render x)-  render (BvuLT x y)        = renderBinary "bvult"  (render x) (render y)-  render (BvuLTHE x y)      = renderBinary "bvule"  (render x) (render y)-  render (BvuGTHE x y)      = renderBinary "bvuge"  (render x) (render y)-  render (BvuGT x y)        = renderBinary "bvugt"  (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)@@ -1006,7 +1059,7 @@ type instance Index   (Expr (ArraySort k v)) = Expr k type instance IxValue (Expr (ArraySort k v)) = Expr v -instance (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Eq (HaskellType v)) => Ixed (Expr (ArraySort k v)) where+instance (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => Ixed (Expr (ArraySort k v)) where   ix i f arr = f (select arr i) <&> store arr i  -- | __Caution for quantified expressions:__ 'uniplate1' will only be applied if quantification has taken place already.@@ -1014,6 +1067,7 @@   uniplate1 _ expr@(Var _)            = pure expr   uniplate1 _ expr@(Constant _)       = pure expr   uniplate1 f (Plus x y)              = Plus <$> f x <*> f y+  uniplate1 f (Minus x y)             = Minus <$> f x <*> f y   uniplate1 f (Neg x)                 = Neg <$> f x   uniplate1 f (Mul x y)               = Mul <$> f x <*> f y   uniplate1 f (Abs x)                 = Abs <$> f x@@ -1044,27 +1098,13 @@   uniplate1 f (ToInt x)               = ToInt <$> f x   uniplate1 f (IsInt x)               = IsInt <$> f x   uniplate1 f (Ite p t n)             = Ite <$> f p <*> f t <*> f n-  uniplate1 f (BvNot x)               = BvNot <$> f x-  uniplate1 f (BvAnd x y)             = BvAnd <$> f x <*> f y-  uniplate1 f (BvOr x y)              = BvOr <$> f x <*> f y-  uniplate1 f (BvXor x y)             = BvXor <$> f x <*> f y   uniplate1 f (BvNand x y)            = BvNand <$> f x <*> f y   uniplate1 f (BvNor x y)             = BvNor <$> f x <*> f y-  uniplate1 f (BvNeg x)               = BvNeg <$> f x-  uniplate1 f (BvAdd x y)             = BvAdd <$> f x <*> f y-  uniplate1 f (BvSub x y)             = BvSub <$> f x <*> f y-  uniplate1 f (BvMul x y)             = BvMul <$> f x <*> f y-  uniplate1 f (BvuDiv x y)            = BvuDiv <$> f x <*> f y-  uniplate1 f (BvuRem x y)            = BvuRem <$> 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 (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-  uniplate1 f (BvuLT x y)             = BvuLT <$> f x <*> f y-  uniplate1 f (BvuLTHE x y)           = BvuLTHE <$> f x <*> f y-  uniplate1 f (BvuGTHE x y)           = BvuGTHE <$> f x <*> f y-  uniplate1 f (BvuGT x y)             = BvuGT <$> f x <*> f y   uniplate1 f (ArrSelect i arr)       = ArrSelect i <$> f arr   uniplate1 f (ArrStore i x arr)      = ArrStore i <$> f x <*> f arr   uniplate1 f (StrConcat x y)         = StrConcat <$> f x <*> f y@@ -1095,6 +1135,7 @@           Var _                -> pure expr           Constant _           -> pure expr           Plus x y             -> Plus <$> tryPlate f' x <*> tryPlate f' y+          Minus x y            -> Minus <$> tryPlate f' x <*> tryPlate f' y           Neg x                -> Neg  <$> tryPlate f' x           Mul x y              -> Mul  <$> tryPlate f' x <*> tryPlate f' y           Abs x                -> Abs  <$> tryPlate f' x@@ -1125,27 +1166,13 @@           ToInt x              -> ToInt  <$> tryPlate f' x           IsInt x              -> IsInt  <$> tryPlate f' x           Ite p t n            -> Ite    <$> tryPlate f' p <*> tryPlate f' t <*> tryPlate f' n-          BvNot x              -> BvNot  <$> tryPlate f' x-          BvAnd x y            -> BvAnd  <$> tryPlate f' x <*> tryPlate f' y-          BvOr x y             -> BvOr   <$> tryPlate f' x <*> tryPlate f' y-          BvXor x y            -> BvXor  <$> tryPlate f' x <*> tryPlate f' y           BvNand x y           -> BvNand <$> tryPlate f' x <*> tryPlate f' y           BvNor x y            -> BvNor  <$> tryPlate f' x <*> tryPlate f' y-          BvNeg x              -> BvNeg  <$> tryPlate f' x-          BvAdd x y            -> BvAdd  <$> tryPlate f' x <*> tryPlate f' y-          BvSub x y            -> BvSub  <$> tryPlate f' x <*> tryPlate f' y-          BvMul x y            -> BvMul  <$> tryPlate f' x <*> tryPlate f' y-          BvuDiv x y           -> BvuDiv <$> tryPlate f' x <*> tryPlate f' y-          BvuRem x y           -> BvuRem <$> 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           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-          BvuLT x y            -> BvuLT    <$> tryPlate f' x <*> tryPlate f' y-          BvuLTHE x y          -> BvuLTHE  <$> tryPlate f' x <*> tryPlate f' y-          BvuGTHE x y          -> BvuGTHE  <$> tryPlate f' x <*> tryPlate f' y-          BvuGT x y            -> BvuGT    <$> tryPlate f' x <*> tryPlate f' y           ArrSelect i arr      -> ArrSelect i   <$> tryPlate f' arr           ArrStore i x arr     -> ArrStore i    <$> tryPlate f' x <*> tryPlate f' arr           StrConcat x y        -> StrConcat     <$> tryPlate f' x <*> tryPlate f' y@@ -1170,6 +1197,7 @@     Var (SMTVar vId)     -> vId `seq` ()     Constant c           -> c `seq` ()     Plus e1 e2           -> grnf e1 `seq` grnf e2+    Minus e1 e2          -> grnf e1 `seq` grnf e2     Neg e                -> grnf e     Mul e1 e2            -> grnf e1 `seq` grnf e2     Abs e                -> grnf e@@ -1200,27 +1228,13 @@     ToInt e              -> grnf e     IsInt e              -> grnf e     Ite c e1 e2          -> grnf c `seq` grnf e1 `seq` grnf e2-    BvNot e              -> grnf e-    BvAnd e1 e2          -> grnf e1 `seq` grnf e2-    BvOr e1 e2           -> grnf e1 `seq` grnf e2-    BvXor e1 e2          -> grnf e1 `seq` grnf e2     BvNand e1 e2         -> grnf e1 `seq` grnf e2     BvNor e1 e2          -> grnf e1 `seq` grnf e2-    BvNeg e              -> grnf e-    BvAdd e1 e2          -> grnf e1 `seq` grnf e2-    BvSub e1 e2          -> grnf e1 `seq` grnf e2-    BvMul e1 e2          -> grnf e1 `seq` grnf e2-    BvuDiv e1 e2         -> grnf e1 `seq` grnf e2-    BvuRem e1 e2         -> grnf e1 `seq` grnf e2     BvShL e1 e2          -> grnf e1 `seq` grnf e2     BvLShR e1 e2         -> grnf e1 `seq` grnf e2     BvConcat e1 e2       -> grnf e1 `seq` grnf e2     BvRotL _ e           -> grnf e     BvRotR _ e           -> grnf e-    BvuLT e1 e2          -> grnf e1 `seq` grnf e2-    BvuLTHE e1 e2        -> grnf e1 `seq` grnf e2-    BvuGTHE e1 e2        -> grnf e1 `seq` grnf e2-    BvuGT e1 e2          -> grnf e1 `seq` grnf e2     ArrSelect e1 e2      -> grnf e1 `seq` grnf e2     ArrStore e1 e2 e3    -> grnf e1 `seq` grnf e2 `seq` grnf e3     StrConcat e1 e2      -> grnf e1 `seq` grnf e2@@ -1239,3 +1253,299 @@     ForAll (Just qv) f   -> grnf $ f $ Var qv     Exists Nothing _     -> ()     Exists (Just qv) f   -> grnf $ f $ Var qv++instance Eq (Expr t) where+  (==) = defaultEq++instance Ord (Expr t) where+  compare = defaultCompare++instance GEq Expr where+  geq = defaultGeq++gcomparing :: GCompare f => [(f a, f b)] -> GOrdering a b+gcomparing [] = GLT+gcomparing ((x,y):xys) = case gcompare x y of+  GEQ -> gcomparing xys+  o -> o++instance GCompare Expr where+  gcompare (Var v) (Var v') = case gcompare (sortSing' v) (sortSing' v') of+    GLT -> GLT+    GEQ -> case compare (coerce @_ @Int v) (coerce v') of+      LT -> GLT+      EQ -> GEQ+      GT -> GGT+    GGT -> GGT+  gcompare (Var _) _ = GLT+  gcompare _ (Var _) = GGT+  gcompare (Constant c) (Constant c') = gcompare c c'+  gcompare (Constant _) _ = GLT+  gcompare _ (Constant _) = GGT+  gcompare (Plus x y) (Plus x' y') = gcomparing [(x,x'), (y,y')]+  gcompare (Plus _ _) _ = GLT+  gcompare _ (Plus _ _) = GGT+  gcompare (Minus x y) (Minus x' y') = gcomparing [(x,x'), (y,y')]+  gcompare (Minus _ _) _ = GLT+  gcompare _ (Minus _ _) = GGT+  gcompare (Neg x) (Neg x') = gcompare x x'+  gcompare (Neg _) _ = GLT+  gcompare _ (Neg _) = GGT+  gcompare (Mul x y) (Mul x' y') = gcomparing [(x,x'), (y,y')]+  gcompare (Mul _ _) _ = GLT+  gcompare _ (Mul _ _) = GGT+  gcompare (Abs x) (Abs x') = gcompare x x'+  gcompare (Abs _) _ = GLT+  gcompare _ (Abs _) = GGT+  gcompare (Mod x y) (Mod x' y') = gcomparing [(x,x'), (y,y')]+  gcompare (Mod _ _) _ = GLT+  gcompare _ (Mod _ _) = GGT+  gcompare (IDiv x y) (IDiv x' y') = gcomparing [(x,x'), (y,y')]+  gcompare (IDiv _ _) _ = GLT+  gcompare _ (IDiv _ _) = GGT+  gcompare (Div x y) (Div x' y') = gcomparing [(x,x'), (y,y')]+  gcompare (Div _ _) _ = GLT+  gcompare _ (Div _ _) = GGT+  gcompare (LTH x y)               (LTH x' y')             = case gcomparing [(x,x'), (y,y')] of+    GLT -> GLT+    GEQ -> GEQ+    GGT -> GGT+  gcompare (LTH _ _) _ = GLT+  gcompare _ (LTH _ _) = GGT+  gcompare (LTHE x y)              (LTHE x' y')            = case gcomparing [(x,x'), (y,y')] of+    GLT -> GLT+    GEQ -> GEQ+    GGT -> GGT+  gcompare (LTHE _ _) _ = GLT+  gcompare _ (LTHE _ _) = GGT+  gcompare (EQU (V.toList -> xs))  (EQU (V.toList -> xs')) = case compare (length xs ) (length xs') of+    LT -> GLT+    EQ -> case gcomparing $ zip xs xs' of+      GGT -> GGT+      GEQ -> GEQ+      GLT -> GLT+    GT -> GGT+  gcompare (EQU _) _ = GLT+  gcompare _ (EQU _) = GGT+  gcompare (Distinct (V.toList -> xs)) (Distinct (V.toList -> xs')) = case compare (length xs ) (length xs') of+    LT -> GLT+    EQ -> case gcomparing $ zip xs xs' of+      GGT -> GGT+      GEQ -> GEQ+      GLT -> GLT+    GT -> GGT+  gcompare (Distinct _) _ = GLT+  gcompare _ (Distinct _) = GGT+  gcompare (GTHE x y)              (GTHE x' y')            = case gcomparing [(x,x'), (y,y')] of+    GLT -> GLT+    GEQ -> GEQ+    GGT -> GGT+  gcompare (GTHE _ _) _ = GLT+  gcompare _ (GTHE _ _) = GGT+  gcompare (GTH x y)               (GTH x' y')             = case gcomparing [(x,x'), (y,y')] of+    GLT -> GLT+    GEQ -> GEQ+    GGT -> GGT+  gcompare (GTH _ _) _ = GLT+  gcompare _ (GTH _ _) = GGT+  gcompare (Not x)                 (Not x')                = gcompare x x'+  gcompare (Not _) _ = GLT+  gcompare _ (Not _) = GGT+  gcompare (And x y)               (And x' y')             = gcomparing [(x,x'), (y,y')]+  gcompare (And _ _) _ = GLT+  gcompare _ (And _ _) = GGT+  gcompare (Or x y)                (Or x' y')              = gcomparing [(x,x'), (y,y')]+  gcompare (Or _ _) _ = GLT+  gcompare _ (Or _ _) = GGT+  gcompare (Impl x y)              (Impl x' y')            = gcomparing [(x,x'), (y,y')]+  gcompare (Impl _ _) _ = GLT+  gcompare _ (Impl _ _) = GGT+  gcompare (Xor x y)               (Xor x' y')             = gcomparing [(x,x'), (y,y')]+  gcompare (Xor _ _) _ = GLT+  gcompare _ (Xor _ _) = GGT+  gcompare Pi                      Pi                      = GEQ+  gcompare Pi _ = GLT+  gcompare _ Pi = GGT+  gcompare (Sqrt x)                (Sqrt x')               = gcompare x x'+  gcompare (Sqrt _) _ = GLT+  gcompare _ (Sqrt _) = GGT+  gcompare (Exp x)                 (Exp x')                = gcompare x x'+  gcompare (Exp _) _ = GLT+  gcompare _ (Exp _) = GGT+  gcompare (Sin x)                 (Sin x')                = gcompare x x'+  gcompare (Sin _) _ = GLT+  gcompare _ (Sin _) = GGT+  gcompare (Cos x)                 (Cos x')                = gcompare x x'+  gcompare (Cos _) _ = GLT+  gcompare _ (Cos _) = GGT+  gcompare (Tan x)                 (Tan x')                = gcompare x x'+  gcompare (Tan _) _ = GLT+  gcompare _ (Tan _) = GGT+  gcompare (Asin x)                (Asin x')               = gcompare x x'+  gcompare (Asin _) _ = GLT+  gcompare _ (Asin _) = GGT+  gcompare (Acos x)                (Acos x')               = gcompare x x'+  gcompare (Acos _) _ = GLT+  gcompare _ (Acos _) = GGT+  gcompare (Atan x)                (Atan x')               = gcompare x x'+  gcompare (Atan _) _ = GLT+  gcompare _ (Atan _) = GGT+  gcompare (ToReal x)              (ToReal x')             = case gcompare x x' of+    GLT -> GLT+    GEQ -> GEQ+    GGT -> GGT+  gcompare (ToReal _) _ = GLT+  gcompare _ (ToReal _) = GGT+  gcompare (ToInt x)               (ToInt x')              = case gcompare x x' of+    GLT -> GLT+    GEQ -> GEQ+    GGT -> GGT+  gcompare (ToInt _) _ = GLT+  gcompare _ (ToInt _) = GGT+  gcompare (IsInt x)               (IsInt x')              = case gcompare x x' of+    GLT -> GLT+    GEQ -> GEQ+    GGT -> GGT+  gcompare (IsInt _) _ = GLT+  gcompare _ (IsInt _) = GGT+  gcompare (Ite p t n)             (Ite p' t' n')          = case gcompare p p' of+    GLT -> GLT+    GEQ -> gcomparing [(t,t'), (n,n')]+    GGT -> GGT+  gcompare (Ite _ _ _) _ = GLT+  gcompare _ (Ite _ _ _) = GGT+  gcompare (BvNand x y)            (BvNand x' y')          = gcomparing [(x,x'), (y,y')]+  gcompare (BvNand _ _) _ = GLT+  gcompare _ (BvNand _ _) = GGT+  gcompare (BvNor x y)             (BvNor x' y')           = gcomparing [(x,x'), (y,y')]+  gcompare (BvNor _ _) _ = GLT+  gcompare _ (BvNor _ _) = GGT+  gcompare (BvShL x y)             (BvShL x' y')           = gcomparing [(x,x'), (y,y')]+  gcompare (BvShL _ _) _ = GLT+  gcompare _ (BvShL _ _) = GGT+  gcompare (BvLShR x y)            (BvLShR x' y')          = gcomparing [(x,x'), (y,y')]+  gcompare (BvLShR _ _) _ = GLT+  gcompare _ (BvLShR _ _) = GGT+  gcompare (BvConcat x y)          (BvConcat x' y')        = case gcompare (sortSing' x) (sortSing' x') of+    GLT -> GLT+    GEQ -> case gcompare x x' of+      GLT -> GLT+      GEQ -> case gcompare (sortSing' y) (sortSing' y') of+        GLT -> GLT+        GEQ -> case gcompare y y' of+          GLT -> GLT+          GEQ -> GEQ+          GGT -> GGT+        GGT -> GGT+      GGT -> GGT+    GGT -> GGT+  gcompare (BvConcat _ _) _ = GLT+  gcompare _ (BvConcat _ _) = GGT+  gcompare (BvRotL i x)            (BvRotL i' x')          = case compare (fromIntegral i :: Integer) (fromIntegral i') of+    LT -> GLT+    EQ -> gcompare x x'+    GT -> GGT+  gcompare (BvRotL _ _) _ = GLT+  gcompare _ (BvRotL _ _) = GGT+  gcompare (BvRotR i x)            (BvRotR i' x')          = case compare (fromIntegral i :: Integer) (fromIntegral i') of+    LT -> GLT+    EQ -> gcompare x x'+    GT -> GGT+  gcompare (BvRotR _ _) _ = GLT+  gcompare _ (BvRotR _ _) = GGT+  gcompare (ArrSelect arr i)       (ArrSelect arr' i')     = case gcompare arr arr' of+    GLT -> GLT+    GEQ -> case gcompare i i' of+      GLT -> GLT+      GEQ -> GEQ+      GGT -> GGT+    GGT -> GGT+  gcompare (ArrSelect _ _) _ = GLT+  gcompare _ (ArrSelect _ _) = GGT+  gcompare (ArrStore arr k v)      (ArrStore arr' k' v')   = case gcompare arr arr' of+    GLT -> GLT+    GEQ -> case gcompare k k' of+      GLT -> GLT+      GEQ -> case gcompare v v' of+        GLT -> GLT+        GEQ -> GEQ+        GGT -> GGT+      GGT -> GGT+    GGT -> GGT+  gcompare (ArrStore _ _ _) _ = GLT+  gcompare _ (ArrStore _ _ _) = GGT+  gcompare (StrConcat x y)         (StrConcat x' y')       = gcomparing [(x,x'), (y,y')]+  gcompare (StrConcat _ _) _ = GLT+  gcompare _ (StrConcat _ _) = GGT+  gcompare (StrLength x)           (StrLength x')          = case gcompare x x' of+    GLT -> GLT+    GEQ -> GEQ+    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+      GLT -> GLT+      GEQ -> GEQ+      GGT -> GGT+    GGT -> GGT+  gcompare (StrAt _ _) _ = GLT+  gcompare _ (StrAt _ _) = GGT+  gcompare (StrSubstring x i j)    (StrSubstring x' i' j') = case gcompare x x' of+    GLT -> GLT+    GEQ -> case gcomparing [(i,i'), (j,j')] of+      GLT -> GLT+      GEQ -> GEQ+      GGT -> GGT+    GGT -> GGT+  gcompare (StrSubstring _ _ _) _ = GLT+  gcompare _ (StrSubstring _ _ _) = GGT+  gcompare (StrPrefixOf x y)       (StrPrefixOf x' y')     = case gcomparing [(x,x'), (y,y')] of+    GLT -> GLT+    GEQ -> GEQ+    GGT -> GGT+  gcompare (StrPrefixOf _ _) _ = GLT+  gcompare _ (StrPrefixOf _ _) = GGT+  gcompare (StrSuffixOf x y)       (StrSuffixOf x' y')     = case gcomparing [(x,x'), (y,y')] of+    GLT -> GLT+    GEQ -> GEQ+    GGT -> GGT+  gcompare (StrSuffixOf _ _) _ = GLT+  gcompare _ (StrSuffixOf _ _) = GGT+  gcompare (StrContains x y)       (StrContains x' y')     = case gcomparing [(x,x'), (y,y')] of+    GLT -> GLT+    GEQ -> GEQ+    GGT -> GGT+  gcompare (StrContains _ _) _ = GLT+  gcompare _ (StrContains _ _) = GGT+  gcompare (StrIndexOf x y i)      (StrIndexOf x' y' i')   = case gcomparing [(x,x'), (y,y')] of+    GLT -> GLT+    GEQ -> gcompare i i'+    GGT -> GGT+  gcompare (StrIndexOf _ _ _) _ = GLT+  gcompare _ (StrIndexOf _ _ _) = GGT+  gcompare (StrReplace source target replacement)     (StrReplace source' target' replacement')     = gcomparing [(source, source'), (target, target'), (replacement, replacement')]+  gcompare (StrReplace _ _ _) _ = GLT+  gcompare _ (StrReplace _ _ _) = GGT+  gcompare (StrReplaceAll source target replacement)  (StrReplaceAll source' target' replacement')  = gcomparing [(source, source'), (target, target'), (replacement, replacement')]+  gcompare (StrReplaceAll _ _ _) _ = GLT+  gcompare _ (StrReplaceAll _ _ _) = GGT+  gcompare (ForAll _ expr)         (ForAll _ expr')        = gcompare (expr $ Var (SMTVar (-1))) (expr' $ Var (SMTVar (-1)))+  gcompare (ForAll _ _) _ = GLT+  gcompare _ (ForAll _ _) = GGT+  gcompare (Exists _ expr)         (Exists _ expr')        = gcompare (expr $ Var (SMTVar (-1))) (expr' $ Var (SMTVar (-1)))+  -- gcompare (Exists _ _) _ = GLT+  -- gcompare _ (Exists _ _) = GGT

@@ -40,7 +40,7 @@   SRealSort   :: SSMTSort RealSort   SBoolSort   :: SSMTSort BoolSort   SBvSort     :: KnownNat n => Proxy n -> SSMTSort (BvSort n)-  SArraySort  :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Eq (HaskellType v)) => Proxy k -> Proxy v -> SSMTSort (ArraySort k v)+  SArraySort  :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Ord (HaskellType v)) => Proxy k -> Proxy v -> SSMTSort (ArraySort k v)   SStringSort :: SSMTSort StringSort  deriving instance Show (SSMTSort t)@@ -95,7 +95,7 @@ instance KnownSMTSort RealSort                 where sortSing = SRealSort instance KnownSMTSort BoolSort                 where sortSing = SBoolSort instance KnownNat n => KnownSMTSort (BvSort n) where sortSing = SBvSort (Proxy @n)-instance (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Eq (HaskellType v)) => KnownSMTSort (ArraySort k v) where+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 @@ -108,6 +108,9 @@   SomeSMTSort :: forall cs f (t :: SMTSort). AllC cs t => f t -> SomeSMTSort cs f  deriving instance (forall t. Show (f t)) => Show (SomeSMTSort cs f)++-- | An existential wrapper that hides some known 'SMTSort'.+type SomeKnownSMTSort f = SomeSMTSort '[KnownSMTSort] f  instance Render (SSMTSort t) where   render SBoolSort   = "Bool"

@@ -0,0 +1,100 @@+{-# LANGUAGE UndecidableInstances #-}++module Language.Hasmtlib.Type.Value+( Value(..)+, wrapValue, unwrapValue+)+where++import Language.Hasmtlib.Type.SMTSort+import Data.GADT.Compare+import Data.Proxy+import Control.Lens+import GHC.TypeLits++-- | A wrapper for values of 'SMTSort's.+--   This wraps a Haskell-value into the SMT-Context.+data Value (t :: SMTSort) where+  IntValue    :: HaskellType IntSort    -> Value IntSort+  RealValue   :: HaskellType RealSort   -> Value RealSort+  BoolValue   :: HaskellType BoolSort   -> Value BoolSort+  BvValue     :: KnownNat n => HaskellType (BvSort n) -> Value (BvSort 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++deriving instance Eq (HaskellType t) => Eq (Value t)+deriving instance Ord (HaskellType t) => Ord (Value t)++instance GEq Value where+  geq (BoolValue x) (BoolValue y)   = if x == y then Just Refl else Nothing+  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+    _   -> Nothing+  geq ax@(ArrayValue x) ay@(ArrayValue y) = case geq (sortSing' ax) (sortSing' ay) of+    Nothing -> Nothing+    Just Refl -> if x == y then Just Refl else Nothing+  geq (StringValue x) (StringValue y) = if x == y then Just Refl else Nothing+  geq _ _ = Nothing++liftOrdering :: forall {k} {a :: k}. Ordering -> GOrdering a a+liftOrdering LT = GLT+liftOrdering EQ = GEQ+liftOrdering GT = GGT+{-# INLINE liftOrdering #-}++instance GCompare Value where+  gcompare (BoolValue x) (BoolValue x')     = liftOrdering $ compare x x'+  gcompare (IntValue x)  (IntValue x')      = liftOrdering $ compare x x'+  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'+    GTI -> GGT+  gcompare (ArrayValue x) (ArrayValue x')   = case gcompare (sortSing' (pk x)) (sortSing' (pk x')) of+    GLT -> GLT+    GEQ -> case gcompare (sortSing' (pv x)) (sortSing' (pv x')) of+      GLT -> GLT+      GEQ -> liftOrdering $ compare x x'+      GGT -> GGT+    GGT -> GGT+    where+      pk :: forall k v. HaskellType (ArraySort k v) -> Proxy k+      pk _ = Proxy @k+      pv :: forall k v. HaskellType (ArraySort k v) -> Proxy v+      pv _ = Proxy @v+  gcompare (StringValue x)(StringValue x')  = liftOrdering $ compare x x'+  gcompare (BoolValue _) _                  = GLT+  gcompare _ (BoolValue _)                  = GGT+  gcompare (IntValue _) _                   = GLT+  gcompare _ (IntValue _)                   = GGT+  gcompare (RealValue _) _                  = GLT+  gcompare _ (RealValue _)                  = GGT+  gcompare (BvValue _) _                    = GLT+  gcompare _ (BvValue _)                    = GGT+  gcompare (ArrayValue _) _                 = GLT+  gcompare _ (ArrayValue _)                 = GGT+  -- gcompare (StringValue _) _                = GLT+  -- gcompare _ (StringValue _)                = GGT++-- | Unwraps a Haskell-value from the SMT-Context-'Value'.+unwrapValue :: Value t -> HaskellType t+unwrapValue (IntValue  v)   = v+unwrapValue (RealValue v)   = v+unwrapValue (BoolValue v)   = v+unwrapValue (BvValue   v)   = v+unwrapValue (ArrayValue v)  = v+unwrapValue (StringValue v) = v+{-# INLINEABLE unwrapValue #-}++-- | Wraps a Haskell-value into the SMT-Context-'Value'.+wrapValue :: forall t. KnownSMTSort t => HaskellType t -> Value t+wrapValue = case sortSing @t of+  SIntSort       -> IntValue+  SRealSort      -> RealValue+  SBoolSort      -> BoolValue+  SBvSort _      -> BvValue+  SArraySort _ _ -> ArrayValue+  SStringSort    -> StringValue+{-# INLINEABLE wrapValue #-}