  Expression simplification is an important task necessary in a variety of
domains, e.g., compilers, digital logic design, etc. Syntax-guided synthesis
(SyGuS) with a cost function can be used for this purpose, but ordered
enumeration through a large space of candidate expressions can be expensive.
Equality saturation is an alternative approach which allows efficient
construction and maintenance of expression equivalence classes generated by
rewrite rules, but the procedure may not reach saturation, meaning global
minimality cannot be confirmed.
  We present a new approach called rewrite-guided synthesis (ReGiS), in which a
unique interplay between SyGuS and equality saturation-based rewriting helps to
overcome these problems, resulting in an efficient, scalable framework for
expression simplification.
  We demonstrate the flexibility and practicality of our approach by applying
ReGiS to regular expression denial of service (ReDoS) attack prevention. Many
real-world regular expression matching engines are vulnerable to these
complexity-based attacks, and while much research has focused on detecting
vulnerable regular expressions, we provide a way for developers to go further,
by automatically transforming their regular expressions to remove
vulnerabilities.
