hasmtlib 2.3.2 → 2.4.0

raw patch · 26 files changed

+1482/−1320 lines, 26 filesdep +unordered-containersPVP ok

version bump matches the API change (PVP)

Dependencies added: unordered-containers

API changes (from Hackage documentation)

Files

• CHANGELOG.md +9/−0
• README.md +4/−4
• hasmtlib.cabal +5/−8
• src/Language/Hasmtlib.hs +0/−8
• src/Language/Hasmtlib/Boolean.hs +15/−12
• src/Language/Hasmtlib/Codec.hs +1/−1
• src/Language/Hasmtlib/Counting.hs +1/−5
• src/Language/Hasmtlib/Equatable.hs +0/−107
• src/Language/Hasmtlib/Internal/Constraint.hs +14/−0
• src/Language/Hasmtlib/Internal/Expr.hs +0/−316
• src/Language/Hasmtlib/Internal/Expr/Num.hs +0/−150
• src/Language/Hasmtlib/Internal/Parser.hs +0/−5
• src/Language/Hasmtlib/Internal/Sharing.hs +74/−0
• src/Language/Hasmtlib/Internal/Uniplate1.hs +16/−0
• src/Language/Hasmtlib/Iteable.hs +0/−64
• src/Language/Hasmtlib/Lens.hs +0/−211
• src/Language/Hasmtlib/Orderable.hs +0/−187
• src/Language/Hasmtlib/Type/Expr.hs +1241/−174
• src/Language/Hasmtlib/Type/MonadSMT.hs +17/−18
• src/Language/Hasmtlib/Type/OMT.hs +19/−6
• src/Language/Hasmtlib/Type/Pipe.hs +37/−17
• src/Language/Hasmtlib/Type/SMT.hs +19/−9
• src/Language/Hasmtlib/Type/SMTSort.hs +6/−13
• src/Language/Hasmtlib/Type/Solution.hs +1/−1
• src/Language/Hasmtlib/Type/Solver.hs +2/−3
• src/Language/Hasmtlib/Variable.hs +1/−1

@@ -6,6 +6,15 @@ 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.4.0 _(2024-08-21)_++### Added+- Added _**observable** sharing_ with `Language.Hasmtlib.Internal.Sharing`. Thank you fabeulous@github for the great help!+- Added `Language.Hasmtlib.Internal.Uniplate1` for plating GADTs++### Changed+- Deleted and moved `Language.Hasmtlib.Equatable`, `Language.Hasmtlib.Orderable`, `Language.Hasmtlib.Iteable` & `Language.Hasmtlib.Internal.Expr` into `Language.Hasmtlib.Type.Expr`+ ## v2.3.2 _(2024-08-17)_  ### Changed

@@ -6,18 +6,18 @@ It takes care of encoding your problem, marshaling the data to an external solver and parsing and interpreting the result into Haskell types. It is highly inspired by [ekmett/ersatz](https://github.com/ekmett/ersatz) which does the same for QSAT. Communication with external solvers is handled by [tweag/smtlib-backends](https://github.com/tweag/smtlib-backends). -Building expressions with type-level representations of the SMTLib2-Types guarantees type-safety when communicating with external solvers.+Building expressions with **type-level representations** of the **SMTLib2-Sorts** guarantees type-safety when communicating with external solvers. -Although Hasmtlib does not yet make use of _observable_ sharing [(StableNames)](https://downloads.haskell.org/ghc/9.6.1/docs/libraries/base-4.18.0.0/System-Mem-StableName.html#:~:text=Stable%20Names,-data%20StableName%20a&text=An%20abstract%20name%20for%20an,makeStableName%20on%20the%20same%20object.) like Ersatz does, sharing in the API still allows for pure formula construction.+While **formula construction** is entirely **pure**, Hasmtlib - just like `ersatz` - makes use of _**observable sharing**_ for expressions. -Therefore, this allows you to use the much richer subset of Haskell than a purely monadic meta-language would, which the strong [hgoes/smtlib2](https://github.com/hgoes/smtlib2) is one of. This ultimately results in extremely compact code.+This allows you to use the much richer subset of Haskell than a purely monadic meta-language would, which ultimately results in extremely compact code.  For instance, to define the addition of two `V3` containing Real-SMT-Expressions: ```haskell 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 for a polymorph definition:+Even better, the [Expr-GADT](https://github.com/bruderj15/Hasmtlib/blob/master/src/Language/Hasmtlib/Internal/Expr.hs) allows a polymorph definition: ```haskell v3Add :: Num (Expr t) => V3 (Expr t) -> V3 (Expr t) -> V3 (Expr t) v3Add = liftA2 (+)

@@ -1,7 +1,7 @@ cabal-version:         3.0  name:                  hasmtlib-version:               2.3.2+version:               2.4.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.@@ -28,18 +28,17 @@   default-extensions:  DataKinds, GADTs, TypeFamilies, OverloadedStrings    exposed-modules:     Language.Hasmtlib-                     , Language.Hasmtlib.Lens                      , Language.Hasmtlib.Codec-                     , Language.Hasmtlib.Iteable                      , Language.Hasmtlib.Boolean                      , Language.Hasmtlib.Variable                      , Language.Hasmtlib.Counting-                     , Language.Hasmtlib.Equatable-                     , Language.Hasmtlib.Orderable                      , Language.Hasmtlib.Integraled                      , Language.Hasmtlib.Internal.Parser                      , Language.Hasmtlib.Internal.Bitvec                      , Language.Hasmtlib.Internal.Render+                     , Language.Hasmtlib.Internal.Sharing+                     , Language.Hasmtlib.Internal.Uniplate1+                     , Language.Hasmtlib.Internal.Constraint                      , Language.Hasmtlib.Solver.Common                      , Language.Hasmtlib.Solver.Bitwuzla                      , Language.Hasmtlib.Solver.CVC5@@ -58,13 +57,11 @@                      , Language.Hasmtlib.Type.Option                      , Language.Hasmtlib.Type.ArrayMap -  other-modules:       Language.Hasmtlib.Internal.Expr-                     , Language.Hasmtlib.Internal.Expr.Num-   build-depends:       attoparsec                   >= 0.14.4 && < 1                      , base                         >= 4.17.2 && < 5                      , bytestring                   >= 0.11.5 && < 1                      , containers                   >= 0.6.7  && < 1+                     , unordered-containers         >= 0.2.20 && < 0.3                      , dependent-map                >= 0.4    && < 1                      , mtl                          >= 2.2.2  && < 3                      , text                         >= 2.0.2  && < 3

@@ -10,12 +10,8 @@   , module Language.Hasmtlib.Type.SMTSort   , module Language.Hasmtlib.Type.Solution   , module Language.Hasmtlib.Type.ArrayMap-  , module Language.Hasmtlib.Lens   , module Language.Hasmtlib.Integraled-  , module Language.Hasmtlib.Iteable   , module Language.Hasmtlib.Boolean-  , module Language.Hasmtlib.Equatable-  , module Language.Hasmtlib.Orderable   , module Language.Hasmtlib.Codec   , module Language.Hasmtlib.Counting   , module Language.Hasmtlib.Variable@@ -39,12 +35,8 @@ import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Solution import Language.Hasmtlib.Type.ArrayMap-import Language.Hasmtlib.Lens import Language.Hasmtlib.Integraled-import Language.Hasmtlib.Iteable import Language.Hasmtlib.Boolean-import Language.Hasmtlib.Equatable-import Language.Hasmtlib.Orderable import Language.Hasmtlib.Codec import Language.Hasmtlib.Counting import Language.Hasmtlib.Variable

@@ -89,20 +89,22 @@ any p = foldl (\acc b -> acc || p b) false  instance Boolean Bool where-  bool  = id-  true  = True-  false = False-  (&&)  = (P.&&)-  (||)  = (P.||)-  not   = P.not-  xor   = (/=)+  bool   = id+  true   = True+  false  = False+  (&&)   = (P.&&)+  (||)   = (P.||)+  not    = P.not+  xor    = (/=)+  (<==>) = (==)  instance Boolean Bit where-  bool = Bit-  (&&) = (.&.)-  (||) = (.|.)-  not  = complement-  xor  = Bits.xor+  bool     = Bit+  (&&)     = (.&.)+  (||)     = (.|.)+  not      = complement+  xor      = Bits.xor+  x <==> y = bool (x == y)  -- | Defined bitwise instance KnownNat n => Boolean (V.Vector n Bit) where@@ -111,3 +113,4 @@   (||) = V.zipWith (||)   not  = V.map not   xor  = V.zipWith Bits.xor+  x <==> y = bool (x == y)

@@ -7,7 +7,7 @@  import Prelude hiding (not, (&&), (||), all, and) import Language.Hasmtlib.Internal.Bitvec-import Language.Hasmtlib.Internal.Expr+import Language.Hasmtlib.Type.Expr (Expr(..), SMTVar(..), unwrapValue, wrapValue) import Language.Hasmtlib.Type.Solution import Language.Hasmtlib.Type.ArrayMap import Language.Hasmtlib.Type.SMTSort

@@ -1,12 +1,8 @@ module Language.Hasmtlib.Counting where  import Prelude hiding (not, (&&), (||), or)-import Language.Hasmtlib.Internal.Expr.Num ()-import Language.Hasmtlib.Internal.Expr import Language.Hasmtlib.Type.SMTSort-import Language.Hasmtlib.Equatable-import Language.Hasmtlib.Orderable-import Language.Hasmtlib.Iteable+import Language.Hasmtlib.Type.Expr import Data.Proxy  -- | Wrapper for 'count' which takes a 'Proxy'.

@@ -1,107 +0,0 @@--- Required for class constraints of form: c (ValueType t) :: Constraint-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE DefaultSignatures #-}--module Language.Hasmtlib.Equatable where--import Prelude hiding (not, (&&))-import Language.Hasmtlib.Internal.Expr-import Language.Hasmtlib.Type.SMTSort-import Language.Hasmtlib.Boolean-import Data.Int-import Data.Word-import Data.Void-import Data.Tree (Tree)-import Data.Monoid (Sum, Product, First, Last, Dual)-import Data.Functor.Identity (Identity)-import qualified Data.Vector.Sized as V-import Numeric.Natural-import GHC.Generics---- | Test two as on equality as SMT-Expression.------   You can derive an instance of this class if your type is 'Generic'.------ @---     x <- var @RealType---     y <- var---     assert $ y === x && not (y /== x)--- @----class Equatable a where-  -- | Test whether two values are equal in the SMT-Problem.-  (===) :: a -> a -> Expr BoolSort-  default (===) :: (Generic a, GEquatable (Rep a)) => a -> a -> Expr BoolSort-  a === b = from a ===# from b--  -- | Test whether two values are not equal in the SMT-Problem.-  (/==) :: a -> a -> Expr BoolSort-  x /== y = not $ x === y--infix 4 ===, /==--instance (KnownSMTSort t, Eq (HaskellType t)) => Equatable (Expr t) where-  x === y = EQU $ V.fromTuple (x,y)-  {-# INLINE (===) #-}-  x /== y = Distinct $ V.fromTuple (x,y)-  {-# INLINE (/==) #-}--class GEquatable f where-  (===#) :: f a -> f a -> Expr BoolSort--instance GEquatable U1 where-  U1 ===# U1 = true--instance GEquatable V1 where-  x ===# y = x `seq` y `seq` error "GEquatable[V1].===#"--instance (GEquatable f, GEquatable g) => GEquatable (f :*: g) where-  (a :*: b) ===# (c :*: d) = (a ===# c) && (b ===# d)--instance (GEquatable f, GEquatable g) => GEquatable (f :+: g) where-  L1 a ===# L1 b = a ===# b-  R1 a ===# R1 b = a ===# b-  _ ===# _ = false--instance GEquatable f => GEquatable (M1 i c f) where-  M1 x ===# M1 y = x ===# y--instance Equatable a => GEquatable (K1 i a) where-  K1 a ===# K1 b = a === b--instance Equatable ()       where _ === _ = true-instance Equatable Void     where x === y = x `seq` y `seq` error "Equatable[Void].==="-instance Equatable Int      where x === y = bool (x == y)-instance Equatable Integer  where x === y = bool (x == y)-instance Equatable Natural  where x === y = bool (x == y)-instance Equatable Word     where x === y = bool (x == y)-instance Equatable Word8    where x === y = bool (x == y)-instance Equatable Word16   where x === y = bool (x == y)-instance Equatable Word32   where x === y = bool (x == y)-instance Equatable Word64   where x === y = bool (x == y)-instance Equatable Int8     where x === y = bool (x == y)-instance Equatable Int16    where x === y = bool (x == y)-instance Equatable Int32    where x === y = bool (x == y)-instance Equatable Int64    where x === y = bool (x == y)-instance Equatable Char     where x === y = bool (x == y)-instance Equatable Float    where x === y = bool (x == y)-instance Equatable Double   where x === y = bool (x == y)-instance Equatable Ordering where x === y = bool (x == y)-instance Equatable Bool     where x === y = bool (x == y)-instance (Equatable a, Equatable b) => Equatable (a,b)-instance (Equatable a, Equatable b, Equatable c) => Equatable (a,b,c)-instance (Equatable a, Equatable b, Equatable c, Equatable d) => Equatable (a,b,c,d)-instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e) => Equatable (a,b,c,d,e)-instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e, Equatable f) => Equatable (a,b,c,d,e,f)-instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e, Equatable f, Equatable g) => Equatable (a,b,c,d,e,f,g)-instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e, Equatable f, Equatable g, Equatable h) => Equatable (a,b,c,d,e,f,g,h)-instance Equatable a => Equatable [a]-instance Equatable a => Equatable (Tree a)-instance Equatable a => Equatable (Maybe a)-instance (Equatable a, Equatable b) => Equatable (Either a b)-instance Equatable a => Equatable (Sum a)-instance Equatable a => Equatable (Product a)-instance Equatable a => Equatable (First a)-instance Equatable a => Equatable (Last a)-instance Equatable a => Equatable (Dual a)-instance Equatable a => Equatable (Identity a)

@@ -0,0 +1,14 @@+module Language.Hasmtlib.Internal.Constraint where++import Data.Kind++-- | AllC ensures that a list of constraints is applied to a poly-kinded 'Type' k+--+-- @+-- AllC '[]       k = ()+-- AllC (c ': cs) k = (c k, AllC cs k)+-- @+type AllC :: [k -> Constraint] -> k -> Constraint+type family AllC cs k :: Constraint where+  AllC '[]       k = ()+  AllC (c ': cs) k = (c k, AllC cs k)

@@ -1,316 +0,0 @@-{-# LANGUAGE RoleAnnotations #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE UndecidableInstances #-}--module Language.Hasmtlib.Internal.Expr where--import Prelude hiding (not)-import Language.Hasmtlib.Internal.Render-import Language.Hasmtlib.Type.ArrayMap-import Language.Hasmtlib.Type.SMTSort-import Language.Hasmtlib.Boolean-import Data.Map hiding (toList)-import Data.Proxy-import Data.Coerce-import Data.String (IsString(..))-import Data.Text (pack)-import Data.ByteString.Builder-import Data.ByteString.Lazy.UTF8 (toString)-import qualified Data.Vector.Sized as V-import Control.Lens-import GHC.TypeLits-import GHC.Generics---- | An internal SMT variable with a phantom-type which holds an 'Int' as it's identifier.-type role SMTVar phantom-newtype SMTVar (t :: SMTSort) = SMTVar { _varId :: Int } deriving (Show, Eq, Ord, Generic)-$(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     :: HaskellType (BvSort n) -> Value (BvSort n)-  ArrayValue  :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => 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)---- | 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, ...).-data Expr (t :: SMTSort) where-  Var       :: SMTVar t -> Expr t-  Constant  :: Value  t -> Expr t--  Plus      :: 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-  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-  Sin       :: Expr RealSort -> Expr RealSort-  Cos       :: Expr RealSort -> Expr RealSort-  Tan       :: Expr RealSort -> Expr RealSort-  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)) => 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-  StrSuffixOf   :: Expr StringSort -> Expr StringSort -> Expr BoolSort-  StrContains   :: Expr StringSort -> Expr StringSort -> Expr BoolSort-  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-  Exists    :: KnownSMTSort t => Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Expr BoolSort--instance Boolean (Expr BoolSort) where-  bool = Constant . BoolValue-  {-# INLINE bool #-}-  (Constant (BoolValue x)) && y = if x then y else false-  x && (Constant (BoolValue y)) = if y then x else false-  x && y = And x y-  {-# INLINE (&&) #-}-  (Constant (BoolValue x)) || y = if x then true else y-  x || (Constant (BoolValue y)) = if y then true else x-  x || y = Or x y-  {-# INLINE (||) #-}-  not (Constant (BoolValue x)) = bool . not $ x-  not x = Not x-  {-# INLINE not #-}-  xor (Constant (BoolValue x)) y = if x then not y else y-  xor x (Constant (BoolValue y)) = if y then not x else x-  xor x y = Xor x y-  {-# INLINE xor #-}--instance KnownNat n => Boolean (Expr (BvSort n)) where-  bool = Constant . BvValue . bool-  {-# INLINE bool #-}-  (&&) = BvAnd-  {-# INLINE (&&) #-}-  (||) = BvOr-  {-# INLINE (||) #-}-  not  = BvNot-  {-# INLINE not #-}-  xor  = BvXor-  {-# INLINE xor #-}--instance Bounded (Expr BoolSort) where-  minBound = false-  maxBound = true--instance KnownNat n => Bounded (Expr (BvSort n)) where-  minBound = Constant $ BvValue minBound-  maxBound = Constant $ BvValue maxBound--instance Semigroup (Expr StringSort) where-  (<>) = StrConcat--instance Monoid (Expr StringSort) where-  mempty = Constant $ StringValue mempty-  mappend = (<>)--instance IsString (Expr StringSort) where-  fromString = Constant . StringValue . pack--instance Render (SMTVar t) where-  render v = "var_" <> intDec (coerce @(SMTVar t) @Int v)-  {-# INLINEABLE render #-}--instance Render (Value t) where-  render (IntValue x)   = render x-  render (RealValue x)  = render x-  render (BoolValue x)  = render x-  render (BvValue   v)  = "#b" <> render v-  render (ArrayValue arr) = case minViewWithKey (arr^.stored) of-    Nothing -> constRender $ arr^.arrConst-    Just ((k,v), stored')-      | size (arr^.stored) > 1 -> render $ ArrStore (Constant (wrapValue (arr & stored .~ stored'))) (Constant (wrapValue k)) (Constant (wrapValue v))-      | 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)) => ConstArray (HaskellType k) (HaskellType v) -> SSMTSort (ArraySort k v)-      goSing _ = sortSing @(ArraySort k v)-  render (StringValue x) = "\"" <> render x <> "\""--instance KnownSMTSort t => Render (Expr t) where-  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 (Abs x)      = renderUnary  "abs" x-  render (Mod x y)    = renderBinary "mod" x y-  render (IDiv x y)   = renderBinary "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 (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 (Not x)      = renderUnary  "not" x-  render (And x y)    = renderBinary "and" x y-  render (Or x y)     = renderBinary "or" x y-  render (Impl x y)   = renderBinary "=>" x y-  render (Xor x y)    = renderBinary "xor" x y--  render Pi           = "real.pi"-  render (Sqrt x)     = renderUnary "sqrt" x-  render (Exp x)      = renderUnary "exp" x-  render (Sin x)      = renderUnary "sin" x-  render (Cos x)      = renderUnary "cos" x-  render (Tan x)      = renderUnary "tan" x-  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 (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 (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)-  render (StrSuffixOf x y)      = renderBinary "str.suffixof" (render x) (render y)-  render (StrContains x y)      = renderBinary "str.contains" (render x) (render y)-  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--renderQuantifier :: forall t. KnownSMTSort t => Builder -> Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Builder-renderQuantifier qname (Just qvar) f =-  renderBinary-    qname-    ("(" <> renderUnary (render qvar) (sortSing @t) <> ")")-    expr-  where-    expr = render $ f $ Var qvar-renderQuantifier _ Nothing _ = mempty--instance Show (Value t) where-  show = toString . toLazyByteString . render--instance KnownSMTSort t => Show (Expr t) where-  show = toString . toLazyByteString . render

@@ -1,150 +0,0 @@-module Language.Hasmtlib.Internal.Expr.Num where--import Prelude hiding (div, mod, quotRem, rem, quot, divMod)-import Language.Hasmtlib.Internal.Expr-import Language.Hasmtlib.Integraled-import Language.Hasmtlib.Type.SMTSort-import Language.Hasmtlib.Iteable-import Language.Hasmtlib.Equatable-import Language.Hasmtlib.Orderable-import GHC.TypeNats--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 = Plus x (Neg 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-   {-# INLINE fromInteger #-}-   (Constant (RealValue 0)) + y = y-   x + (Constant (RealValue 0)) = x-   (Constant (RealValue x)) + (Constant (RealValue y)) = Constant (RealValue (x + y))-   x + y = Plus x y-   {-# INLINE (+) #-}-   x - (Constant (RealValue 0)) = x-   (Constant (RealValue x)) - (Constant (RealValue y)) = Constant (RealValue (x - y))-   x - y = Plus x (Neg 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))-   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 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 = BvAdd x y-   {-# INLINE (+) #-}-   x - (Constant (BvValue 0)) = x-   (Constant (BvValue x)) - (Constant (BvValue y)) = Constant (BvValue (x - y))-   x - y = BvSub 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-   {-# INLINE (*) #-}-   abs         = id-   {-# INLINE abs #-}-   signum _    = 0-   {-# 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 / y          = Div x y-  {-# INLINE (/) #-}--instance Floating (Expr RealSort) where-    pi    = Pi-    {-# INLINE pi #-}-    exp   = Exp-    {-# INLINE exp #-}-    log   = error "SMT-Solvers currently do not support log"-    sqrt  = Sqrt-    {-# INLINE sqrt #-}-    sin   = Sin-    {-# INLINE sin #-}-    cos   = Cos-    {-# INLINE cos #-}-    tan   = Tan-    {-# INLINE tan #-}-    asin  = Asin-    {-# INLINE asin #-}-    acos  = Acos-    {-# INLINE acos #-}-    atan  = Atan-    {-# INLINE atan #-}-    sinh  = error "SMT-Solver currently do not support sinh"-    cosh  = error "SMT-Solver currently do not support cosh"-    tanh  = error "SMT-Solver currently do not support tanh"-    asinh = error "SMT-Solver currently do not support asinh"-    acosh = error "SMT-Solver currently do not support acosh"-    atanh = error "SMT-Solver currently do not support atanh"--instance Integraled (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 #-}--instance KnownNat n => Integraled (Expr (BvSort n)) where-  quot        = BvuDiv-  {-# INLINE quot #-}-  rem         = BvuRem-  {-# INLINE rem #-}-  div         = BvuDiv-  {-# INLINE div #-}-  mod         = BvuRem-  {-# INLINE mod #-}-  quotRem x y = (quot x y, rem x y)-  {-# INLINE quotRem #-}-  divMod x y  = (div x y, mod x y)-  {-# INLINE divMod #-}

@@ -6,12 +6,7 @@ import Prelude hiding (not, (&&), (||), and , or) import Language.Hasmtlib.Internal.Bitvec import Language.Hasmtlib.Internal.Render-import Language.Hasmtlib.Internal.Expr.Num ()-import Language.Hasmtlib.Internal.Expr-import Language.Hasmtlib.Equatable-import Language.Hasmtlib.Orderable import Language.Hasmtlib.Boolean-import Language.Hasmtlib.Iteable import Language.Hasmtlib.Codec import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Solution

@@ -0,0 +1,74 @@+{-# LANGUAGE Trustworthy #-}++module Language.Hasmtlib.Internal.Sharing+  ( Sharing(..)+  , runSharing, share+  )+where++import Language.Hasmtlib.Internal.Uniplate1+import Language.Hasmtlib.Type.MonadSMT+import Language.Hasmtlib.Type.SMTSort+import Language.Hasmtlib.Type.Expr+import Data.GADT.Compare+import Data.HashMap.Lazy+import Control.Monad.State+import Control.Lens+import System.Mem.StableName+import System.IO.Unsafe+import Unsafe.Coerce++import Data.Kind++-- | States that can share expressions by comparing their 'StableName's.+class Sharing s where+  -- | A constraint on the monad used when asserting the shared node in 'assertSharedNode'.+  type SharingMonad s :: (Type -> Type) -> Constraint++  -- | A 'Lens'' on a mapping between a 'StableName' and it's 'Expr' we may share.+  stableMap :: Lens' s (HashMap (StableName ()) (SomeKnownSMTSort Expr))++  -- | Asserts that a node-expression is represented by it's auxiliary node-variable: @nodeExpr :: Expr t === nodeVar@.+  --   Also gives access to the 'StableName' of the original expression.+  assertSharedNode :: (MonadState s m, SharingMonad s m) => StableName () -> Expr BoolSort -> m ()++-- | Shares all possible sub-expressions in given expression.+--   Replaces each node in the expression-tree with an auxiliary variable.+--   All nodes @x@ @y@ where @makeStableName x == makeStableName y@ are replaced with the same auxiliary variable.+--   Therefore this creates a DAG.+runSharing :: (KnownSMTSort t, MonadSMT s m, Sharing s, SharingMonad s m) => Expr t -> m (Expr t)+runSharing = lazyParaM1 (+    \origExpr expr ->+      if isLeaf origExpr+      then return origExpr+      else case sortSing' origExpr of   -- scopes Equatable (Expr t) for specific t+        SBoolSort      -> share origExpr expr+        SIntSort       -> share origExpr expr+        SRealSort      -> share origExpr expr+        SBvSort _      -> share origExpr expr+        SArraySort _ _ -> share origExpr expr+        SStringSort    -> share origExpr expr)++-- | Returns an auxiliary variable representing this expression node.+--   If such a shared auxiliary variable exists already, returns that.+--   Otherwise creates one and returns it.+share :: (Equatable (Expr t), KnownSMTSort t, MonadSMT s m, Sharing s, SharingMonad s m) => Expr t -> m (Expr t) -> m (Expr t)+share expr@(ForAll _ _) _ = return expr     -- sharing quantified expression would out-scope quantified var+share expr@(Exists _ _) _ = return expr+share origExpr expr = do+  let sn = unsafePerformIO (makeStableName' origExpr)+   in use (stableMap.at sn) >>= \mexpr' -> case mexpr' of+        Just (SomeSMTSort expr') -> case geq (sortSing' origExpr) (sortSing' expr') of+          Nothing -> expr >>= makeNode sn+          Just Refl -> return expr'+        Nothing -> expr >>= makeNode sn++makeNode :: (Equatable (Expr t), KnownSMTSort t, MonadSMT s m, Sharing s, SharingMonad s m) => StableName () -> Expr t -> m (Expr t)+makeNode sn nodeExpr = do+  nodeVar <- var+  assertSharedNode sn $ nodeVar === nodeExpr+  stableMap.at sn ?= SomeSMTSort nodeVar+  return nodeVar++makeStableName' :: a -> IO (StableName ())+makeStableName' x = x `seq` fmap unsafeCoerce (makeStableName x)

@@ -0,0 +1,16 @@+{-# LANGUAGE FunctionalDependencies #-}++module Language.Hasmtlib.Internal.Uniplate1 where++import Language.Hasmtlib.Internal.Constraint+import Data.Kind++type Uniplate1 :: (k -> Type) -> [k -> Constraint] -> Constraint+class Uniplate1 f cs | f -> cs where+  uniplate1 :: (Applicative m, AllC cs b) => (forall a. AllC cs a => f a -> m (f a)) -> f b -> m (f b)++transformM1 :: (Monad m, Uniplate1 f cs, AllC cs b) => (forall a. AllC cs a => f a -> m (f a)) -> f b -> m (f b)+transformM1 f x = uniplate1 (transformM1 f) x >>= f++lazyParaM1 :: (Monad m, Uniplate1 f cs, AllC cs b) => (forall a. AllC cs a => f a -> m (f a) -> m (f a)) -> f b -> m (f b)+lazyParaM1 f x = f x (uniplate1 (lazyParaM1 f) x)

@@ -1,64 +0,0 @@-{-# LANGUAGE DefaultSignatures #-}--module Language.Hasmtlib.Iteable where--import Language.Hasmtlib.Internal.Expr-import Language.Hasmtlib.Type.SMTSort-import Data.Sequence (Seq)-import Data.Tree-import Data.Monoid (Sum, Product, First, Last, Dual)-import Data.Functor.Identity (Identity)---- | If condition (p :: b) then (t :: a) else (f :: a)------    >>> ite true "1" "2"---        "1"---    >>> ite false 100 42---        42-class Iteable b a where-  ite :: b -> a -> a -> a-  default ite :: (Iteable b c, Applicative f, f c ~ a) => b -> a -> a -> a-  ite p t f = ite p <$> t <*> f--instance Iteable (Expr BoolSort) (Expr t) where-  ite = Ite-  {-# INLINE ite #-}--instance Iteable Bool a where-  ite p t f = if p then t else f-  {-# INLINE ite #-}--instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) [a]-instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Maybe a)-instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Seq a)-instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Tree a)-instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Sum a)-instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Product a)-instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (First a)-instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Last a)-instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Dual a)-instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Identity a)--instance Iteable (Expr BoolSort) () where-  ite _ _ _ = ()--instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b) => Iteable (Expr BoolSort) (a,b) where-  ite p (a,b) (a',b') = (ite p a a', ite p b b')--instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c) => Iteable (Expr BoolSort) (a,b,c) where-  ite p (a,b,c) (a',b',c') = (ite p a a', ite p b b', ite p c c')--instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d) => Iteable (Expr BoolSort) (a,b,c,d) where-  ite p (a,b,c,d) (a',b',c',d') = (ite p a a', ite p b b', ite p c c', ite p d d')--instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d, Iteable (Expr BoolSort) e) => Iteable (Expr BoolSort) (a,b,c,d,e) where-  ite p (a,b,c,d,e) (a',b',c',d',e') = (ite p a a', ite p b b', ite p c c', ite p d d', ite p e e')--instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d, Iteable (Expr BoolSort) e, Iteable (Expr BoolSort) f) => Iteable (Expr BoolSort) (a,b,c,d,e,f) where-  ite p (a,b,c,d,e,f) (a',b',c',d',e',f') = (ite p a a', ite p b b', ite p c c', ite p d d', ite p e e', ite p f f')--instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d, Iteable (Expr BoolSort) e, Iteable (Expr BoolSort) f, Iteable (Expr BoolSort) g) => Iteable (Expr BoolSort) (a,b,c,d,e,f,g) where-  ite p (a,b,c,d,e,f,g) (a',b',c',d',e',f',g') = (ite p a a', ite p b b', ite p c c', ite p d d', ite p e e', ite p f f', ite p g g')--instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d, Iteable (Expr BoolSort) e, Iteable (Expr BoolSort) f, Iteable (Expr BoolSort) g, Iteable (Expr BoolSort) h) => Iteable (Expr BoolSort) (a,b,c,d,e,f,g,h) where-  ite p (a,b,c,d,e,f,g,h) (a',b',c',d',e',f',g',h') = (ite p a a', ite p b b', ite p c c', ite p d d', ite p e e', ite p f f', ite p g g', ite p h h')

@@ -1,211 +0,0 @@-{-# LANGUAGE UndecidableInstances #-}--module Language.Hasmtlib.Lens where--import Language.Hasmtlib.Internal.Expr-import Language.Hasmtlib.Type.Expr-import Language.Hasmtlib.Type.SMTSort-import Language.Hasmtlib.Equatable-import Language.Hasmtlib.Orderable-import Language.Hasmtlib.Iteable-import Data.GADT.Compare-import Control.Lens--type instance Index   (Expr StringSort) = Expr IntSort-type instance IxValue (Expr StringSort) = Expr StringSort--instance Ixed (Expr StringSort) where-  ix i f s = f (strAt s i) <&> \a ->-    let l = strSubstring a 0 i-        r = strSubstring a i (strLength a)-     in l <> strReplace r (strAt a i) s--instance AsEmpty (Expr StringSort) where-  _Empty = prism'-    (const mempty)-    (\s -> ite (s === mempty) (Just ()) Nothing)--instance Prefixed (Expr StringSort) where-  prefixed p = prism'-    (p <>)-    (\s -> ite (p `strPrefixOf` s) (Just $ strReplace s p mempty) Nothing)--instance Suffixed (Expr StringSort) where-  suffixed qs = prism'-    (<> qs)-    (\s -> ite (qs `strSuffixOf` s) (Just $ strSubstring s 0 (strLength s - strLength qs)) Nothing)--instance Cons (Expr StringSort) (Expr StringSort) (Expr StringSort) (Expr StringSort) where-  _Cons = prism'-    (uncurry (<>))-    (\s -> ite (strLength s >? 0) (Just (strAt s 0, strSubstring s 1 (strLength s))) Nothing)--instance Snoc (Expr StringSort) (Expr StringSort) (Expr StringSort) (Expr StringSort) where-  _Snoc = prism'-    (uncurry (<>))-    (\s -> ite (strLength s >? 0) (Just (strSubstring s 0 (strLength s - 1), strAt s (strLength s - 1))) Nothing)--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)) => Ixed (Expr (ArraySort k v)) where-  ix i f arr = f (select arr i) <&> store arr i---- | **Caution for quantified expressions:** 'plate-function' @f@ will only be applied if quantification already has taken place.(&&)---   Therefore make sure 'quantify' has been run before.---   Otherwise the quantified expression and therefore all it's sub-expressions will not have @f@ applied.-instance KnownSMTSort t => Plated (Expr t) where-  plate _ expr@(Var _)            = pure expr-  plate _ expr@(Constant _)       = pure expr-  plate f (Plus x y)              = Plus <$> f x <*> f y-  plate f (Neg x)                 = Neg <$> f x-  plate f (Mul x y)               = Mul <$> f x <*> f y-  plate f (Abs x)                 = Abs <$> f x-  plate f (Mod x y)               = Mod <$> f x <*> f y-  plate f (IDiv x y)              = IDiv <$> f x <*> f y-  plate f (Div x y)               = Div <$> f x <*> f y-  plate f (LTH x y)               = LTH <$> somePlate f x <*> somePlate f y-  plate f (LTHE x y)              = LTHE <$> somePlate f x <*> somePlate f y-  plate f (EQU xs)                = EQU <$> traverse (somePlate f) xs-  plate f (Distinct xs)           = Distinct <$> traverse (somePlate f) xs-  plate f (GTHE x y)              = GTHE <$> somePlate f x <*> somePlate f y-  plate f (GTH x y)               = GTH <$> somePlate f x <*> somePlate f y-  plate f (Not x)                 = Not <$> somePlate f x-  plate f (And x y)               = And <$> somePlate f x <*> somePlate f y-  plate f (Or x y)                = Or <$> somePlate f x <*> somePlate f y-  plate f (Impl x y)              = Impl <$> somePlate f x <*> somePlate f y-  plate f (Xor x y)               = Xor <$> somePlate f x <*> somePlate f y-  plate _ Pi                      = pure Pi-  plate f (Sqrt x)                = Sqrt <$> f x-  plate f (Exp x)                 = Exp <$> f x-  plate f (Sin x)                 = Sin <$> f x-  plate f (Cos x)                 = Cos <$> f x-  plate f (Tan x)                 = Tan <$> f x-  plate f (Asin x)                = Asin <$> f x-  plate f (Acos x)                = Acos <$> f x-  plate f (Atan x)                = Atan <$> f x-  plate f (ToReal x)              = ToReal <$> somePlate f x-  plate f (ToInt x)               = ToInt <$> somePlate f x-  plate f (IsInt x)               = IsInt <$> somePlate f x-  plate f (Ite p t n)             = Ite <$> somePlate f p <*> f t <*> f n-  plate f (BvNot x)               = BvNot <$> f x-  plate f (BvAnd x y)             = BvAnd <$> f x <*> f y-  plate f (BvOr x y)              = BvOr <$> f x <*> f y-  plate f (BvXor x y)             = BvXor <$> f x <*> f y-  plate f (BvNand x y)            = BvNand <$> f x <*> f y-  plate f (BvNor x y)             = BvNor <$> f x <*> f y-  plate f (BvNeg x)               = BvNeg <$> f x-  plate f (BvAdd x y)             = BvAdd <$> f x <*> f y-  plate f (BvSub x y)             = BvSub <$> f x <*> f y-  plate f (BvMul x y)             = BvMul <$> f x <*> f y-  plate f (BvuDiv x y)            = BvuDiv <$> f x <*> f y-  plate f (BvuRem x y)            = BvuRem <$> f x <*> f y-  plate f (BvShL x y)             = BvShL <$> f x <*> f y-  plate f (BvLShR x y)            = BvLShR <$> f x <*> f y-  plate f (BvConcat x y)          = BvConcat <$> somePlate f x <*> somePlate f y-  plate f (BvRotL i x)            = BvRotL i <$> f x-  plate f (BvRotR i x)            = BvRotR i <$> f x-  plate f (BvuLT x y)             = BvuLT <$> somePlate f x <*> somePlate f y-  plate f (BvuLTHE x y)           = BvuLTHE <$> somePlate f x <*> somePlate f y-  plate f (BvuGTHE x y)           = BvuGTHE <$> somePlate f x <*> somePlate f y-  plate f (BvuGT x y)             = BvuGT <$> somePlate f x <*> somePlate f y-  plate f (ArrSelect i arr)       = ArrSelect i <$> somePlate f arr-  plate f (ArrStore i x arr)      = ArrStore i <$> somePlate f x <*> somePlate f arr-  plate f (StrConcat x y)         = StrConcat <$> f x <*> f y-  plate f (StrLength x)           = StrLength <$> somePlate f x-  plate f (StrLT x y)             = StrLT <$> somePlate f x <*> somePlate f y-  plate f (StrLTHE x y)           = StrLTHE <$> somePlate f x <*> somePlate f y-  plate f (StrAt x i)             = StrAt <$> f x <*> somePlate f i-  plate f (StrSubstring x i j)    = StrSubstring <$> f x <*> somePlate f i <*> somePlate f j-  plate f (StrPrefixOf x y)       = StrPrefixOf <$> somePlate f x <*> somePlate f y-  plate f (StrSuffixOf x y)       = StrSuffixOf <$> somePlate f x <*> somePlate f y-  plate f (StrContains x y)       = StrContains <$> somePlate f x <*> somePlate f y-  plate f (StrIndexOf x y i)      = StrIndexOf <$> somePlate f x <*> somePlate f y <*> f i-  plate f (StrReplace x y y')     = StrReplace <$> f x <*> f y <*> f y'-  plate f (StrReplaceAll x y y')  = StrReplaceAll <$> f x <*> f y <*> f y'-  plate f (ForAll (Just qv) expr) = ForAll (Just qv) . const <$> somePlate f (expr (Var qv))-  plate _ (ForAll Nothing expr)   = pure $ ForAll Nothing expr-  plate f (Exists (Just qv) expr) = Exists (Just qv) . const <$> somePlate f (expr (Var qv))-  plate _ (Exists Nothing expr)   = pure $ Exists Nothing expr---- | Apply the 'plate'-function @f@ for given 'Expr' @expr@ if possible.---   Otherwise try to apply @f@ for the children of @expr@.---   **Caution for quantified expressions:** 'plate-function' @f@ will only be applied if quantification already has taken place.(&&)---   Therefore make sure 'quantify' has been run before.---   Otherwise the quantified expression and therefore all it's sub-expressions will not have @f@ applied.-somePlate :: forall t f. (KnownSMTSort t, Applicative f) => (Expr t -> f (Expr t)) -> (forall s. KnownSMTSort s => Expr s -> f (Expr s))-somePlate f expr = case geq (sortSing @t) (sortSing' expr) of-  Just Refl -> f expr-  Nothing   -> case expr of-    Var _                -> pure expr-    Constant _           -> pure expr-    Plus x y             -> Plus <$> somePlate f x <*> somePlate f y-    Neg x                -> Neg  <$> somePlate f x-    Mul x y              -> Mul  <$> somePlate f x <*> somePlate f y-    Abs x                -> Abs  <$> somePlate f x-    Mod x y              -> Mod  <$> somePlate f x <*> somePlate f y-    IDiv x y             -> IDiv <$> somePlate f x <*> somePlate f y-    Div x y              -> Div  <$> somePlate f x <*> somePlate f y-    LTH x y              -> LTH  <$> somePlate f x <*> somePlate f y-    LTHE x y             -> LTHE <$> somePlate f x <*> somePlate f y-    EQU xs               -> EQU  <$> traverse (somePlate f) xs-    Distinct xs          -> Distinct <$> traverse (somePlate f) xs-    GTHE x y             -> GTHE <$> somePlate f x <*> somePlate f y-    GTH x y              -> GTH  <$> somePlate f x <*> somePlate f y-    Not x                -> Not  <$> somePlate f x-    And x y              -> And  <$> somePlate f x <*> somePlate f y-    Or x y               -> Or   <$> somePlate f x <*> somePlate f y-    Impl x y             -> Impl <$> somePlate f x <*> somePlate f y-    Xor x y              -> Xor  <$> somePlate f x <*> somePlate f y-    Pi                   -> pure Pi-    Sqrt x               -> Sqrt <$> somePlate f x-    Exp x                -> Exp  <$> somePlate f x-    Sin x                -> Sin  <$> somePlate f x-    Cos x                -> Cos  <$> somePlate f x-    Tan x                -> Tan  <$> somePlate f x-    Asin x               -> Asin <$> somePlate f x-    Acos x               -> Acos <$> somePlate f x-    Atan x               -> Atan <$> somePlate f x-    ToReal x             -> ToReal <$> somePlate f x-    ToInt x              -> ToInt  <$> somePlate f x-    IsInt x              -> IsInt  <$> somePlate f x-    Ite p t n            -> Ite    <$> somePlate f p <*> somePlate f t <*> somePlate f n-    BvNot x              -> BvNot  <$> somePlate f x-    BvAnd x y            -> BvAnd  <$> somePlate f x <*> somePlate f y-    BvOr x y             -> BvOr   <$> somePlate f x <*> somePlate f y-    BvXor x y            -> BvXor  <$> somePlate f x <*> somePlate f y-    BvNand x y           -> BvNand <$> somePlate f x <*> somePlate f y-    BvNor x y            -> BvNor  <$> somePlate f x <*> somePlate f y-    BvNeg x              -> BvNeg  <$> somePlate f x-    BvAdd x y            -> BvAdd  <$> somePlate f x <*> somePlate f y-    BvSub x y            -> BvSub  <$> somePlate f x <*> somePlate f y-    BvMul x y            -> BvMul  <$> somePlate f x <*> somePlate f y-    BvuDiv x y           -> BvuDiv <$> somePlate f x <*> somePlate f y-    BvuRem x y           -> BvuRem <$> somePlate f x <*> somePlate f y-    BvShL x y            -> BvShL  <$> somePlate f x <*> somePlate f y-    BvLShR x y           -> BvLShR <$> somePlate f x <*> somePlate f y-    BvConcat x y         -> BvConcat <$> somePlate f x <*> somePlate f y-    BvRotL i x           -> BvRotL i <$> somePlate f x-    BvRotR i x           -> BvRotR i <$> somePlate f x-    BvuLT x y            -> BvuLT    <$> somePlate f x <*> somePlate f y-    BvuLTHE x y          -> BvuLTHE  <$> somePlate f x <*> somePlate f y-    BvuGTHE x y          -> BvuGTHE  <$> somePlate f x <*> somePlate f y-    BvuGT x y            -> BvuGT    <$> somePlate f x <*> somePlate f y-    ArrSelect i arr      -> ArrSelect i   <$> somePlate f arr-    ArrStore i x arr     -> ArrStore i    <$> somePlate f x <*> somePlate f arr-    StrConcat x y        -> StrConcat     <$> somePlate f x <*> somePlate f y-    StrLength x          -> StrLength     <$> somePlate f x-    StrLT x y            -> StrLT         <$> somePlate f x <*> somePlate f y-    StrLTHE x y          -> StrLTHE       <$> somePlate f x <*> somePlate f y-    StrAt x i            -> StrAt         <$> somePlate f x <*> somePlate f i-    StrSubstring x i j   -> StrSubstring  <$> somePlate f x <*> somePlate f i <*> somePlate f j-    StrPrefixOf x y      -> StrPrefixOf   <$> somePlate f x <*> somePlate f y-    StrSuffixOf x y      -> StrSuffixOf   <$> somePlate f x <*> somePlate f y-    StrContains x y      -> StrContains   <$> somePlate f x <*> somePlate f y-    StrIndexOf x y i     -> StrIndexOf    <$> somePlate f x <*> somePlate f y <*> somePlate f i-    StrReplace x y y'    -> StrReplace    <$> somePlate f x <*> somePlate f y <*> somePlate f y'-    StrReplaceAll x y y' -> StrReplaceAll <$> somePlate f x <*> somePlate f y <*> somePlate f y'-    ForAll (Just qv) qexpr -> ForAll (Just qv) . const <$> somePlate f (qexpr (Var qv))-    ForAll Nothing qexpr   -> pure $ ForAll Nothing qexpr-    Exists (Just qv) qexpr -> Exists (Just qv) . const <$> somePlate f (qexpr (Var qv))-    Exists Nothing qexpr   -> pure $ Exists Nothing qexpr

@@ -1,187 +0,0 @@--- Required for class constraints of form: c (ValueType t) :: Constraint-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE DefaultSignatures #-}--module Language.Hasmtlib.Orderable where--import Prelude hiding (not, (&&), (||))-import Language.Hasmtlib.Internal.Expr-import Language.Hasmtlib.Type.SMTSort-import Language.Hasmtlib.Equatable-import Language.Hasmtlib.Iteable-import Language.Hasmtlib.Boolean-import Data.Int-import Data.Word-import Data.Void-import Data.Tree (Tree)-import Data.Monoid (Sum, Product, First, Last, Dual)-import Data.Functor.Identity (Identity)-import Numeric.Natural-import GHC.Generics-import GHC.TypeNats---- | Compare two as as SMT-Expression.------   You can derive an instance of this class if your type is 'Generic'.------ @--- x <- var @RealSort--- y <- var--- assert $ x >? y--- assert $ x === min' 42 100--- @----class Equatable a => Orderable a where-  (<=?) :: a -> a -> Expr BoolSort-  default (<=?) :: (Generic a, GOrderable (Rep a)) => a -> a -> Expr BoolSort-  x <=? y = from x <=?# from y--  (>=?) :: a -> a -> Expr BoolSort-  x >=? y = y <=? x--  (<?)  :: a -> a -> Expr BoolSort-  x <? y = not $ y <=? x--  (>?)  :: a -> a -> Expr BoolSort-  x >? y = not $ x <=? y--infix 4 <?, <=?, >=?, >?---- | Minimum of two as SMT-Expression.-min' :: (Orderable a, Iteable (Expr BoolSort) a) => a -> a -> a-min' x y = ite (x <=? y) x y---- | Maximum of two as SMT-Expression.-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-  (<?)     = BvuLT-  {-# INLINE (<?) #-}-  (<=?)    = BvuLTHE-  {-# INLINE (<=?) #-}-  (>=?)    = BvuGTHE-  {-# INLINE (>=?) #-}-  (>?)     = BvuGT-  {-# 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--instance GOrderable U1 where-  U1 <?#  U1 = false-  U1 <=?# U1 = true--instance GOrderable V1 where-  x <?# y = x `seq` y `seq` error "GOrderable[V1].<?#"-  x <=?# y = x `seq` y `seq` error "GOrderable[V1].<=?#"--instance (GOrderable f, GOrderable g) => GOrderable (f :*: g) where-  (a :*: b) <?#  (c :*: d) = (a <?# c) || (a ===# c && b <?# d)-  (a :*: b) <=?# (c :*: d) = (a <?# c) || (a ===# c && b <=?# d)--instance (GOrderable f, GOrderable g) => GOrderable (f :+: g) where-  L1 _ <?# R1 _ = true-  L1 a <?# L1 b = a <?# b-  R1 a <?# R1 b = a <?# b-  R1 _ <?# L1 _ = false--  L1 _ <=?# R1 _ = true-  L1 a <=?# L1 b = a <=?# b-  R1 a <=?# R1 b = a <=?# b-  R1 _ <=?# L1 _ = false--instance GOrderable f => GOrderable (M1 i c f) where-  M1 x <?#  M1 y = x <?#  y-  M1 x <=?# M1 y = x <=?# y--instance Orderable a => GOrderable (K1 i a) where-  K1 a <?#  K1 b = a <?  b-  K1 a <=?# K1 b = a <=? b---- Boring instances that end up being useful when deriving Orderable with Generics--instance Orderable ()       where _ <?  _ = false-                                  _ <=? _ = true-instance Orderable Void     where x <?  y = x `seq` y `seq` error "Orderable[Void].<?"-                                  x <=? y = x `seq` y `seq` error "Orderable[Void].<=?"-instance Orderable Int      where x <?  y = bool (x <  y)-                                  x <=? y = bool (x <= y)-instance Orderable Integer  where x <?  y = bool (x <  y)-                                  x <=? y = bool (x <= y)-instance Orderable Natural  where x <?  y = bool (x <  y)-                                  x <=? y = bool (x <= y)-instance Orderable Word     where x <?  y = bool (x <  y)-                                  x <=? y = bool (x <= y)-instance Orderable Word8    where x <?  y = bool (x <  y)-                                  x <=? y = bool (x <= y)-instance Orderable Word16   where x <?  y = bool (x <  y)-                                  x <=? y = bool (x <= y)-instance Orderable Word32   where x <?  y = bool (x <  y)-                                  x <=? y = bool (x <= y)-instance Orderable Word64   where x <?  y = bool (x <  y)-                                  x <=? y = bool (x <= y)-instance Orderable Int8     where x <?  y = bool (x <  y)-                                  x <=? y = bool (x <= y)-instance Orderable Int16    where x <?  y = bool (x <  y)-                                  x <=? y = bool (x <= y)-instance Orderable Int32    where x <?  y = bool (x <  y)-                                  x <=? y = bool (x <= y)-instance Orderable Int64    where x <?  y = bool (x <  y)-                                  x <=? y = bool (x <= y)-instance Orderable Char     where x <?  y = bool (x <  y)-                                  x <=? y = bool (x <= y)-instance Orderable Float    where x <?  y = bool (x <  y)-                                  x <=? y = bool (x <= y)-instance Orderable Double   where x <?  y = bool (x <  y)-                                  x <=? y = bool (x <= y)-instance Orderable Ordering where x <?  y = bool (x <  y)-                                  x <=? y = bool (x <= y)-instance Orderable Bool     where x <?  y = bool (x <  y)-                                  x <=? y = bool (x <= y)--instance (Orderable a, Orderable b) => Orderable (a,b)-instance (Orderable a, Orderable b, Orderable c) => Orderable (a,b,c)-instance (Orderable a, Orderable b, Orderable c, Orderable d) => Orderable (a,b,c,d)-instance (Orderable a, Orderable b, Orderable c, Orderable d, Orderable e) => Orderable (a,b,c,d,e)-instance (Orderable a, Orderable b, Orderable c, Orderable d, Orderable e, Orderable f) => Orderable (a,b,c,d,e,f)-instance (Orderable a, Orderable b, Orderable c, Orderable d, Orderable e, Orderable f, Orderable g) => Orderable (a,b,c,d,e,f,g)-instance (Orderable a, Orderable b, Orderable c, Orderable d, Orderable e, Orderable f, Orderable g, Orderable h) => Orderable (a,b,c,d,e,f,g,h)-instance Orderable a => Orderable [a]-instance Orderable a => Orderable (Tree a)-instance Orderable a => Orderable (Maybe a)-instance (Orderable a, Orderable b) => Orderable (Either a b)-instance Orderable a => Orderable (Sum a)-instance Orderable a => Orderable (Product a)-instance Orderable a => Orderable (First a)-instance Orderable a => Orderable (Last a)-instance Orderable a => Orderable (Dual a)-instance Orderable a => Orderable (Identity a)

@@ -1,174 +1,1241 @@-{-# LANGUAGE AllowAmbiguousTypes #-}-{-# LANGUAGE ViewPatterns #-}--module Language.Hasmtlib.Type.Expr- ( SMTVar(..), varId- , Value(..), unwrapValue, wrapValue- , Expr(..)- , equal, distinct- , bvShL, bvLShR, bvConcat, bvRotL, bvRotR- , toIntSort, toRealSort, isIntSort- , for_all , exists- , select, store- , strLength, strAt, strSubstring, strPrefixOf, strSuffixOf, strContains, strIndexOf, strReplace, strReplaceAll- )-where--import Language.Hasmtlib.Internal.Expr-import Language.Hasmtlib.Internal.Expr.Num ()-import Language.Hasmtlib.Type.SMTSort-import Language.Hasmtlib.Boolean-import Data.Proxy-import Data.List (genericLength)-import Data.Foldable (toList)-import qualified Data.Vector.Sized as V-import GHC.TypeNats---- | Test multiple expressions on equality within in the 'SMT'-Problem.-equal :: (Eq (HaskellType t), KnownSMTSort t, Foldable f) => f (Expr t) -> Expr BoolSort-equal (toList -> (a:b:xs)) = case someNatVal (genericLength xs) of-  SomeNat n -> case V.fromListN' n xs of-    Nothing  -> EQU $ V.fromTuple (a,b)-    Just xs' -> EQU $ xs' V.++ V.fromTuple (a,b)-equal (toList -> _)        = true---- | Test multiple expressions on distinctness within in the 'SMT'-Problem.-distinct :: (Eq (HaskellType t), KnownSMTSort t, Foldable f) => f (Expr t) -> Expr BoolSort-distinct (toList -> (a:b:xs)) = case someNatVal (genericLength xs) of-  SomeNat n -> case V.fromListN' n xs of-    Nothing  -> Distinct $ V.fromTuple (a,b)-    Just xs' -> Distinct $ xs' V.++ V.fromTuple (a,b)-distinct (toList -> _)        = true---- | A universal quantification for any specific 'SMTSort'.---   If the type cannot be inferred, apply a type-annotation.---   Nested quantifiers are also supported.------   Usage:------   @---   assert $---      for_all @IntSort $ \x ->---         x + 0 === x && 0 + x === x---   @------   The lambdas 'x' is all-quantified here.---   It will only be scoped for the lambdas body.-for_all :: forall t. KnownSMTSort t => (Expr t -> Expr BoolSort) -> Expr BoolSort-for_all = ForAll Nothing---- | An existential quantification for any specific 'SMTSort'---   If the type cannot be inferred, apply a type-annotation.---   Nested quantifiers are also supported.------   Usage:------   @---   assert $---      for_all @(BvSort 8) $ \x ->---          exists $ \y ->---            x - y === 0---   @------   The lambdas 'y' is existentially quantified here.---   It will only be scoped for the lambdas body.-exists :: forall t. KnownSMTSort t => (Expr t -> Expr BoolSort) -> Expr BoolSort-exists = Exists Nothing---- | Select a value from an array.-select :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v-select = ArrSelect---- | Store a value in an array.-store :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v -> Expr (ArraySort k v)-store = ArrStore---- | Bitvector shift left-bvShL    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)-bvShL    = BvShL-{-# INLINE bvShL #-}---- | Bitvector logical shift right-bvLShR   :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)-bvLShR   = BvLShR-{-# INLINE bvLShR #-}---- | Concat two bitvectors-bvConcat :: (KnownNat n, KnownNat m) => Expr (BvSort n) -> Expr (BvSort m) -> Expr (BvSort (n + m))-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---- | Converts an expression of type 'RealSort' to type 'IntSort'.-toIntSort :: Expr RealSort -> Expr IntSort-toIntSort = ToInt---- | Checks whether an expression of type 'RealSort' may be safely converted to type 'IntSort'.-isIntSort :: Expr RealSort -> Expr BoolSort-isIntSort = IsInt---- | Length of a string.-strLength :: Expr StringSort -> Expr IntSort-strLength = StrLength---- | Singleton string containing a character at given position---   or empty string when position is out of range.---   The leftmost position is 0.-strAt :: Expr StringSort -> Expr IntSort -> Expr StringSort-strAt = StrAt---- | @(strSubstring s i n)@ evaluates to the longest (unscattered) substring---   of @s@ of length at most @n@ starting at position @i@.---   It evaluates to the empty string if @n@ is negative or @i@ is not in---   the interval @[0,l-1]@ where @l@ is the length of @s@.-strSubstring :: Expr StringSort -> Expr IntSort -> Expr IntSort -> Expr StringSort-strSubstring = StrSubstring---- | First string is a prefix of second one.---   @(str.prefixof s t)@ is @true@ iff @s@ is a prefix of @t@.-strPrefixOf :: Expr StringSort -> Expr StringSort -> Expr BoolSort-strPrefixOf = StrPrefixOf---- | First string is a suffix of second one.---   @(str.suffixof s t)@ is @true@ iff @s@ is a suffix of @t@.-strSuffixOf :: Expr StringSort -> Expr StringSort -> Expr BoolSort-strSuffixOf = StrSuffixOf---- | First string contains second one---   @(str.contains s t)@ iff @s@ contains @t@.-strContains :: Expr StringSort -> Expr StringSort -> Expr BoolSort-strContains = StrContains---- | Index of first occurrence of second string in first one starting at the position specified by the third argument.---   @(str.indexof s t i)@, with @0 <= i <= |s|@ is the position of the first---   occurrence of @t@ in @s@ at or after position @i@, if any.---   Otherwise, it is @-1@. Note that the result is @i@ whenever @i@ is within---   the range @[0, |s|]@ and @t@ is empty.-strIndexOf :: Expr StringSort -> Expr StringSort -> Expr IntSort -> Expr IntSort-strIndexOf = StrIndexOf---- | @(str.replace s t t')@ is the string obtained by replacing the first---   occurrence of @t@ in @s@, if any, by @t'@. Note that if @t@ is empty, the---   result is to prepend @t'@ to @s@; also, if @t@ does not occur in @s@ then---   the result is @s@.-strReplace :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort-strReplace = StrReplace---- | @(str.replace_all s t t’)@ is @s@ if @t@ is the empty string. Otherwise, it---   is the string obtained from @s@ by replacing all occurrences of @t@ in @s@---   by @t’@, starting with the first occurrence and proceeding in left-to-right order.-strReplaceAll :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort-strReplaceAll = StrReplaceAll+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE DefaultSignatures #-}+{-# LANGUAGE DerivingStrategies #-}++module Language.Hasmtlib.Type.Expr where++import Prelude hiding (Integral(..), not, and, or, any, all, (&&), (||))+import Language.Hasmtlib.Internal.Render+import Language.Hasmtlib.Internal.Uniplate1+import Language.Hasmtlib.Type.ArrayMap+import Language.Hasmtlib.Type.SMTSort+import Language.Hasmtlib.Integraled+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.Int+import Data.Word+import Data.Void+import Data.Sequence (Seq)+import Data.Tree (Tree)+import Data.Monoid (Sum, Product, First, Last, Dual)+import Data.String (IsString(..))+import Data.Text (pack)+import Data.List(genericLength)+import Data.Foldable (toList)+import Data.ByteString.Builder+import Data.ByteString.Lazy.UTF8 (toString)+import qualified Data.Vector.Sized as V+import Control.Lens hiding (from, to)+import GHC.TypeLits hiding (someNatVal)+import GHC.TypeNats (someNatVal)+import GHC.Generics++-- | An internal SMT variable with a phantom-type which holds an 'Int' as it's identifier.+type role SMTVar phantom+newtype SMTVar (t :: SMTSort) = SMTVar { _varId :: Int }+  deriving stock (Show, Generic)+  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, ...).+data Expr (t :: SMTSort) where+  Var       :: SMTVar t -> Expr t+  Constant  :: Value  t -> Expr t++  Plus      :: 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+  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+  Sin       :: Expr RealSort -> Expr RealSort+  Cos       :: Expr RealSort -> Expr RealSort+  Tan       :: Expr RealSort -> Expr RealSort+  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+  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+  StrSuffixOf   :: Expr StringSort -> Expr StringSort -> Expr BoolSort+  StrContains   :: Expr StringSort -> Expr StringSort -> Expr BoolSort+  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.+isLeaf :: Expr t -> Bool+isLeaf (Var _) = True+isLeaf (Constant _) = True+isLeaf Pi = True+isLeaf _ = False+{-# INLINE isLeaf #-}++-- | If condition (p :: b) then (t :: a) else (f :: a)+--+--    >>> ite true "1" "2"+--        "1"+--    >>> ite false 100 42+--        42+class Iteable b a where+  ite :: b -> a -> a -> a+  default ite :: (Iteable b c, Applicative f, f c ~ a) => b -> a -> a -> a+  ite p t f = ite p <$> t <*> f++instance Iteable (Expr BoolSort) (Expr t) where+  ite = Ite+  {-# INLINE ite #-}++instance Iteable Bool a where+  ite p t f = if p then t else f+  {-# INLINE ite #-}++instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) [a]+instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Maybe a)+instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Seq a)+instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Tree a)+instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Sum a)+instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Product a)+instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (First a)+instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Last a)+instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Dual a)+instance Iteable (Expr BoolSort) a => Iteable (Expr BoolSort) (Identity a)++instance Iteable (Expr BoolSort) () where+  ite _ _ _ = ()++instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b) => Iteable (Expr BoolSort) (a,b) where+  ite p (a,b) (a',b') = (ite p a a', ite p b b')++instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c) => Iteable (Expr BoolSort) (a,b,c) where+  ite p (a,b,c) (a',b',c') = (ite p a a', ite p b b', ite p c c')++instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d) => Iteable (Expr BoolSort) (a,b,c,d) where+  ite p (a,b,c,d) (a',b',c',d') = (ite p a a', ite p b b', ite p c c', ite p d d')++instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d, Iteable (Expr BoolSort) e) => Iteable (Expr BoolSort) (a,b,c,d,e) where+  ite p (a,b,c,d,e) (a',b',c',d',e') = (ite p a a', ite p b b', ite p c c', ite p d d', ite p e e')++instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d, Iteable (Expr BoolSort) e, Iteable (Expr BoolSort) f) => Iteable (Expr BoolSort) (a,b,c,d,e,f) where+  ite p (a,b,c,d,e,f) (a',b',c',d',e',f') = (ite p a a', ite p b b', ite p c c', ite p d d', ite p e e', ite p f f')++instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d, Iteable (Expr BoolSort) e, Iteable (Expr BoolSort) f, Iteable (Expr BoolSort) g) => Iteable (Expr BoolSort) (a,b,c,d,e,f,g) where+  ite p (a,b,c,d,e,f,g) (a',b',c',d',e',f',g') = (ite p a a', ite p b b', ite p c c', ite p d d', ite p e e', ite p f f', ite p g g')++instance (Iteable (Expr BoolSort) a, Iteable (Expr BoolSort) b, Iteable (Expr BoolSort) c, Iteable (Expr BoolSort) d, Iteable (Expr BoolSort) e, Iteable (Expr BoolSort) f, Iteable (Expr BoolSort) g, Iteable (Expr BoolSort) h) => Iteable (Expr BoolSort) (a,b,c,d,e,f,g,h) where+  ite p (a,b,c,d,e,f,g,h) (a',b',c',d',e',f',g',h') = (ite p a a', ite p b b', ite p c c', ite p d d', ite p e e', ite p f f', ite p g g', ite p h h')++-- | Test two as on equality as SMT-Expression.+--+--   You can derive an instance of this class if your type is 'Generic'.+--+-- @+--     x <- var @RealType+--     y <- var+--     assert $ y === x && not (y /== x)+-- @+--+class Equatable a where+  -- | Test whether two values are equal in the SMT-Problem.+  (===) :: a -> a -> Expr BoolSort+  default (===) :: (Generic a, GEquatable (Rep a)) => a -> a -> Expr BoolSort+  a === b = from a ===# from b++  -- | Test whether two values are not equal in the SMT-Problem.+  (/==) :: a -> a -> Expr BoolSort+  x /== y = not $ x === y++infix 4 ===, /==++instance (KnownSMTSort t, Eq (HaskellType t)) => Equatable (Expr t) where+  x === y = EQU $ V.fromTuple (x,y)+  {-# INLINE (===) #-}+  x /== y = Distinct $ V.fromTuple (x,y)+  {-# INLINE (/==) #-}++class GEquatable f where+  (===#) :: f a -> f a -> Expr BoolSort++instance GEquatable U1 where+  U1 ===# U1 = true++instance GEquatable V1 where+  x ===# y = x `seq` y `seq` error "GEquatable[V1].===#"++instance (GEquatable f, GEquatable g) => GEquatable (f :*: g) where+  (a :*: b) ===# (c :*: d) = (a ===# c) && (b ===# d)++instance (GEquatable f, GEquatable g) => GEquatable (f :+: g) where+  L1 a ===# L1 b = a ===# b+  R1 a ===# R1 b = a ===# b+  _ ===# _ = false++instance GEquatable f => GEquatable (M1 i c f) where+  M1 x ===# M1 y = x ===# y++instance Equatable a => GEquatable (K1 i a) where+  K1 a ===# K1 b = a === b++instance Equatable ()       where _ === _ = true+instance Equatable Void     where x === y = x `seq` y `seq` error "Equatable[Void].==="+instance Equatable Int      where x === y = bool (x == y)+instance Equatable Integer  where x === y = bool (x == y)+instance Equatable Natural  where x === y = bool (x == y)+instance Equatable Word     where x === y = bool (x == y)+instance Equatable Word8    where x === y = bool (x == y)+instance Equatable Word16   where x === y = bool (x == y)+instance Equatable Word32   where x === y = bool (x == y)+instance Equatable Word64   where x === y = bool (x == y)+instance Equatable Int8     where x === y = bool (x == y)+instance Equatable Int16    where x === y = bool (x == y)+instance Equatable Int32    where x === y = bool (x == y)+instance Equatable Int64    where x === y = bool (x == y)+instance Equatable Char     where x === y = bool (x == y)+instance Equatable Float    where x === y = bool (x == y)+instance Equatable Double   where x === y = bool (x == y)+instance Equatable Ordering where x === y = bool (x == y)+instance Equatable Bool     where x === y = bool (x == y)+instance (Equatable a, Equatable b) => Equatable (a,b)+instance (Equatable a, Equatable b, Equatable c) => Equatable (a,b,c)+instance (Equatable a, Equatable b, Equatable c, Equatable d) => Equatable (a,b,c,d)+instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e) => Equatable (a,b,c,d,e)+instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e, Equatable f) => Equatable (a,b,c,d,e,f)+instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e, Equatable f, Equatable g) => Equatable (a,b,c,d,e,f,g)+instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e, Equatable f, Equatable g, Equatable h) => Equatable (a,b,c,d,e,f,g,h)+instance Equatable a => Equatable [a]+instance Equatable a => Equatable (Tree a)+instance Equatable a => Equatable (Maybe a)+instance (Equatable a, Equatable b) => Equatable (Either a b)+instance Equatable a => Equatable (Sum a)+instance Equatable a => Equatable (Product a)+instance Equatable a => Equatable (First a)+instance Equatable a => Equatable (Last a)+instance Equatable a => Equatable (Dual a)+instance Equatable a => Equatable (Identity a)++-- | Compare two as as SMT-Expression.+--+--   You can derive an instance of this class if your type is 'Generic'.+--+-- @+-- x <- var @RealSort+-- y <- var+-- assert $ x >? y+-- assert $ x === min' 42 100+-- @+--+class Equatable a => Orderable a where+  (<=?) :: a -> a -> Expr BoolSort+  default (<=?) :: (Generic a, GOrderable (Rep a)) => a -> a -> Expr BoolSort+  x <=? y = from x <=?# from y++  (>=?) :: a -> a -> Expr BoolSort+  x >=? y = y <=? x++  (<?)  :: a -> a -> Expr BoolSort+  x <? y = not $ y <=? x++  (>?)  :: a -> a -> Expr BoolSort+  x >? y = not $ x <=? y++infix 4 <?, <=?, >=?, >?++-- | Minimum of two as SMT-Expression.+min' :: (Orderable a, Iteable (Expr BoolSort) a) => a -> a -> a+min' x y = ite (x <=? y) x y++-- | Maximum of two as SMT-Expression.+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+  (<?)     = BvuLT+  {-# INLINE (<?) #-}+  (<=?)    = BvuLTHE+  {-# INLINE (<=?) #-}+  (>=?)    = BvuGTHE+  {-# INLINE (>=?) #-}+  (>?)     = BvuGT+  {-# 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++instance GOrderable U1 where+  U1 <?#  U1 = false+  U1 <=?# U1 = true++instance GOrderable V1 where+  x <?# y = x `seq` y `seq` error "GOrderable[V1].<?#"+  x <=?# y = x `seq` y `seq` error "GOrderable[V1].<=?#"++instance (GOrderable f, GOrderable g) => GOrderable (f :*: g) where+  (a :*: b) <?#  (c :*: d) = (a <?# c) || (a ===# c && b <?# d)+  (a :*: b) <=?# (c :*: d) = (a <?# c) || (a ===# c && b <=?# d)++instance (GOrderable f, GOrderable g) => GOrderable (f :+: g) where+  L1 _ <?# R1 _ = true+  L1 a <?# L1 b = a <?# b+  R1 a <?# R1 b = a <?# b+  R1 _ <?# L1 _ = false++  L1 _ <=?# R1 _ = true+  L1 a <=?# L1 b = a <=?# b+  R1 a <=?# R1 b = a <=?# b+  R1 _ <=?# L1 _ = false++instance GOrderable f => GOrderable (M1 i c f) where+  M1 x <?#  M1 y = x <?#  y+  M1 x <=?# M1 y = x <=?# y++instance Orderable a => GOrderable (K1 i a) where+  K1 a <?#  K1 b = a <?  b+  K1 a <=?# K1 b = a <=? b++-- Boring instances that end up being useful when deriving Orderable with Generics++instance Orderable ()       where _ <?  _ = false+                                  _ <=? _ = true+instance Orderable Void     where x <?  y = x `seq` y `seq` error "Orderable[Void].<?"+                                  x <=? y = x `seq` y `seq` error "Orderable[Void].<=?"+instance Orderable Int      where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Integer  where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Natural  where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Word     where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Word8    where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Word16   where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Word32   where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Word64   where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Int8     where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Int16    where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Int32    where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Int64    where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Char     where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Float    where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Double   where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Ordering where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)+instance Orderable Bool     where x <?  y = bool (x <  y)+                                  x <=? y = bool (x <= y)++instance (Orderable a, Orderable b) => Orderable (a,b)+instance (Orderable a, Orderable b, Orderable c) => Orderable (a,b,c)+instance (Orderable a, Orderable b, Orderable c, Orderable d) => Orderable (a,b,c,d)+instance (Orderable a, Orderable b, Orderable c, Orderable d, Orderable e) => Orderable (a,b,c,d,e)+instance (Orderable a, Orderable b, Orderable c, Orderable d, Orderable e, Orderable f) => Orderable (a,b,c,d,e,f)+instance (Orderable a, Orderable b, Orderable c, Orderable d, Orderable e, Orderable f, Orderable g) => Orderable (a,b,c,d,e,f,g)+instance (Orderable a, Orderable b, Orderable c, Orderable d, Orderable e, Orderable f, Orderable g, Orderable h) => Orderable (a,b,c,d,e,f,g,h)+instance Orderable a => Orderable [a]+instance Orderable a => Orderable (Tree a)+instance Orderable a => Orderable (Maybe a)+instance (Orderable a, Orderable b) => Orderable (Either a b)+instance Orderable a => Orderable (Sum a)+instance Orderable a => Orderable (Product a)+instance Orderable a => Orderable (First a)+instance Orderable a => Orderable (Last a)+instance Orderable a => Orderable (Dual a)+instance Orderable a => Orderable (Identity a)++-- | Test multiple expressions on equality within in the 'SMT'-Problem.+equal :: (Eq (HaskellType t), KnownSMTSort t, Foldable f) => f (Expr t) -> Expr BoolSort+equal (toList -> (a:b:xs)) = case someNatVal (genericLength xs) of+  SomeNat n -> case V.fromListN' n xs of+    Nothing  -> EQU $ V.fromTuple (a,b)+    Just xs' -> EQU $ xs' V.++ V.fromTuple (a,b)+equal (toList -> _)        = true++-- | Test multiple expressions on distinctness within in the 'SMT'-Problem.+distinct :: (Eq (HaskellType t), KnownSMTSort t, Foldable f) => f (Expr t) -> Expr BoolSort+distinct (toList -> (a:b:xs)) = case someNatVal (genericLength xs) of+  SomeNat n -> case V.fromListN' n xs of+    Nothing  -> Distinct $ V.fromTuple (a,b)+    Just xs' -> Distinct $ xs' V.++ V.fromTuple (a,b)+distinct (toList -> _)        = true++-- | A universal quantification for any specific 'SMTSort'.+--   If the type cannot be inferred, apply a type-annotation.+--   Nested quantifiers are also supported.+--+--   Usage:+--+--   @+--   assert $+--      for_all @IntSort $ \x ->+--         x + 0 === x && 0 + x === x+--   @+--+--   The lambdas 'x' is all-quantified here.+--   It will only be scoped for the lambdas body.+for_all :: forall t. KnownSMTSort t => (Expr t -> Expr BoolSort) -> Expr BoolSort+for_all = ForAll Nothing+{-# INLINE for_all #-}++-- | An existential quantification for any specific 'SMTSort'+--   If the type cannot be inferred, apply a type-annotation.+--   Nested quantifiers are also supported.+--+--   Usage:+--+--   @+--   assert $+--      for_all @(BvSort 8) $ \x ->+--          exists $ \y ->+--            x - y === 0+--   @+--+--   The lambdas 'y' is existentially quantified here.+--   It will only be scoped for the lambdas body.+exists :: forall t. KnownSMTSort t => (Expr t -> Expr BoolSort) -> Expr BoolSort+exists = Exists Nothing+{-# 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 = ArrSelect+{-# INLINE select #-}++-- | Store a value in an array.+store :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Expr (ArraySort k v) -> Expr k -> Expr v -> Expr (ArraySort k v)+store = ArrStore+{-# INLINE store #-}++-- | Bitvector shift left+bvShL    :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)+bvShL    = BvShL+{-# INLINE bvShL #-}++-- | Bitvector logical shift right+bvLShR   :: KnownNat n => Expr (BvSort n) -> Expr (BvSort n) -> Expr (BvSort n)+bvLShR   = BvLShR+{-# INLINE bvLShR #-}++-- | Concat two bitvectors+bvConcat :: (KnownNat n, KnownNat m) => Expr (BvSort n) -> Expr (BvSort m) -> Expr (BvSort (n + m))+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+{-# INLINE toRealSort #-}++-- | Converts an expression of type 'RealSort' to type 'IntSort'.+toIntSort :: Expr RealSort -> Expr IntSort+toIntSort = ToInt+{-# INLINE toIntSort #-}++-- | Checks whether an expression of type 'RealSort' may be safely converted to type 'IntSort'.+isIntSort :: Expr RealSort -> Expr BoolSort+isIntSort = IsInt+{-# INLINE isIntSort #-}++-- | Length of a string.+strLength :: Expr StringSort -> Expr IntSort+strLength = StrLength+{-# INLINE strLength #-}++-- | Singleton string containing a character at given position+--   or empty string when position is out of range.+--   The leftmost position is 0.+strAt :: Expr StringSort -> Expr IntSort -> Expr StringSort+strAt = StrAt+{-# INLINE strAt #-}++-- | @(strSubstring s i n)@ evaluates to the longest (unscattered) substring+--   of @s@ of length at most @n@ starting at position @i@.+--   It evaluates to the empty string if @n@ is negative or @i@ is not in+--   the interval @[0,l-1]@ where @l@ is the length of @s@.+strSubstring :: Expr StringSort -> Expr IntSort -> Expr IntSort -> Expr StringSort+strSubstring = StrSubstring+{-# INLINE strSubstring #-}++-- | First string is a prefix of second one.+--   @(str.prefixof s t)@ is @true@ iff @s@ is a prefix of @t@.+strPrefixOf :: Expr StringSort -> Expr StringSort -> Expr BoolSort+strPrefixOf = StrPrefixOf+{-# INLINE strPrefixOf #-}++-- | First string is a suffix of second one.+--   @(str.suffixof s t)@ is @true@ iff @s@ is a suffix of @t@.+strSuffixOf :: Expr StringSort -> Expr StringSort -> Expr BoolSort+strSuffixOf = StrSuffixOf+{-# INLINE strSuffixOf #-}++-- | First string contains second one+--   @(str.contains s t)@ iff @s@ contains @t@.+strContains :: Expr StringSort -> Expr StringSort -> Expr BoolSort+strContains = StrContains+{-# INLINE strContains #-}++-- | Index of first occurrence of second string in first one starting at the position specified by the third argument.+--   @(str.indexof s t i)@, with @0 <= i <= |s|@ is the position of the first+--   occurrence of @t@ in @s@ at or after position @i@, if any.+--   Otherwise, it is @-1@. Note that the result is @i@ whenever @i@ is within+--   the range @[0, |s|]@ and @t@ is empty.+strIndexOf :: Expr StringSort -> Expr StringSort -> Expr IntSort -> Expr IntSort+strIndexOf = StrIndexOf+{-# INLINE strIndexOf #-}++-- | @(str.replace s t t')@ is the string obtained by replacing the first+--   occurrence of @t@ in @s@, if any, by @t'@. Note that if @t@ is empty, the+--   result is to prepend @t'@ to @s@; also, if @t@ does not occur in @s@ then+--   the result is @s@.+strReplace :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort+strReplace = StrReplace+{-# INLINE strReplace #-}++-- | @(str.replace_all s t t’)@ is @s@ if @t@ is the empty string. Otherwise, it+--   is the string obtained from @s@ by replacing all occurrences of @t@ in @s@+--   by @t’@, starting with the first occurrence and proceeding in left-to-right order.+strReplaceAll :: Expr StringSort -> Expr StringSort -> Expr StringSort -> Expr StringSort+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 = Plus x (Neg 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+   {-# INLINE fromInteger #-}+   (Constant (RealValue 0)) + y = y+   x + (Constant (RealValue 0)) = x+   (Constant (RealValue x)) + (Constant (RealValue y)) = Constant (RealValue (x + y))+   x + y = Plus x y+   {-# INLINE (+) #-}+   x - (Constant (RealValue 0)) = x+   (Constant (RealValue x)) - (Constant (RealValue y)) = Constant (RealValue (x - y))+   x - y = Plus x (Neg 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))+   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 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 = BvAdd x y+   {-# INLINE (+) #-}+   x - (Constant (BvValue 0)) = x+   (Constant (BvValue x)) - (Constant (BvValue y)) = Constant (BvValue (x - y))+   x - y = BvSub 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+   {-# INLINE (*) #-}+   abs         = id+   {-# INLINE abs #-}+   signum _    = 0+   {-# 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 / y          = Div x y+  {-# INLINE (/) #-}++-- | Not in the SMTLib2.6-standard. Solvers like CVC5 and MathSAT support it though.+instance Floating (Expr RealSort) where+    pi    = Pi+    {-# INLINE pi #-}+    exp   = Exp+    {-# INLINE exp #-}+    log   = error "SMT-Solvers currently do not support log"+    sqrt  = Sqrt+    {-# INLINE sqrt #-}+    sin   = Sin+    {-# INLINE sin #-}+    cos   = Cos+    {-# INLINE cos #-}+    tan   = Tan+    {-# INLINE tan #-}+    asin  = Asin+    {-# INLINE asin #-}+    acos  = Acos+    {-# INLINE acos #-}+    atan  = Atan+    {-# INLINE atan #-}+    sinh  = error "SMT-Solvers currently do not support sinh"+    cosh  = error "SMT-Solvers currently do not support cosh"+    tanh  = error "SMT-Solvers currently do not support tanh"+    asinh = error "SMT-Solvers currently do not support asinh"+    acosh = error "SMT-Solvers currently do not support acosh"+    atanh = error "SMT-Solvers currently do not support atanh"++instance Integraled (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 #-}++instance KnownNat n => Integraled (Expr (BvSort n)) where+  quot        = BvuDiv+  {-# INLINE quot #-}+  rem         = BvuRem+  {-# INLINE rem #-}+  div         = BvuDiv+  {-# INLINE div #-}+  mod         = BvuRem+  {-# INLINE mod #-}+  quotRem x y = (quot x y, rem x y)+  {-# INLINE quotRem #-}+  divMod x y  = (div x y, mod x y)+  {-# INLINE divMod #-}++instance Boolean (Expr BoolSort) where+  bool = Constant . BoolValue+  {-# INLINE bool #-}+  (&&) = And+  {-# INLINE (&&) #-}+  (||) = Or+  {-# INLINE (||) #-}+  not  = Not+  {-# INLINE not #-}+  xor  = Xor+  {-# INLINE xor #-}+  (<==>) = (===)+  {-# INLINE (<==>) #-}++instance KnownNat n => Boolean (Expr (BvSort n)) where+  bool = Constant . BvValue . bool+  {-# INLINE bool #-}+  (&&) = BvAnd+  {-# INLINE (&&) #-}+  (||) = BvOr+  {-# INLINE (||) #-}+  not  = BvNot+  {-# INLINE not #-}+  xor  = BvXor+  {-# INLINE xor #-}++instance Bounded (Expr BoolSort) where+  minBound = false+  maxBound = true++instance KnownNat n => Bounded (Expr (BvSort n)) where+  minBound = Constant $ BvValue minBound+  maxBound = Constant $ BvValue maxBound++instance Semigroup (Expr StringSort) where+  (<>) = StrConcat+  {-# INLINE (<>) #-}++instance Monoid (Expr StringSort) where+  mempty = Constant $ StringValue mempty+  {-# INLINE mempty #-}+  mappend = (<>)+  {-# INLINE mappend #-}++instance IsString (Expr StringSort) where+  fromString = Constant . StringValue . pack+  {-# INLINE fromString #-}++instance Render (SMTVar t) where+  render v = "var_" <> intDec (coerce @(SMTVar t) @Int v)+  {-# INLINE render #-}++instance Render (Value t) where+  render (IntValue x)   = render x+  render (RealValue x)  = render x+  render (BoolValue x)  = render x+  render (BvValue   v)  = "#b" <> render v+  render (ArrayValue arr) = case minViewWithKey (arr^.stored) of+    Nothing -> constRender $ arr^.arrConst+    Just ((k,v), stored')+      | size (arr^.stored) > 1 -> render $ ArrStore (Constant (wrapValue (arr & stored .~ stored'))) (Constant (wrapValue k)) (Constant (wrapValue v))+      | 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 _ = sortSing @(ArraySort k v)+  render (StringValue x) = "\"" <> render x <> "\""++instance KnownSMTSort t => Render (Expr t) where+  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 (Abs x)      = renderUnary  "abs" x+  render (Mod x y)    = renderBinary "mod" x y+  render (IDiv x y)   = renderBinary "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 (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 (Not x)      = renderUnary  "not" x+  render (And x y)    = renderBinary "and" x y+  render (Or x y)     = renderBinary "or" x y+  render (Impl x y)   = renderBinary "=>" x y+  render (Xor x y)    = renderBinary "xor" x y++  render Pi           = "real.pi"+  render (Sqrt x)     = renderUnary "sqrt" x+  render (Exp x)      = renderUnary "exp" x+  render (Sin x)      = renderUnary "sin" x+  render (Cos x)      = renderUnary "cos" x+  render (Tan x)      = renderUnary "tan" x+  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 (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 (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)+  render (StrSuffixOf x y)      = renderBinary "str.suffixof" (render x) (render y)+  render (StrContains x y)      = renderBinary "str.contains" (render x) (render y)+  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++renderQuantifier :: forall t. KnownSMTSort t => Builder -> Maybe (SMTVar t) -> (Expr t -> Expr BoolSort) -> Builder+renderQuantifier qname (Just qvar) f =+  renderBinary+    qname+    ("(" <> renderUnary (render qvar) (sortSing @t) <> ")")+    expr+  where+    expr = render $ f $ Var qvar+renderQuantifier _ Nothing _ = mempty++instance Show (Value t) where+  show = toString . toLazyByteString . render++instance KnownSMTSort t => Show (Expr t) where+  show = toString . toLazyByteString . render++type instance Index   (Expr StringSort) = Expr IntSort+type instance IxValue (Expr StringSort) = Expr StringSort++instance Ixed (Expr StringSort) where+  ix i f s = f (strAt s i) <&> \a ->+    let l = strSubstring a 0 i+        r = strSubstring a i (strLength a)+     in l <> strReplace r (strAt a i) s++instance AsEmpty (Expr StringSort) where+  _Empty = prism'+    (const mempty)+    (\s -> ite @(Expr BoolSort) (s === mempty) (Just ()) Nothing)++instance Prefixed (Expr StringSort) where+  prefixed p = prism'+    (p <>)+    (\s -> ite (p `strPrefixOf` s) (Just $ strReplace s p mempty) Nothing)++instance Suffixed (Expr StringSort) where+  suffixed qs = prism'+    (<> qs)+    (\s -> ite (qs `strSuffixOf` s) (Just $ strSubstring s 0 (strLength s - strLength qs)) Nothing)++instance Cons (Expr StringSort) (Expr StringSort) (Expr StringSort) (Expr StringSort) where+  _Cons = prism'+    (uncurry (<>))+    (\s -> ite @(Expr BoolSort) (strLength s >? 0) (Just (strAt s 0, strSubstring s 1 (strLength s))) Nothing)++instance Snoc (Expr StringSort) (Expr StringSort) (Expr StringSort) (Expr StringSort) where+  _Snoc = prism'+    (uncurry (<>))+    (\s -> ite @(Expr BoolSort) (strLength s >? 0) (Just (strSubstring s 0 (strLength s - 1), strAt s (strLength s - 1))) Nothing)++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+  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.+instance Uniplate1 Expr '[KnownSMTSort] where+  uniplate1 _ expr@(Var _)            = pure expr+  uniplate1 _ expr@(Constant _)       = pure expr+  uniplate1 f (Plus x y)              = Plus <$> 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+  uniplate1 f (Mod x y)               = Mod <$> 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+  uniplate1 f (LTHE x y)              = LTHE <$> f x <*> f y+  uniplate1 f (EQU xs)                = EQU <$> traverse f xs+  uniplate1 f (Distinct xs)           = Distinct <$> traverse f xs+  uniplate1 f (GTHE x y)              = GTHE <$> f x <*> f y+  uniplate1 f (GTH x y)               = GTH <$> f x <*> f y+  uniplate1 f (Not x)                 = Not <$> f x+  uniplate1 f (And x y)               = And <$> f x <*> f y+  uniplate1 f (Or x y)                = Or <$> f x <*> f y+  uniplate1 f (Impl x y)              = Impl <$> f x <*> f y+  uniplate1 f (Xor x y)               = Xor <$> f x <*> f y+  uniplate1 _ Pi                      = pure Pi+  uniplate1 f (Sqrt x)                = Sqrt <$> f x+  uniplate1 f (Exp x)                 = Exp <$> f x+  uniplate1 f (Sin x)                 = Sin <$> f x+  uniplate1 f (Cos x)                 = Cos <$> f x+  uniplate1 f (Tan x)                 = Tan <$> f x+  uniplate1 f (Asin x)                = Asin <$> f x+  uniplate1 f (Acos x)                = Acos <$> f x+  uniplate1 f (Atan x)                = Atan <$> f x+  uniplate1 f (ToReal x)              = ToReal <$> f x+  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+  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+  uniplate1 f (StrSuffixOf x y)       = StrSuffixOf <$> f x <*> f y+  uniplate1 f (StrContains x y)       = StrContains <$> f x <*> f y+  uniplate1 f (StrIndexOf x y i)      = StrIndexOf <$> f x <*> f y <*> f i+  uniplate1 f (StrReplace x y y')     = StrReplace <$> f x <*> f y <*> f y'+  uniplate1 f (StrReplaceAll x y y')  = StrReplaceAll <$> f x <*> f y <*> f y'+  uniplate1 f (ForAll (Just qv) expr) = ForAll (Just qv) . const <$> f (expr (Var qv))+  uniplate1 _ (ForAll Nothing expr)   = pure $ ForAll Nothing expr+  uniplate1 f (Exists (Just qv) expr) = Exists (Just qv) . const <$> f (expr (Var qv))+  uniplate1 _ (Exists Nothing expr)   = pure $ Exists Nothing expr++-- | __Caution for quantified expressions:__ 'plate' will only be applied if quantification has taken place already.+instance KnownSMTSort t => Plated (Expr t) where+  plate f = uniplate1 (tryPlate f)+    where+      tryPlate :: forall s f. (KnownSMTSort s, Applicative f) => (Expr s -> f (Expr s)) -> (forall r. KnownSMTSort r => Expr r -> f (Expr r))+      tryPlate f' expr = case geq (sortSing @s) (sortSing' expr) of+        Just Refl -> f' expr+        Nothing   -> case expr of+          Var _                -> pure expr+          Constant _           -> pure expr+          Plus x y             -> Plus <$> 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+          Mod 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+          LTHE x y             -> LTHE <$> tryPlate f' x <*> tryPlate f' y+          EQU xs               -> EQU  <$> traverse (tryPlate f') xs+          Distinct xs          -> Distinct <$> traverse (tryPlate f') xs+          GTHE x y             -> GTHE <$> tryPlate f' x <*> tryPlate f' y+          GTH x y              -> GTH  <$> tryPlate f' x <*> tryPlate f' y+          Not x                -> Not  <$> tryPlate f' x+          And x y              -> And  <$> tryPlate f' x <*> tryPlate f' y+          Or x y               -> Or   <$> tryPlate f' x <*> tryPlate f' y+          Impl x y             -> Impl <$> tryPlate f' x <*> tryPlate f' y+          Xor x y              -> Xor  <$> tryPlate f' x <*> tryPlate f' y+          Pi                   -> pure Pi+          Sqrt x               -> Sqrt <$> tryPlate f' x+          Exp x                -> Exp  <$> tryPlate f' x+          Sin x                -> Sin  <$> tryPlate f' x+          Cos x                -> Cos  <$> tryPlate f' x+          Tan x                -> Tan  <$> tryPlate f' x+          Asin x               -> Asin <$> tryPlate f' x+          Acos x               -> Acos <$> tryPlate f' x+          Atan x               -> Atan <$> tryPlate f' x+          ToReal x             -> ToReal <$> tryPlate f' x+          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+          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+          StrSuffixOf x y      -> StrSuffixOf   <$> tryPlate f' x <*> tryPlate f' y+          StrContains x y      -> StrContains   <$> tryPlate f' x <*> tryPlate f' y+          StrIndexOf x y i     -> StrIndexOf    <$> tryPlate f' x <*> tryPlate f' y <*> tryPlate f' i+          StrReplace x y y'    -> StrReplace    <$> tryPlate f' x <*> tryPlate f' y <*> tryPlate f' y'+          StrReplaceAll x y y' -> StrReplaceAll <$> tryPlate f' x <*> tryPlate f' y <*> tryPlate f' y'+          ForAll (Just qv) qexpr -> ForAll (Just qv) . const <$> tryPlate f' (qexpr (Var qv))+          ForAll Nothing qexpr   -> pure $ ForAll Nothing qexpr+          Exists (Just qv) qexpr -> Exists (Just qv) . const <$> tryPlate f' (qexpr (Var qv))+          Exists Nothing qexpr   -> pure $ Exists Nothing qexpr++instance GNFData Expr where+  grnf expr = case expr of+    Var (SMTVar vId)     -> vId `seq` ()+    Constant c           -> c `seq` ()+    Plus e1 e2           -> grnf e1 `seq` grnf e2+    Neg e                -> grnf e+    Mul e1 e2            -> grnf e1 `seq` grnf e2+    Abs e                -> grnf e+    Mod 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+    LTHE e1 e2           -> grnf e1 `seq` grnf e2+    EQU vec              -> vec `seq` V.foldl' (const grnf) () vec+    Distinct vec         -> vec `seq` V.foldl' (const grnf) () vec+    GTHE e1 e2           -> grnf e1 `seq` grnf e2+    GTH e1 e2            -> grnf e1 `seq` grnf e2+    Not e                -> grnf e+    And e1 e2            -> grnf e1 `seq` grnf e2+    Or e1 e2             -> grnf e1 `seq` grnf e2+    Impl e1 e2           -> grnf e1 `seq` grnf e2+    Xor e1 e2            -> grnf e1 `seq` grnf e2+    Pi                   -> ()+    Sqrt e               -> grnf e+    Exp e                -> grnf e+    Sin e                -> grnf e+    Cos e                -> grnf e+    Tan e                -> grnf e+    Asin e               -> grnf e+    Acos e               -> grnf e+    Atan e               -> grnf e+    ToReal e             -> grnf e+    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+    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+    StrSuffixOf e1 e2    -> grnf e1 `seq` grnf e2+    StrContains e1 e2    -> grnf e1 `seq` grnf e2+    StrIndexOf e1 e2 e3  -> grnf e1 `seq` grnf e2 `seq` grnf e3+    StrReplace e1 e2 e3  -> grnf e1 `seq` grnf e2 `seq` grnf e3+    StrReplaceAll e1 e2 e3 -> grnf e1 `seq` grnf e2 `seq` grnf e3+    ForAll Nothing _     -> ()+    ForAll (Just qv) f   -> grnf $ f $ Var qv+    Exists Nothing _     -> ()+    Exists (Just qv) f   -> grnf $ f $ Var qv

@@ -1,11 +1,14 @@+{-# LANGUAGE LambdaCase #-}+ module Language.Hasmtlib.Type.MonadSMT where -import Language.Hasmtlib.Internal.Expr+import Language.Hasmtlib.Type.Expr import Language.Hasmtlib.Type.Option import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Solution import Language.Hasmtlib.Codec import Data.Proxy+import Control.Lens import Control.Monad import Control.Monad.State @@ -87,26 +90,22 @@  --   We need this separate so we get a pure API for quantifiers --   Ideally we would do that when rendering the expression---   However renderSMTLib2 is pure but we need a new quantified var which is stateful+--   However Language.Hasmtlib.Internal.Render#render is pure but we need a new quantified var which is stateful -- | Assign quantified variables to all quantified subexpressions of an expression. --   This shall only be used internally. --   Usually before rendering an assert.-quantify :: MonadSMT s m => Expr t -> m (Expr t)-quantify (Not x)      = fmap   Not  (quantify x)-quantify (And x y)    = liftM2 And  (quantify x) (quantify y)-quantify (Or x y)     = liftM2 Or   (quantify x) (quantify y)-quantify (Impl x y)   = liftM2 Impl (quantify x) (quantify y)-quantify (Xor x y)    = liftM2 Xor  (quantify x) (quantify y)-quantify (Ite p t f)  = liftM3 Ite  (quantify p) (quantify t) (quantify f)-quantify (ForAll _ f) = do-  qVar <- smtvar-  qBody <- quantify $ f $ Var qVar-  return $ ForAll (Just qVar) (const qBody)-quantify (Exists _ f) = do-  qVar <- smtvar-  qBody <- quantify $ f $ Var qVar-  return $ Exists (Just qVar) (const qBody)-quantify expr = return expr+quantify :: MonadSMT s m => KnownSMTSort t => Expr t -> m (Expr t)+quantify = transformM (+  \case (ForAll _ f) -> do+          qVar <- smtvar+          qBody <- quantify $ f $ Var qVar+          return $ ForAll (Just qVar) (const qBody)+        (Exists _ f) -> do+          qVar <- smtvar+          qBody <- quantify $ f $ Var qVar+          return $ Exists (Just qVar) (const qBody)+        expr -> return expr+  )  -- | A 'MonadSMT' that allows incremental solving. class MonadSMT s m => MonadIncrSMT s m where

@@ -4,11 +4,12 @@  module Language.Hasmtlib.Type.OMT where -import Language.Hasmtlib.Internal.Expr+import Language.Hasmtlib.Internal.Sharing import Language.Hasmtlib.Internal.Render import Language.Hasmtlib.Type.MonadSMT import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Option+import Language.Hasmtlib.Type.Expr import Language.Hasmtlib.Type.SMT import Data.List (isPrefixOf) import Data.Default@@ -44,6 +45,11 @@ instance Default OMT where   def = OMT def mempty mempty mempty +instance Sharing OMT where+  type SharingMonad OMT = Monad+  stableMap = smt.Language.Hasmtlib.Type.SMT.stableMap+  assertSharedNode _ expr = modifying (smt.formulas) (|> expr)+ instance MonadState OMT m => MonadSMT OMT m where   smtvar' _ = fmap coerce $ (smt.lastVarId) <+= 1   {-# INLINE smtvar' #-}@@ -56,9 +62,10 @@    assert expr = do     omt <- get+    sExpr <- runSharing expr     qExpr <- case omt^.smt.mlogic of-      Nothing    -> return expr-      Just logic -> if "QF" `isPrefixOf` logic then return expr else quantify expr+      Nothing    -> return sExpr+      Just logic -> if "QF" `isPrefixOf` logic then return sExpr else quantify sExpr     modify $ \s -> s & (smt.formulas) %~ (|> qExpr)   {-# INLINE assert #-} @@ -70,9 +77,15 @@   setLogic l = smt.mlogic ?= l  instance MonadSMT OMT m => MonadOMT OMT m where-  minimize expr = targetMinimize %= (|> SomeSMTSort (Minimize expr))-  maximize expr = targetMaximize %= (|> SomeSMTSort (Maximize expr))-  assertSoft expr w gid = softFormulas %= (|> SoftFormula expr w gid)+  minimize expr = do+    sExpr <- runSharing expr+    modifying targetMinimize (|> SomeSMTSort (Minimize sExpr))+  maximize expr = do+    sExpr <- runSharing expr+    modifying targetMaximize (|> SomeSMTSort (Maximize sExpr))+  assertSoft expr w gid = do+    sExpr <- runSharing expr+    modifying softFormulas (|> SoftFormula sExpr w gid)  instance Render SoftFormula where   render sf = "(assert-soft " <> render (sf^.formula) <> " :weight " <> maybe "1" render (sf^.mWeight) <> renderGroupId (sf^.mGroupId) <> ")"

@@ -1,20 +1,24 @@ {-# LANGUAGE TemplateHaskell #-} {-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE LambdaCase #-}  module Language.Hasmtlib.Type.Pipe where +import Language.Hasmtlib.Internal.Sharing+import Language.Hasmtlib.Internal.Render+import Language.Hasmtlib.Type.Expr import Language.Hasmtlib.Type.SMT import Language.Hasmtlib.Type.OMT (SoftFormula(..), Minimize(..), Maximize(..)) import Language.Hasmtlib.Type.MonadSMT-import Language.Hasmtlib.Internal.Expr-import Language.Hasmtlib.Internal.Render import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Solution import Language.Hasmtlib.Codec import Language.Hasmtlib.Internal.Parser hiding (var, constant) import qualified SMTLIB.Backends as B+import Data.HashMap.Lazy+import Data.Sequence hiding ((|>), (:>)) import Data.List (isPrefixOf)-import Data.IntMap as IMap (singleton)+import Data.IntMap as IntMap (singleton) import Data.Dependent.Map as DMap import Data.Coerce import qualified Data.ByteString.Lazy.Char8 as ByteString.Char8@@ -24,20 +28,32 @@ import Control.Monad.State import Control.Monad import Control.Lens hiding (List)+import System.Mem.StableName  -- | A pipe to the solver. --   If 'B.Solver' is 'B.Queuing' then all commands that do not expect an answer are sent to the queue. --   All commands that expect an answer have the queue to be sent to the solver before sending the command itself. --   If 'B.Solver' is not 'B.Queuing', all commands are sent to the solver immediately. data Pipe = Pipe-  { _lastPipeVarId :: {-# UNPACK #-} !Int              -- ^ Last Id assigned to a new var-  , _mPipeLogic    :: Maybe String                     -- ^ Logic for the SMT-Solver-  , _pipe          :: !B.Solver                        -- ^ Active pipe to the backend-  , _isDebugging   :: Bool                             -- ^ Flag if pipe shall debug+  { _lastPipeVarId     :: {-# UNPACK #-} !Int                                 -- ^ Last Id assigned to a new var+  , _mPipeLogic        :: Maybe String                                        -- ^ Logic for the SMT-Solver+  , _pipeStableMap     :: !(HashMap (StableName ()) (SomeKnownSMTSort Expr))  -- ^ Mapping between a 'StableName' and it's 'Expr' we may share+  , _incrSharedAuxs    :: !(Seq (Seq (StableName ())))                        -- ^ Index of each 'Seq' ('StableName' ()) is incremental stack height where 'StableName' representing auxiliary var that has been shared+  , _pipe              :: !B.Solver                                           -- ^ Active pipe to the backend+  , _isDebugging       :: !Bool                                               -- ^ Flag if pipe shall debug   }- $(makeLenses ''Pipe) +instance Sharing Pipe where+  type SharingMonad Pipe = MonadIO+  stableMap = pipeStableMap+  assertSharedNode sn expr = do+    smt <- get+    modifying (incrSharedAuxs._last) (|> sn)+    let cmd = renderAssert expr+    when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd+    liftIO $ B.command_ (smt^.pipe) cmd+ instance (MonadState Pipe m, MonadIO m) => MonadSMT Pipe m where   smtvar' _ = fmap coerce $ lastPipeVarId <+= 1   {-# INLINE smtvar' #-}@@ -53,9 +69,10 @@    assert expr = do     smt <- get+    sExpr <- runSharing expr     qExpr <- case smt^.mPipeLogic of-      Nothing    -> return expr-      Just logic -> if "QF" `isPrefixOf` logic then return expr else quantify expr+      Nothing    -> return sExpr+      Just logic -> if "QF" `isPrefixOf` logic then return sExpr else quantify sExpr     let cmd = renderAssert qExpr     when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd     liftIO $ B.command_ (smt^.pipe) cmd@@ -80,14 +97,15 @@     let cmd = "(push 1)"     when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd     liftIO $ B.command_ (smt^.pipe) cmd-  {-# INLINE push #-}+    incrSharedAuxs <>= mempty    pop = do     smt <- get     let cmd = "(pop 1)"     when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd     liftIO $ B.command_ (smt^.pipe) cmd-  {-# INLINE pop #-}+    forMOf_ (incrSharedAuxs._last.folded) smt (\sn -> pipeStableMap.at sn .= Nothing)+    modifying incrSharedAuxs $ \case (auxs:>_) -> auxs ; auxs -> auxs    checkSat = do     smt <- get@@ -129,31 +147,33 @@           decode             (DMap.singleton               (sortSing @t)-              (IntValueMap $ IMap.singleton (sol^.solVar.varId) (sol^.solVal)))+              (IntValueMap $ IntMap.singleton (sol^.solVar.varId) (sol^.solVal)))             v   getValue expr = do     model <- getModel     return $ decode model expr-  {-# INLINEABLE getValue #-}  instance (MonadSMT Pipe m, MonadIO m) => MonadOMT Pipe m where   minimize expr = do     smt <- get-    let cmd = render $ Minimize expr+    sExpr <- runSharing expr+    let cmd = render $ Minimize sExpr     when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd     liftIO $ B.command_ (smt^.pipe) cmd   {-# INLINEABLE minimize #-}    maximize expr = do     smt <- get-    let cmd = render $ Maximize expr+    sExpr <- runSharing expr+    let cmd = render $ Maximize sExpr     when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd     liftIO $ B.command_ (smt^.pipe) cmd   {-# INLINEABLE maximize #-}    assertSoft expr w gid = do     smt <- get-    let cmd = render $ SoftFormula expr w gid+    sExpr <- runSharing expr+    let cmd = render $ SoftFormula sExpr w gid     when (smt^.isDebugging) $ liftIO $ ByteString.Char8.putStrLn $ toLazyByteString cmd     liftIO $ B.command_ (smt^.pipe) cmd   {-# INLINEABLE assertSoft #-}

@@ -3,33 +3,42 @@  module Language.Hasmtlib.Type.SMT where -import Language.Hasmtlib.Internal.Expr+import Language.Hasmtlib.Internal.Sharing import Language.Hasmtlib.Internal.Render import Language.Hasmtlib.Type.MonadSMT import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Option+import Language.Hasmtlib.Type.Expr import Data.List (isPrefixOf) import Data.Default import Data.Coerce import Data.Sequence hiding ((|>), filter) import Data.Data (toConstr, showConstr) import Data.ByteString.Builder+import Data.HashMap.Lazy (HashMap) import Control.Monad.State import Control.Lens hiding (List)+import System.Mem.StableName  -- | The state of the SMT-problem. data SMT = SMT-  { _lastVarId :: {-# UNPACK #-} !Int                     -- ^ Last Id assigned to a new var-  , _vars     :: !(Seq (SomeKnownSMTSort SMTVar))         -- ^ All constructed variables-  , _formulas :: !(Seq (Expr BoolSort))                   -- ^ All asserted formulas-  , _mlogic   :: Maybe String                             -- ^ Logic for the SMT-Solver-  , _options  :: [SMTOption]                              -- ^ All manually configured SMT-Solver-Options+  { _lastVarId :: {-# UNPACK #-} !Int                                 -- ^ Last Id assigned to a new var+  , _vars      :: !(Seq (SomeKnownSMTSort SMTVar))                    -- ^ All constructed variables+  , _formulas  :: !(Seq (Expr BoolSort))                              -- ^ All asserted formulas+  , _mlogic    :: Maybe String                                        -- ^ Logic for the SMT-Solver+  , _options   :: [SMTOption]                                         -- ^ All manually configured SMT-Solver-Options+  , _stableMap :: !(HashMap (StableName ()) (SomeKnownSMTSort Expr))  -- ^ Mapping between a 'StableName' and it's 'Expr' we may share   } $(makeLenses ''SMT)  instance Default SMT where-  def = SMT 0 mempty mempty mempty [ProduceModels True]+  def = SMT 0 mempty mempty mempty [ProduceModels True] mempty +instance Sharing SMT where+  type SharingMonad SMT = Monad+  stableMap = Language.Hasmtlib.Type.SMT.stableMap+  assertSharedNode _ expr = modifying formulas (|> expr)+ instance MonadState SMT m => MonadSMT SMT m where   smtvar' _ = fmap coerce $ lastVarId <+= 1   {-# INLINE smtvar' #-}@@ -42,9 +51,10 @@    assert expr = do     smt <- get+    sExpr <- runSharing expr     qExpr <- case smt^.mlogic of-      Nothing    -> return expr-      Just logic -> if "QF" `isPrefixOf` logic then return expr else quantify expr+      Nothing    -> return sExpr+      Just logic -> if "QF" `isPrefixOf` logic then return sExpr else quantify sExpr     modify $ \s -> s & formulas %~ (|> qExpr)   {-# INLINE assert #-} 

@@ -1,8 +1,10 @@ {-# LANGUAGE TypeFamilyDependencies #-} {-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE QuantifiedConstraints #-}  module Language.Hasmtlib.Type.SMTSort where +import Language.Hasmtlib.Internal.Constraint import Language.Hasmtlib.Internal.Bitvec import Language.Hasmtlib.Internal.Render import Language.Hasmtlib.Type.ArrayMap@@ -38,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)) => Proxy k -> Proxy v -> SSMTSort (ArraySort k v)+  SArraySort  :: (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Eq (HaskellType v)) => Proxy k -> Proxy v -> SSMTSort (ArraySort k v)   SStringSort :: SSMTSort StringSort  deriving instance Show (SSMTSort t)@@ -93,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)) => KnownSMTSort (ArraySort k v) where+instance (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k), Eq (HaskellType v)) => KnownSMTSort (ArraySort k v) where    sortSing = SArraySort (Proxy @k) (Proxy @v) instance KnownSMTSort StringSort                 where sortSing = SStringSort @@ -101,20 +103,11 @@ sortSing' :: forall prxy t. KnownSMTSort t => prxy t -> SSMTSort t sortSing' _ = sortSing @t --- | AllC ensures that a list of constraints is applied to a poly-kinded 'Type' k------ @--- AllC '[]       k = ()--- AllC (c ': cs) k = (c k, AllC cs k)--- @-type AllC :: [k -> Constraint] -> k -> Constraint-type family AllC cs k :: Constraint where-  AllC '[]       k = ()-  AllC (c ': cs) k = (c k, AllC cs k)- -- | An existential wrapper that hides some 'SMTSort' and a list of 'Constraint's holding for it. data SomeSMTSort cs f where   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)  instance Render (SSMTSort t) where   render SBoolSort   = "Bool"

@@ -5,7 +5,7 @@  module Language.Hasmtlib.Type.Solution where -import Language.Hasmtlib.Internal.Expr+import Language.Hasmtlib.Type.Expr import Language.Hasmtlib.Type.SMTSort import Data.IntMap as IMap hiding (foldl) import Data.Dependent.Map as DMap

@@ -8,11 +8,10 @@ where  import Language.Hasmtlib.Type.MonadSMT-import Language.Hasmtlib.Internal.Expr+import Language.Hasmtlib.Type.Expr import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Solution import Language.Hasmtlib.Type.Pipe-import Language.Hasmtlib.Orderable import Language.Hasmtlib.Codec import qualified SMTLIB.Backends as Backend import qualified SMTLIB.Backends.Process as Process@@ -25,7 +24,7 @@   withSolver :: Backend.Solver -> Bool -> a  instance WithSolver Pipe where-  withSolver = Pipe 0 Nothing+  withSolver = Pipe 0 Nothing mempty mempty  -- | @'solveWith' solver prob@ solves a SMT problem @prob@ with the given -- @solver@. It returns a pair consisting of:

@@ -2,7 +2,7 @@  module Language.Hasmtlib.Variable where -import Language.Hasmtlib.Internal.Expr+import Language.Hasmtlib.Type.Expr import Language.Hasmtlib.Type.MonadSMT import Language.Hasmtlib.Type.SMTSort import Data.Proxy