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 -> bnot (null s) ==> singleton (head s) .++ tail s .== s
Q.E.D.

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\NUL\EOT" :: 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 -> 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.

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 $ \s i -> i .> 0 &&& i .< length s ==> indexOf s (subStr s i 1) .== i
Falsifiable. Counter-example:
  s0 = "\NUL\NUL\NUL\NUL\NUL" :: String
  s1 =                      3 :: Integer
>>> 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 n .>= 0 &&& n .< 10 ==> length s .== 1
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.