String and Sequence Syntax

SMT-LIB-Like String and Sequence Syntax Support (In Progress)

Syntax	Semantics	CVC4	Norn	Z3seq	Z3str3
String literal	Printable ASCII characters enclosed in double quotes	✓	✓	✓	✓
String sort	E.g. in (declare-const X String)	✓	✓	✓	✓
(= s t)	Equality: String x String -> Bool	✓	✓	✓	✓
(int.to.str i)	Retrieve string encoding of integer i.	✓		✓	✓
(str.to.int s)	Retrieve integer encoded by string s.	✓		✓	✓
(str.++ a b c)	Concatenation of one or more strings	✓	✓	✓	✓
(str.at s offset)	Substring of length 1 at offset in s.	✓		✓	✓
(str.contains s sub)	Does s contain the substring sub?	✓		✓	✓
(str.indexof s sub offset)	First position of sub at or after offset in s. Returns -1 otherwise.	✓		✓	✓
(str.indexof s sub)	First position of sub in s. Returns -1 otherwise.	✗	✗	✓	✓
(str.len s)	Length. Returns an integer.	✓	✓	✓	✓
(str.prefixof pre s)	Is pre a prefix of s?	✓		✓	✓
(str.replace s src dst)	Replace the first occurrence of src by dst in s.	✓	✓	✓	✓
(str.substr s offset length)	Retrieves string of s at offset of length length	✓		✓	✓
(str.suffixof suf s)	Is suf a suffix of s?	✓		✓	✓

Syntax	Semantics	Z3seq
Seq sort	E.g. in (declare-const s (Seq Int)) for sequence of integers.	✓
(= s t)	Equality: Seq x Seq -> Bool	✓
(as seq.empty (Seq S))	The empty sequence with elements of sort S.	✓
(seq.unit elem)	Sequence with a single element elem.	✓
(seq.++ a b c)	Concatenation of one or more sequences	✓
(seq.at s offset)	Subsequence of length 1 at offset in s.	✓
(seq.contains s sub)	Does s contain the subsequence sub?	✓
(seq.indexof s sub offset)	First position of sub at or after offset in s. Returns -1 otherwise.	✓
(seq.indexof s sub)	Retrieves first position of sub in s. Returns -1 otherwise.	✓
(seq.len s)	Length. Returns an integer.	✓
(seq.replace s src dst)	Replace the first occurrence of src by dst in s.	✓
(seq.extract s offset length)	Retrieves subsequence of s at offset	✓
(seq.prefixof pre s)	Is pre a prefix of s?	✓
(seq.suffixof suf s)	Is suf a suffix of s?	✓
(seq.subseq s sub)	Does s contain the subsequence sub?
(seq.nth s n)	Subsequence of length 1 at offset in s.
(seq.cons e s)	Prepend an element e to s
(seq.rev.cons s e)	Postpend an element e to s
(seq.head s)	First element of s
(seq.tail s)	Tail of s
(seq.last s)	Last element of s
(seq.first s)	All but the last element of s

Syntax	Semantics	CVC4	Norn	Z3seq	Z3str3
(str.in.re s r)	Determine if string s is in the language generated by r.	✓	✓	✓	✓
(str.to.re s)	Convert string to regular expression accepting s.	✓	✓	✓	✓
((_ re.loop lo hi) r)	from lo to hi number of repetitions of r.	✗	✗	✓	✗
(as re.all R)	The regular expression of sort R accepting every sequence.	✗	✗	✓	✓
(as re.allchar R)	The regular expression of sort R accepting every string.	✓	✗	✓	✓
(as re.empty R)	The regular expression R rejecting every sequence.	✗	✗	✓	✓
(as re.nostr R)	The regular expression of sort R rejecting every string.	✓	✗	✓	✓
(re.* r)	Kleene star.	✓	✓	✓	✓
(re.+ r)	Kleene plus.	✓	✗	✓	✓
(re.++ r1 r2 r3)	Concatenation of regular expressions.	✓	✓	✓	✓
(re.inter r1 r2)	The intersection of regular languages.	✓	✗	✓	✗
(re.opt r)	Zero or one use of r.	✓	✗	✓	✓
(re.range ch1 ch2)	The range of elements between ch1 and ch2.	✓	✗	✓	✓
(re.union r1 r2)	The union of regular languages.	✓	✓	✓	✓
(re.complement r)	Complement language of r
(re.of.pred array r)	Range of predicate; array is an array of booleans
(re.difference r1 r2)	Language that accepts strings that are not accepted by both r1 and r2
(seq.in.re s r)	Determine if sequence s is in the language generated by r.			✓
(seq.to.re s)	Convert sequence to regular expression accepting s.			✓