Length of a string.

>>> sat $ \s -> length s .== 2
Satisfiable. Model:
  s0 = "\NUL\NUL" :: String
>>> sat $ \s -> length s .< 0
Unsatisfiable
>>> prove $ \s1 s2 -> length s1 + length s2 .== length (s1 .++ s2)
Q.E.D.

null s is True iff the string is empty

>>> prove $ \s -> null s .<=> length s .== 0
Q.E.D.
>>> prove $ \s -> null s .<=> s .== ""
Q.E.D.

head returns the head of a string. Unspecified if the string is empty.

>>> prove $ \c -> head (singleton c) .== c
Q.E.D.

tail returns the tail of a string. Unspecified if the string is empty.

>>> prove $ \h s -> tail (singleton h .++ s) .== s
Q.E.D.
>>> prove $ \s -> length s .> 0 .=> length (tail s) .== length s - 1
Q.E.D.
>>> prove $ \s -> sNot (null s) .=> singleton (head s) .++ tail s .== s
Q.E.D.

@uncons returns the pair of the first character and tail. Unspecified if the string is empty.

init returns all but the last element of the list. Unspecified if the string is empty.

>>> prove $ \c t -> init (t .++ singleton c) .== t
Q.E.D.

singleton c is the string of length 1 that contains the only character whose value is the 8-bit value c.

>>> prove $ \c -> c .== literal 'A' .=> singleton c .== "A"
Q.E.D.
>>> prove $ \c -> length (singleton c) .== 1
Q.E.D.

strToStrAt s offset. Substring of length 1 at offset in s. Unspecified if offset is out of bounds.

>>> prove $ \s1 s2 -> strToStrAt (s1 .++ s2) (length s1) .== strToStrAt s2 0
Q.E.D.
>>> sat $ \s -> length s .>= 2 .&& strToStrAt s 0 ./= strToStrAt s (length s - 1)
Satisfiable. Model:
  s0 = "\NUL\STX" :: String

strToCharAt s i is the 8-bit value stored at location i. Unspecified if index is out of bounds.

>>> prove $ \i -> i .>= 0 .&& i .<= 4 .=> "AAAAA" `strToCharAt` i .== literal 'A'
Q.E.D.
>>> prove $ \s i c -> i `inRange` (0, length s - 1) .&& s `strToCharAt` i .== c .=> indexOf s (singleton c) .<= i
Q.E.D.

Short cut for strToCharAt

implode cs is the string of length |cs| containing precisely those characters. Note that there is no corresponding function explode, since we wouldn't know the length of a symbolic string.

>>> prove $ \c1 c2 c3 -> length (implode [c1, c2, c3]) .== 3
Q.E.D.
>>> prove $ \c1 c2 c3 -> map (strToCharAt (implode [c1, c2, c3])) (map literal [0 .. 2]) .== [c1, c2, c3]
Q.E.D.

Concatenate two strings. See also .++.

Prepend an element, the traditional cons.

Append an element

Empty string. This value has the property that it's the only string with length 0:

>>> prove $ \l -> length l .== 0 .<=> l .== nil
Q.E.D.

Short cut for concat.

>>> sat $ \x y z -> length x .== 5 .&& length y .== 1 .&& x .++ y .++ z .== "Hello world!"
Satisfiable. Model:
  s0 =  "Hello" :: String
  s1 =      " " :: String
  s2 = "world!" :: String

isInfixOf sub s. Does s contain the substring sub?

>>> prove $ \s1 s2 s3 -> s2 `isInfixOf` (s1 .++ s2 .++ s3)
Q.E.D.
>>> prove $ \s1 s2 -> s1 `isInfixOf` s2 .&& s2 `isInfixOf` s1 .<=> s1 .== s2
Q.E.D.

isSuffixOf suf s. Is suf a suffix of s?

>>> prove $ \s1 s2 -> s2 `isSuffixOf` (s1 .++ s2)
Q.E.D.
>>> prove $ \s1 s2 -> s1 `isSuffixOf` s2 .=> subStr s2 (length s2 - length s1) (length s1) .== s1
Q.E.D.

isPrefixOf pre s. Is pre a prefix of s?

>>> prove $ \s1 s2 -> s1 `isPrefixOf` (s1 .++ s2)
Q.E.D.
>>> prove $ \s1 s2 -> s1 `isPrefixOf` s2 .=> subStr s2 0 (length s1) .== s1
Q.E.D.

take len s. Corresponds to Haskell's take on symbolic-strings.

>>> prove $ \s i -> i .>= 0 .=> length (take i s) .<= i
Q.E.D.

drop len s. Corresponds to Haskell's drop on symbolic-strings.

>>> prove $ \s i -> length (drop i s) .<= length s
Q.E.D.
>>> prove $ \s i -> take i s .++ drop i s .== s
Q.E.D.

subStr s offset len is the substring of s at offset offset with length len. This function is under-specified when the offset is outside the range of positions in s or len is negative or offset+len exceeds the length of s.

>>> prove $ \s i -> i .>= 0 .&& i .< length s .=> subStr s 0 i .++ subStr s i (length s - i) .== s
Q.E.D.
>>> sat  $ \i j -> subStr "hello" i j .== "ell"
Satisfiable. Model:
  s0 = 1 :: Integer
  s1 = 3 :: Integer
>>> sat  $ \i j -> subStr "hell" i j .== "no"
Unsatisfiable

replace s src dst. Replace the first occurrence of src by dst in s

>>> prove $ \s -> replace "hello" s "world" .== "world" .=> s .== "hello"
Q.E.D.
>>> prove $ \s1 s2 s3 -> length s2 .> length s1 .=> replace s1 s2 s3 .== s1
Q.E.D.

indexOf s sub. Retrieves first position of sub in s, -1 if there are no occurrences. Equivalent to offsetIndexOf s sub 0.

>>> prove $ \s i -> i .> 0 .&& i .< length s .=> indexOf s (subStr s i 1) .<= i
Q.E.D.
>>> prove $ \s1 s2 -> length s2 .> length s1 .=> indexOf s1 s2 .== -1
Q.E.D.

offsetIndexOf s sub offset. Retrieves first position of sub at or after offset in s, -1 if there are no occurrences.

>>> prove $ \s sub -> offsetIndexOf s sub 0 .== indexOf s sub
Q.E.D.
>>> prove $ \s sub i -> i .>= length s .&& length sub .> 0 .=> offsetIndexOf s sub i .== -1
Q.E.D.
>>> prove $ \s sub i -> i .> length s .=> offsetIndexOf s sub i .== -1
Q.E.D.

strToNat s. Retrieve integer encoded by string s (ground rewriting only). Note that by definition this function only works when s only contains digits, that is, if it encodes a natural number. Otherwise, it returns '-1'. See http://cvc4.cs.stanford.edu/wiki/Strings for details.

>>> prove $ \s -> let n = strToNat s in length s .== 1 .=> (-1) .<= n .&& n .<= 9
Q.E.D.

natToStr i. Retrieve string encoded by integer i (ground rewriting only). Again, only naturals are supported, any input that is not a natural number produces empty string, even though we take an integer as an argument. See http://cvc4.cs.stanford.edu/wiki/Strings for details.

>>> prove $ \i -> length (natToStr i) .== 3 .=> i .<= 999
Q.E.D.