Skip to content

Commit

Permalink
Merge pull request #68 from bruderj15/66-strings
Browse files Browse the repository at this point in the history
66 strings
  • Loading branch information
bruderj15 authored Aug 12, 2024
2 parents a22ee40 + ae6d407 commit 4f69a75
Show file tree
Hide file tree
Showing 13 changed files with 474 additions and 173 deletions.
10 changes: 10 additions & 0 deletions CHANGELOG.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
10 changes: 8 additions & 2 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -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))
Expand Down
5 changes: 3 additions & 2 deletions hasmtlib.cabal
Original file line number Diff line number Diff line change
@@ -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.
Expand All @@ -14,7 +14,7 @@ license-file: LICENSE
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
Expand All @@ -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
Expand Down
2 changes: 2 additions & 0 deletions src/Language/Hasmtlib.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
21 changes: 20 additions & 1 deletion src/Language/Hasmtlib/Codec.hs
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
{-# LANGUAGE DefaultSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ViewPatterns #-}

module Language.Hasmtlib.Codec where

Expand All @@ -19,6 +20,7 @@ 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
Expand Down Expand Up @@ -132,9 +134,26 @@ 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 () where type Decoded () = ()
Expand Down
26 changes: 26 additions & 0 deletions src/Language/Hasmtlib/Example/String.hs
Original file line number Diff line number Diff line change
@@ -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
152 changes: 67 additions & 85 deletions src/Language/Hasmtlib/Internal/Expr.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 #-}
Expand All @@ -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
Expand Down Expand Up @@ -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

Expand All @@ -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
Loading

0 comments on commit 4f69a75

Please sign in to comment.