Strings and Sequences in Z3

Introduction

Strings

Built-in types and constants

(declare-const a String)
(declare-const b String)
(assert (= (str.++ b a) (str.++ "abc" b)))
(check-sat)
(get-model)

String literals

To represent non-ASCII characters Z3 treats the sequence \xHH where HH are two hexa-decimal numerals (using one of the characters, 0-9, a-f, A-F) as an encoding of an 8 bit character. Furthermore, the following escape sequences correspond to their ASCII escape encodings.

\a

\b

\f

\n

\r

\t

\v

Note that other occurrences of the character \ are treated as the charcter \. The following example shows three ways to enter the newline character.

(define-const a String "\x0a")
(define-const b String "
")
(define-const c String "\n")
(simplify (= a b))
(simplify (= a c))
(simplify (str.++ a b c))

Operations

Note that (str.indexof s offset) is shorthand for (str.indexof s offset 0).

Examples

(simplify (str.++ (str.at "abc" 1) (str.at "abc" 0)))
(simplify (str.indexof "abcabc" "a"))
(simplify (str.indexof "abcabc" "a" 1))
(simplify (str.substr "xxabcyy" 2 3))

(declare-const a String)
(assert (= (str.++ a "b") (str.++ "a" a)))
(check-sat)

(declare-const a String)
(declare-const b String)
(declare-const c String)
(assert (= (str.++ a b) "abcd"))
(assert (= (str.++ b c) "cdef"))
(assert (not (= b "")))
(check-sat)

(declare-const a String)
(declare-const b String)
(assert (= (str.++ "abc" a) (str.++ b "cef")))
(assert (<= (str.len a) 2))
(check-sat)

(declare-const a String)
(declare-const b String)
(declare-const c String)
(assert (= (str.++ a "ab" b) (str.++ b "ba" c)))
(assert (= c (str.++ a b)))
(assert (not (= (str.++ a "a") (str.++ "a" a))))
(check-sat)
(get-model)

(declare-const a String)
(declare-const b String)
(declare-const c String)
(assert (str.contains a b))
(assert (str.contains b c))
(assert (not (str.contains a c)))
(check-sat)

(declare-const a String)
(declare-const b String)
(declare-const c String)
(assert (str.contains a b))
(assert (str.contains a c))
(assert (not (str.contains b c)))
(assert (not (str.contains c b)))
(check-sat)
(get-model)

(declare-const a String)
(declare-const b String)
(declare-const c String)
(assert (str.prefixof b a))
(assert (str.suffixof c a))
(assert (= (str.len a) (+ (str.len b) (str.len c))))
(assert (not (= a (str.++ b c))))
(check-sat)

Sequences

Operations

Examples

(declare-const s (Seq Int))
(declare-const t (Seq Int))
(declare-const j Int)
(declare-const b Int)

(assert (<= 10 (seq.len s)))
(assert (<= 8 j))
(assert (< j (seq.len s)))
(assert (= t (seq.++ (seq.extract s 0 j) (seq.unit b) (seq.extract s (+ j 1) (- (seq.len s) j 1)))))
(push)
(assert (not (= (seq.unit b) (seq.at t j))))
(check-sat)
(pop)
(push)
(assert (not (= (seq.len s) (seq.len t))))
(check-sat)
(pop)
(push)
(assert (not (= (seq.at s 8) (seq.at t 8))))
(assert (not (= (seq.at s 9) (seq.at t 9))))
(check-sat)
(pop)

Regular Expressions

Operations

The re.range operator expects two strings each encoding a single character. For example (str.range "a" "\xff") is a valid range of characters, while (str.range "aa" "") is not associated with any specified range.

For added compatibility with CVC4's format, Z3 also accepts expressions of the form (re.loop r lo hi). Z3 understands only the meaning of these terms when lo, hi are integer numerals.

What (not) to expect of regular expressions

Examples

(declare-const a String)
(push)
(set-info :status sat)
(assert (str.in.re a ((_ re.loop 1 3) (str.to.re "ab"))))
(assert (= (str.len a) 6))
(check-sat)
(get-model)
(pop)

(push)
(set-info :status unsat)
(assert (str.in.re a ((_ re.loop 1 3) (str.to.re "ab"))))
(assert (> (str.len a) 6))
(check-sat)
(pop)