Expand description
Basic string representation and operations for the SMT-LIB theory of strings
In SMT-LIB, a string is a sequence of integers in the range 0x00000 .. 0x2FFFF (inclusive). This is enough to encode Unicode characters but can also include non Unicode characters.
This module provide functions for constructing SMT string constants. It also implements all operations on strings defined by the SMT-LIB standard.
We limit the length of string constants to i32::MAX and the code will panic if this bound is exceeded.
Structs§
- SmtString
- Internal representation of an SMT string
Constants§
- EMPTY
- The empty string
- MAX_
CHAR - Maximal character index
- MAX_
LENGTH - Maximal length of a string
- REPLACEMENT_
CHAR - Replacement for an integer not in the range [0…0x2FFFF]
Functions§
- char_
to_ smt - Convert integer x (interpreted as a Unicode codepoint) to a string in the SMT syntax:
- good_
char - Check whether an integer is a valid SMT character
- good_
string - Check whether all elements in a slice are valid SMT characters
- parse_
smt_ literal - Parse a string literal in the SMT-LIB syntax and convert it to an SmtString.
- smt_
char_ as_ string - Convert an SMT character to a string literal
- str_at
- Character at index i in s, converted to a single-character string
- str_
concat - Concatenate two strings
- str_
contains - Check whether s2 is a substring of s1
- str_
from_ code - Single-character string with character code x
- str_
from_ int - Convert x to a string
- str_
indexof - Index of the first occurrence of s2 in s1, starting from index i
- str_
is_ digit - Check whether s contains a single digit between ‘0’ and ‘9’
- str_le
- Lexicographic comparison.
- str_len
- String length
- str_lt
- Strict lexicographic comparison.
- str_
prefixof - Check whether s1 is a prefix of s2
- str_
replace - Replace the first occurrence of p in s with r.
- str_
replace_ all - Replace all occurrences of p in s with r.
- str_
substr - Substring of s that starts at index i and has length at most n
- str_
suffixof - Check whether s1 is a suffix of s2
- str_
to_ code - Code for s if s is a single-character string, -1 otherwise
- str_
to_ int - Convert s to an integer