Merge pull request #69 from bruderj15/develop

Develop

CHANGELOG.md

@@ -6,6 +6,16 @@ file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [PVP versioning](https://pvp.haskell.org/).
 
+## v2.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

README.md

@@ -59,12 +59,18 @@ May print: `(Sat,Just (V3 (-2.0) (-1.0) 0.0,V3 (-2.0) (-1.0) 0.0))`
 
 - [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))

hasmtlib.cabal

@@ -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 @@ license-file:          LICENSE
 author:                Julian Bruder
 maintainer:            [email protected]
 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 @@ library
   default-extensions:  DataKinds, GADTs, TypeFamilies, OverloadedStrings
 
   exposed-modules:     Language.Hasmtlib
+                     , Language.Hasmtlib.Lens
                      , Language.Hasmtlib.Codec
                      , Language.Hasmtlib.Iteable
                      , Language.Hasmtlib.Boolean

src/Language/Hasmtlib.hs

@@ -10,6 +10,7 @@ module Language.Hasmtlib
   , 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.Option
 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

src/Language/Hasmtlib/Codec.hs

@@ -1,6 +1,7 @@
 {-# LANGUAGE DefaultSignatures #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ViewPatterns #-}
 
 module Language.Hasmtlib.Codec where
 
@@ -19,11 +20,13 @@ import Data.Sequence (Seq)
 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 @@ type family DefaultDecoded a :: Type where
   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 @@ instance KnownSMTSort t => Codec (Expr t) where
   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)

src/Language/Hasmtlib/Example/String.hs

@@ -0,0 +1,26 @@
+module Language.Hasmtlib.Example.Arith where
+
+import Prelude hiding ((&&))
+import Language.Hasmtlib
+import Control.Lens
+
+main :: IO ()
+main = do
+  res <- solveWith @SMT (solver cvc5) $ do
+    setLogic "QF_S"
+
+    x <- var @StringSort
+    y <- var @StringSort
+    z <- var @StringSort
+
+    assert $ x === "H" <> "e" <> "llo"
+    assert $ y === "World"
+    assert $ z === x <> " " <> y
+
+    p <- var @StringSort
+    let argh :: Expr StringSort = "Argh!"
+    assert $ p === "_Cons: " <| z <> argh^.ix 4
+
+    return p
+
+  print res

src/Language/Hasmtlib/Internal/Expr.hs

@@ -9,51 +9,59 @@ import Language.Hasmtlib.Type.ArrayMap
 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 @@ data Expr (t :: SMTSort) where
   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 @@ 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 #-}
@@ -176,6 +207,7 @@ instance Render (Value t) 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
@@ -243,6 +275,19 @@ instance KnownSMTSort t => Render (Expr t) where
   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 qname (Just qvar) f =
 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
-
-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)))) ++ ")"
+  show = toString . toLazyByteString . render
+
+instance KnownSMTSort t => Show (Expr t) where
+  show = toString . toLazyByteString . render