hasmtlib 2.2.0 → 2.3.0

raw patch · 12 files changed

+456/−175 lines, 12 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +10/−0
• README.md +8/−2
• hasmtlib.cabal +3/−2
• src/Language/Hasmtlib.hs +2/−0
• src/Language/Hasmtlib/Codec.hs +29/−4
• src/Language/Hasmtlib/Internal/Expr.hs +66/−84
• src/Language/Hasmtlib/Internal/Parser.hs +39/−77
• src/Language/Hasmtlib/Internal/Render.hs +6/−0
• src/Language/Hasmtlib/Lens.hs +211/−0
• src/Language/Hasmtlib/Orderable.hs +7/−0
• src/Language/Hasmtlib/Type/Expr.hs +55/−1
• src/Language/Hasmtlib/Type/SMTSort.hs +20/−5

@@ -6,6 +6,16 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [PVP versioning](https://pvp.haskell.org/). +## v2.3.0 _(2024-08-12)_++### Added+- Added full SMTLib2.6-standard support for sort String+- Added module `Language.Hasmtlib.Lens` featuring `instance Plated (Expr t)` for rewriting++### Changed+- Export constructors of `Expr t`+- `instance Show (Expr t)` now displays expressions in SMTLib2-Syntax+ ## v2.2.0 _(2024-08-09)_  ### Added

@@ -59,12 +59,18 @@  - [x] SMTLib2-Sorts in the Haskell-Type   ```haskell-    data SMTSort = BoolSort | IntSort | RealSort | BvSort Nat | ArraySort SMTSort SMTSort+    data SMTSort =+        BoolSort+      | IntSort+      | RealSort+      | BvSort Nat+      | ArraySort SMTSort SMTSort+      | StringSort     data Expr (t :: SMTSort) where ...      ite :: Expr BoolSort -> Expr t -> Expr t -> Expr t   ```-- [x] Full SMTLib 2.6 standard support for Sorts Int, Real, Bool, unsigned BitVec & Array+- [x] Full SMTLib 2.6 standard support for Sorts Int, Real, Bool, unsigned BitVec, Array & String - [x] Type-level length-indexed Bitvectors for BitVec   ```haskell     bvConcat :: (KnownNat n, KnownNat m) => Expr (BvSort n) -> Expr (BvSort m) -> Expr (BvSort (n + m))

@@ -1,7 +1,7 @@ cabal-version:         3.0  name:                  hasmtlib-version:               2.2.0+version:               2.3.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.@@ -14,7 +14,7 @@ author:                Julian Bruder maintainer:            julian.bruder@outlook.com copyright:             © 2024 Julian Bruder-category:              SMT+category:              SMT, Logic build-type:            Simple extra-source-files:    README.md extra-doc-files:       CHANGELOG.md@@ -26,6 +26,7 @@   default-extensions:  DataKinds, GADTs, TypeFamilies, OverloadedStrings    exposed-modules:     Language.Hasmtlib+                     , Language.Hasmtlib.Lens                      , Language.Hasmtlib.Codec                      , Language.Hasmtlib.Iteable                      , Language.Hasmtlib.Boolean

@@ -10,6 +10,7 @@   , 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@@ -38,6 +39,7 @@ 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

@@ -1,6 +1,7 @@ {-# LANGUAGE DefaultSignatures #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ViewPatterns #-}  module Language.Hasmtlib.Codec where @@ -19,11 +20,13 @@ import Data.IntMap as IM hiding (foldl) import Data.Dependent.Map as DMap import Data.Tree (Tree)+import qualified Data.Text as Text import Data.Monoid (Sum, Product, First, Last, Dual) import Data.Functor.Identity (Identity) import qualified Data.Vector.Sized as V import Control.Monad import GHC.Generics+import GHC.TypeLits  -- | Computes a default 'Decoded' 'Type' by distributing 'Decoded' to it's type arguments. type family DefaultDecoded a :: Type where@@ -35,13 +38,18 @@   DefaultDecoded (t a b c) = t (Decoded a) (Decoded b) (Decoded c)   DefaultDecoded (t a b) = t (Decoded a) (Decoded b)   DefaultDecoded (t a) = t (Decoded a)-  DefaultDecoded () = ()+  DefaultDecoded x = TypeError (+          Text "DefaultDecoded (" :<>: ShowType x :<>: Text ") is not allowed."+    :$$:  Text "Try providing the associated Type Decoded (" :<>: ShowType x :<>: Text ") manually:"+    :$$:  Text "instance Codec (" :<>: ShowType x :<>: Text ") where "+    :$$:  Text "   type Decoded (" :<>: ShowType x :<>: Text ") = ... "+    )  -- | Lift values to SMT-Values or decode them. -- --   You can derive an instance of this class if your type is 'Generic'. class Codec a where-  -- | Resulting of decoding @a@+  -- | Result of decoding @a@.   type Decoded a :: Type   type Decoded a = DefaultDecoded a @@ -126,12 +134,29 @@   decode sol (BvuGT x y)        = liftA2 (>) (decode sol x) (decode sol y)   decode sol (ArrSelect i arr)  = liftA2 arrSelect (decode sol i) (decode sol arr)   decode sol (ArrStore i x arr) = liftM3 arrStore (decode sol i) (decode sol x) (decode sol arr)+  decode sol (StrConcat x y)         = liftM2 (<>) (decode sol x) (decode sol y)+  decode sol (StrLength x)           = toInteger . Text.length <$> decode sol x+  decode sol (StrLT x y)             = liftM2 (<) (decode sol x) (decode sol y)+  decode sol (StrLTHE x y)           = liftM2 (<=) (decode sol x) (decode sol y)+  decode sol (StrAt x i)             = liftM2 (\x' i' -> Text.singleton $ Text.index x' (fromInteger i')) (decode sol x) (decode sol i)+  decode sol (StrSubstring x i j)    = liftM3 (\x' (fromInteger -> i') (fromInteger -> j') -> Text.take (j' - i') $ Text.drop i' x') (decode sol x) (decode sol i) (decode sol j)+  decode sol (StrPrefixOf x y)       = liftM2 Text.isPrefixOf (decode sol x) (decode sol y)+  decode sol (StrSuffixOf x y)       = liftM2 Text.isSuffixOf (decode sol x) (decode sol y)+  decode sol (StrContains x y)       = liftM2 (flip Text.isInfixOf) (decode sol x) (decode sol y)+  decode sol (StrIndexOf x y i)      = join $ liftM3 (\x' y' (fromInteger -> i') -> Text.findIndex ((y' ==) . Text.singleton) (Text.drop i' x') >>= Just . toInteger) (decode sol x) (decode sol y) (decode sol i)+  decode sol (StrReplace src target replacement) = liftM3 (\src' target' replacement' -> replaceOne target' replacement' src') (decode sol target) (decode sol src) (decode sol replacement)+    where+      replaceOne pattern substitution text+        | Text.null back = text+        | otherwise = Text.concat [front, substitution, Text.drop (Text.length pattern) back]+          where+            (front, back) = Text.breakOn pattern text+  decode sol (StrReplaceAll src target replacement) = liftM3 (\src' target' replacement' -> Text.replace target' replacement' src') (decode sol target) (decode sol src) (decode sol replacement)   decode _ (ForAll _ _)         = Nothing   decode _ (Exists _ _)         = Nothing-   encode = Constant . wrapValue -instance Codec ()+instance Codec () where type Decoded () = () instance (Codec a, Codec b) => Codec (a,b) instance (Codec a, Codec b, Codec c) => Codec (a,b,c) instance (Codec a, Codec b, Codec c, Codec d) => Codec (a,b,c,d)

@@ -9,51 +9,59 @@ import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Boolean import Data.Map hiding (toList)-import Data.List (intercalate) import Data.Proxy import Data.Coerce-import Data.Foldable (toList)+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)+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)+  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 (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+  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 --- | A SMT expression.+-- | Am SMT expression. --   For internal use only. --   For building expressions use the corresponding instances (Num, Boolean, ...). data Expr (t :: SMTSort) where@@ -122,6 +130,19 @@   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@@ -158,6 +179,16 @@   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 #-}@@ -176,6 +207,7 @@       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@@ -243,6 +275,19 @@   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 @@ -257,70 +302,7 @@ renderQuantifier _ Nothing _ = mempty  instance Show (Value t) where-  show (IntValue x)   = "IntValue "   ++ show x-  show (RealValue x)  = "RealValue "  ++ show x-  show (BoolValue x)  = "BoolValue "  ++ show x-  show (BvValue x)    = "BvValue "    ++ show x-  show (ArrayValue x) = "ArrValue: "  ++ show (render (ArrayValue x)) -- FIXME: This is bad but easy now+  show = toString . toLazyByteString . render -instance Show (Expr t) where-  show (Var v)              = show v-  show (Constant c)         = show c-  show (Plus x y)           = "(" ++ show x ++ " + " ++ show y ++ ")"-  show (Neg x)              = "(- " ++ show x ++ ")"-  show (Mul x y)            = "(" ++ show x ++ " * " ++ show y ++ ")"-  show (Abs x)              = "(abs " ++ show x ++ ")"-  show (Mod x y)            = "(" ++ show x ++ " mod " ++ show y ++ ")"-  show (IDiv x y)           = "(" ++ show x ++ " div " ++ show y ++ ")"-  show (Div x y)            = "(" ++ show x ++ " / " ++ show y ++ ")"-  show (LTH x y)            = "(" ++ show x ++ " < " ++ show y ++ ")"-  show (LTHE x y)           = "(" ++ show x ++ " <= " ++ show y ++ ")"-  show (EQU xs)             = "(= " ++ intercalate " " (show <$> toList xs) ++ ")"-  show (Distinct xs)        = "(distinct " ++ intercalate " " (show <$> toList xs) ++ ")"-  show (GTHE x y)           = "(" ++ show x ++ " >= " ++ show y ++ ")"-  show (GTH x y)            = "(" ++ show x ++ " > " ++ show y ++ ")"-  show (Not x)              = "(not " ++ show x ++ ")"-  show (And x y)            = "(" ++ show x ++ " && " ++ show y ++ ")"-  show (Or x y)             = "(" ++ show x ++ " || " ++ show y ++ ")"-  show (Impl x y)           = "(" ++ show x ++ " ==> " ++ show y ++ ")"-  show (Xor x y)            = "(" ++ show x ++ " xor " ++ show y ++ ")"-  show Pi                   = "pi"-  show (Sqrt x)             = "(sqrt "    ++ show x ++ ")"-  show (Exp x)              = "(exp "     ++ show x ++ ")"-  show (Sin x)              = "(sin "     ++ show x ++ ")"-  show (Cos x)              = "(cos "     ++ show x ++ ")"-  show (Tan x)              = "(tan "     ++ show x ++ ")"-  show (Asin x)             = "(arcsin "  ++ show x ++ ")"-  show (Acos x)             = "(arccos "  ++ show x ++ ")"-  show (Atan x)             = "(arctan "  ++ show x ++ ")"-  show (ToReal x)           = "(to_real " ++ show x ++ ")"-  show (ToInt x)            = "(to_int "  ++ show x ++ ")"-  show (IsInt x)            = "(is_int "  ++ show x ++ ")"-  show (Ite p t f)          = "(ite " ++ show p ++ " " ++ show t ++ " " ++ show f ++ ")"-  show (BvNot x)            = "(not "  ++ show x ++ ")"-  show (BvAnd x y)          = "(" ++ show x ++ " && " ++ show y ++ ")"-  show (BvOr x y)           = "(" ++ show x ++ " || " ++ show y ++ ")"-  show (BvXor x y)          = "(" ++ show x ++ " xor " ++ show y ++ ")"-  show (BvNand x y)         = "(" ++ show x ++ " nand " ++ show y ++ ")"-  show (BvNor x y)          = "(" ++ show x ++ " nor " ++ show y ++ ")"-  show (BvNeg x)            = "(- " ++ show x ++ ")"-  show (BvAdd x y)          = "(" ++ show x ++ " + " ++ show y ++ ")"-  show (BvSub x y)          = "(" ++ show x ++ " - " ++ show y ++ ")"-  show (BvMul x y)          = "(" ++ show x ++ " * " ++ show y ++ ")"-  show (BvuDiv x y)         = "(" ++ show x ++ " udiv " ++ show y ++ ")"-  show (BvuRem x y)         = "(" ++ show x ++ " urem " ++ show y ++ ")"-  show (BvShL x y)          = "(" ++ show x ++ " bvshl " ++ show y ++ ")"-  show (BvLShR x y)         = "(" ++ show x ++ " bvlshr " ++ show y ++ ")"-  show (BvConcat x y)       = "(" ++ show x ++ " bvconcat " ++ show y ++ ")"-  show (BvRotL i x)         = "(" ++ show x ++ " bvrotl " ++ show (natVal i) ++ ")"-  show (BvRotR i x)         = "(" ++ show x ++ " bvrotr " ++ show (natVal i) ++ ")"-  show (BvuLT x y)          = "(" ++ show x ++ " bvult " ++ show y ++ ")"-  show (BvuLTHE x y)        = "(" ++ show x ++ " bvule " ++ show y ++ ")"-  show (BvuGTHE x y)        = "(" ++ show x ++ " bvuge " ++ show y ++ ")"-  show (BvuGT x y)          = "(" ++ show x ++ " bvugt " ++ show y ++ ")"-  show (ForAll (Just qv) f) = "(forall " ++ show qv ++ ": " ++ show (f (Var qv)) ++ ")"-  show (ForAll Nothing f)   = "(forall var_-1: " ++ show (f (Var (SMTVar (-1)))) ++ ")"-  show (ArrSelect i arr)    = "(select " ++ show i ++ " " ++ show arr ++ ")"-  show (ArrStore i x arr)   = "(select " ++ show i ++ " " ++ show x ++ " " ++ show arr ++ ")"-  show (Exists (Just qv) f) = "(exists " ++ show qv ++ ": " ++ show (f (Var qv)) ++ ")"-  show (Exists Nothing f)   = "(exists var_-1: " ++ show (f (Var (SMTVar (-1)))) ++ ")"+instance KnownSMTSort t => Show (Expr t) where+  show = toString . toLazyByteString . render

@@ -16,14 +16,17 @@ import Language.Hasmtlib.Type.SMTSort import Language.Hasmtlib.Type.Solution import Language.Hasmtlib.Type.ArrayMap+import Language.Hasmtlib.Type.Expr import Data.Bit import Data.Coerce import Data.Proxy import Data.Ratio ((%)) import Data.ByteString import Data.ByteString.Builder-import Data.Attoparsec.ByteString hiding (Result, skipWhile)+import Data.Attoparsec.ByteString hiding (Result, skipWhile, takeTill) import Data.Attoparsec.ByteString.Char8 hiding (Result)+import Data.Text.Encoding (decodeUtf8)+import qualified Data.Text as Text import Control.Applicative import Control.Lens hiding (op) import GHC.TypeNats@@ -83,6 +86,7 @@         <|> (string "Real" *> pure (SomeSMTSort SRealSort))         <|> parseSomeBitVecSort         <|> parseSomeArraySort+        <|> (string "String" *> pure (SomeSMTSort SStringSort)) {-# INLINEABLE parseSomeSort #-}  parseSomeBitVecSort :: Parser (SomeKnownOrdSMTSort SSMTSort)@@ -115,19 +119,19 @@  -- TODO: Add parseSelect parseExpr :: forall t. KnownSMTSort t => Parser (Expr t)-parseExpr = var <|> constantExpr <|> smtIte+parseExpr = var <|> constantExpr <|> ternary "ite" (ite @(Expr BoolSort))         <|> case sortSing @t of               SIntSort  -> unary "abs" abs <|> unary  "-" negate                       <|> nary "+" sum  <|> binary "-" (-) <|> nary "*" product <|> binary "mod" Mod-                      <|> toIntFun+                      <|> unary "to_int" toIntSort <|> unary "str.len" strLength+                      <|> ternary "str.indexof" strIndexOf               SRealSort -> unary "abs" abs <|> unary  "-" negate                       <|> nary "+" sum  <|> binary "-" (-) <|> nary "*" product <|> binary "/" (/)-                      <|> toRealFun+                      <|> unary "to_real" toRealSort                       <|> smtPi <|> unary "sqrt" sqrt <|> unary "exp" exp                       <|> unary "sin" sin <|> unary "cos" cos <|> unary "tan" tan                       <|> unary "arcsin" asin <|> unary "arccos" acos <|> unary "arctan" atan-              SBoolSort -> isIntFun-                      <|> unary "not" not+              SBoolSort -> unary "not" not                       <|> nary "and" and  <|> nary "or" or <|> binary "=>" (==>) <|> binary "xor" xor                       <|> binary @IntSort  "=" (===) <|> binary @IntSort  "distinct" (/==)                       <|> binary @RealSort "=" (===) <|> binary @RealSort "distinct" (/==)@@ -136,6 +140,10 @@                       <|> binary @IntSort ">=" (>=?) <|> binary @IntSort ">" (>?)                       <|> binary @RealSort "<" (<?) <|> binary @RealSort "<=" (<=?)                       <|> binary @RealSort ">=" (>=?) <|> binary @RealSort ">" (>?)+                      <|> binary @StringSort "str.<" (<?) <|> binary @StringSort "str.<=" (<=?)+                      <|> unary "is_int" isIntSort+                      <|> binary "str.prefixof" strPrefixOf <|> binary "str.suffixof" strSuffixOf+                      <|> binary "str.contains" strContains                       -- TODO: Add compare ops for all (?) bv-sorts               SBvSort _ -> unary "bvnot" not                       <|> binary "bvand" (&&)  <|> binary "bvor" (||) <|> binary "bvxor" xor <|> binary "bvnand" BvNand <|> binary "bvnor" BvNor@@ -143,14 +151,15 @@                       <|> binary "bvadd" (+)  <|> binary "bvsub" (-) <|> binary "bvmul" (*)                       <|> binary "bvudiv" BvuDiv <|> binary "bvurem" BvuRem                       <|> binary "bvshl" BvShL <|> binary "bvlshr" BvLShR-              SArraySort _ _ -> parseStore+              SArraySort _ _ -> ternary "store" ArrStore                       -- TODO: Add compare ops for all (?) array-sorts+              SStringSort -> binary "str.++" (<>) <|> binary "str.at" strAt <|> ternary "str.substr" StrSubstring+                      <|> ternary "str.replace" strReplace <|> ternary "str.replace_all" strReplaceAll  var :: Parser (Expr t) var = do   _     <- string "var_"   vId <- decimal @Int-   return $ Var $ coerce vId {-# INLINE var #-} @@ -161,7 +170,8 @@   SBoolSort -> parseBool   SBvSort p -> anyBitvector p   SArraySort k v -> constArray k v-{-# INLINE constant #-}+  SStringSort -> parseSmtString+{-# INLINEABLE constant #-}  constantExpr :: forall t. KnownSMTSort t => Parser (Expr t) constantExpr = Constant . wrapValue <$> constant @t@@ -210,29 +220,12 @@   return $ asConst constVal {-# INLINEABLE constArray #-} -parseSelect :: forall k v. (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Proxy k -> Parser (Expr v)-parseSelect _ = do-  _ <- char '(' >> skipSpace-  _ <- string "select" >> skipSpace-  arr <- parseExpr @(ArraySort k v)-  _ <- skipSpace-  i <- parseExpr @k-  _ <- skipSpace >> char ')'--  return $ ArrSelect arr i--parseStore :: forall k v. (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => Parser (Expr (ArraySort k v))-parseStore = do-  _ <- char '(' >> skipSpace-  _ <- string "store" >> skipSpace-  arr <- parseExpr @(ArraySort k v)-  _ <- skipSpace-  i <- parseExpr @k-  _ <- skipSpace-  x <- parseExpr @v-  _ <- skipSpace >> char ')'--  return $ ArrStore arr i x+parseSmtString :: Parser Text.Text+parseSmtString = do+  _ <- char '"'+  s <- decodeUtf8 <$> takeTill (== '"')+  _ <- char '"'+  return s  unary :: forall t r. KnownSMTSort t => ByteString -> (Expr t -> Expr r) -> Parser (Expr r) unary opStr op = do@@ -244,7 +237,7 @@   return $ op val {-# INLINE unary #-} -binary :: forall t r. KnownSMTSort t => ByteString -> (Expr t -> Expr t -> Expr r) -> Parser (Expr r)+binary :: forall t u r. (KnownSMTSort t, KnownSMTSort u) => ByteString -> (Expr t -> Expr u -> Expr r) -> Parser (Expr r) binary opStr op = do   _ <- char '(' >> skipSpace   _ <- string opStr >> skipSpace@@ -255,6 +248,19 @@   return $ l `op` r {-# INLINE binary #-} +ternary :: forall t u v r. (KnownSMTSort t, KnownSMTSort u, KnownSMTSort v) => ByteString -> (Expr t -> Expr u -> Expr v -> Expr r) -> Parser (Expr r)+ternary opStr op = do+  _ <- char '(' >> skipSpace+  _ <- string opStr >> skipSpace+  l <- parseExpr+  _ <- skipSpace+  m <- parseExpr+  _ <- skipSpace+  r <- parseExpr+  _ <- skipSpace >> char ')'+  return $ op l m r+{-# INLINE ternary #-}+ nary :: forall t r. KnownSMTSort t => ByteString -> ([Expr t] -> Expr r) -> Parser (Expr r) nary opStr op = do   _    <- char '(' >> skipSpace@@ -267,50 +273,6 @@ smtPi :: Parser (Expr RealSort) smtPi = string "real.pi" *> return pi {-# INLINE smtPi #-}--toRealFun :: Parser (Expr RealSort)-toRealFun = do-  _ <- char '(' >> skipSpace-  _ <- string "to_real" >> skipSpace-  val <- parseExpr-  _ <- skipSpace >> char ')'--  return $ ToReal val-{-# INLINEABLE toRealFun #-}--toIntFun :: Parser (Expr IntSort)-toIntFun = do-  _ <- char '(' >> skipSpace-  _ <- string "to_int" >> skipSpace-  val <- parseExpr-  _ <- skipSpace >> char ')'--  return $ ToInt val-{-# INLINEABLE toIntFun #-}--isIntFun :: Parser (Expr BoolSort)-isIntFun = do-  _ <- char '(' >> skipSpace-  _ <- string "is_int" >> skipSpace-  val <- parseExpr-  _ <- skipSpace >> char ')'--  return $ IsInt val-{-# INLINEABLE isIntFun #-}--smtIte :: forall t. KnownSMTSort t => Parser (Expr t)-smtIte = do-  _ <- char '(' >> skipSpace-  _ <- string "ite" >> skipSpace-  p <- parseExpr @BoolSort-  _ <- skipSpace-  t <- parseExpr-  _ <- skipSpace-  f <- parseExpr-  _ <- skipSpace >> char ')'--  return $ ite p t f-{-# INLINEABLE smtIte #-}  anyValue :: Num a => Parser a -> Parser a anyValue p = negativeValue p <|> p

@@ -3,6 +3,8 @@ import Data.ByteString.Builder import Data.Foldable (foldl') import Data.Sequence+import qualified Data.Text as Text+import qualified Data.Text.Encoding as Text.Enc import GHC.TypeNats  -- | Render values to their SMTLib2-Lisp form, represented as 'Builder'.@@ -39,6 +41,10 @@  instance Render Builder where   render = id+  {-# INLINE render #-}++instance Render Text.Text where+  render = Text.Enc.encodeUtf8Builder   {-# INLINE render #-}  renderUnary :: Render a => Builder -> a -> Builder

@@ -0,0 +1,211 @@+{-# 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

@@ -85,6 +85,13 @@   (>?)     = 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

@@ -4,12 +4,13 @@ module Language.Hasmtlib.Type.Expr  ( SMTVar(..), varId  , Value(..), unwrapValue, wrapValue- , Expr+ , 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 @@ -118,3 +119,56 @@ -- | 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

@@ -10,6 +10,7 @@ import Data.Kind import Data.Proxy import Data.ByteString.Builder+import qualified Data.Text as Text import Control.Lens import GHC.TypeLits @@ -20,6 +21,7 @@   | RealSort                      -- ^ Sort of Real   | BvSort Nat                    -- ^ Sort of BitVec with length n   | ArraySort SMTSort SMTSort     -- ^ Sort of Array with indices k and values v+  | StringSort                    -- ^ Sort of String  -- | Injective type-family that computes the Haskell 'Type' of an 'SMTSort'. type family HaskellType (t :: SMTSort) = (r :: Type) | r -> t where@@ -28,14 +30,16 @@   HaskellType BoolSort        = Bool   HaskellType (BvSort n)      = Bitvec n   HaskellType (ArraySort k v) = ConstArray (HaskellType k) (HaskellType v)+  HaskellType StringSort      = Text.Text  -- | Singleton for 'SMTSort'. data SSMTSort (t :: SMTSort) where-  SIntSort   :: SSMTSort IntSort-  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)+  SIntSort    :: SSMTSort IntSort+  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)+  SStringSort :: SSMTSort StringSort  deriving instance Show (SSMTSort t) deriving instance Eq   (SSMTSort t)@@ -46,8 +50,14 @@   geq SRealSort SRealSort     = Just Refl   geq SBoolSort SBoolSort     = Just Refl   geq (SBvSort n) (SBvSort m) = case sameNat n m of+    Nothing   -> Nothing     Just Refl -> Just Refl+  geq (SArraySort k v) (SArraySort k' v') = case geq (sortSing' k) (sortSing' k') of     Nothing   -> Nothing+    Just Refl -> case geq (sortSing' v) (sortSing' v') of+      Nothing -> Nothing+      Just Refl -> Just Refl+  geq SStringSort SStringSort = Just Refl   geq _ _                     = Nothing  instance GCompare SSMTSort where@@ -65,6 +75,7 @@       GEQ -> GEQ       GGT -> GGT     GGT -> GGT+  gcompare SStringSort SStringSort = GEQ   gcompare SBoolSort _        = GLT   gcompare _ SBoolSort        = GGT   gcompare SIntSort _         = GLT@@ -73,6 +84,8 @@   gcompare _ SRealSort        = GGT   gcompare (SArraySort _ _) _ = GLT   gcompare _ (SArraySort _ _) = GGT+  gcompare SStringSort _      = GLT+  gcompare _ SStringSort      = GGT  -- | Compute singleton 'SSMTSort' from it's promoted type 'SMTSort'. class    KnownSMTSort (t :: SMTSort)           where sortSing :: SSMTSort t@@ -82,6 +95,7 @@ instance KnownNat n => KnownSMTSort (BvSort n) where sortSing = SBvSort (Proxy @n) instance (KnownSMTSort k, KnownSMTSort v, Ord (HaskellType k)) => KnownSMTSort (ArraySort k v) where    sortSing = SArraySort (Proxy @k) (Proxy @v)+instance KnownSMTSort StringSort                 where sortSing = SStringSort  -- | Wrapper for 'sortSing' which takes a 'Proxy' sortSing' :: forall prxy t. KnownSMTSort t => prxy t -> SSMTSort t@@ -108,4 +122,5 @@   render SRealSort   = "Real"   render (SBvSort p) = renderBinary "_" ("BitVec" :: Builder) (natVal p)   render (SArraySort k v) = renderBinary "Array" (sortSing' k) (sortSing' v)+  render SStringSort   = "String"   {-# INLINEABLE render #-}