Proposed operator str.indexof_re

[barrettcw]

From Andy and Andres (email May 21, 2021):

Hi Cesare and all,

Andres and I discussed having another operator in SMT-LIB for the theory of strings:

(str.indexof_re x R n)

of type (-> String RegLan Int Int)

which returns the first index, starting from n in x that is a non-empty match for regular expression R.

This operator could be used when reasoning about str.replace_re, analogously to how str.indexof relates to str.replace.

Cheers,
Andy