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

### Strings

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? | ✓ | ✓ | ✓ |

### Sequences

Syntax | Semantics | CVC4 | Norn | Z3seq | Z3str3 |
---|---|---|---|---|---|

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 |

### Regular Expressions

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. | ✓ |