Regex Decision Procedures in Extended RE#

We develop decision procedures for extended regular expressions in the new ERE# framework that uses span semantics, utilizing the power of symbolic derivatives. We prove a normal form theorem in Lean for ERE# that is closed under all Boolean operations and provides the basis for the given decision procedures. The tool is evaluated on existing SMT benchmarks for regexes that shows it to be the fastest solver to date – often orders of magnitude faster than state-of-the-art – albeit specialized for the single-variable fragment of string theory.