Module smt_regular_expressions

Source
Expand description

Regular expressions as defined in the SMT-LIB QF_S Theory The alphabet is the set of u32 between 0 and 0x2FFFF.

Functionsยง

re_all
Full language
re_allchar
All strings of length 1
re_comp
Complement
re_concat
Concatenation of two regular expressions
re_concat_list
Concatenation of several regular expressions
re_diff
Difference of two regular expressions
re_diff_list
Difference of several languages
re_inter
Intersection of two regular expressions
re_inter_list
Intersection of several regular expressions
re_loop
Loop
re_none
Empty language
re_opt
Option
re_plus
Kleene cross
re_power
Power
re_range
Range
re_star
Kleene closure
re_union
Union of two regular expressions
re_union_list
Union of several regular expressions
str_in_re
Check whether a string is in a regular expression
str_replace_re
Replace the first and shortest occurrence of r by s2 in s1
str_replace_re_all
Replace all non-empty matches of r by s2 in s1
str_to_re
Singleton language