Regular expressions are a classical concept in formal language
theory. Regular expressions in programming languages (RegEx) such as
JavaScript, feature non-standard semantics of operators
(e.g. greedy/lazy Kleene star), as well as additional features such as
capturing groups and references. While symbolic execution of programs
containing RegExes appeals to string solvers natively supporting
important features of RegEx, such a string solver is hitherto
missing. In this paper, we propose the first string theory and string
solver that natively provides such support. The key idea of our string
solver is to introduce a new automata model, called prioritized
streaming string transducers (PSST), to formalize the semantics of
RegEx-dependent string functions.  PSSTs combine priorities, which
have previously been introduced in prioritized finite-state automata
to capture greedy/lazy semantics, with string variables as in
streaming string transducers to model capturing groups. We validate
the consistency of the formal semantics with the actual JavaScript
semantics by extensive experiments.  Furthermore, to solve the string
constraints, we show that PSSTs enjoy nice closure and algorithmic
properties, in particular, the regularity-preserving property (i.e.,
pre-images of regular constraints under PSSTs are regular), and
introduce a sound sequent calculus that exploits these properties and
performs propagation of regular constraints by means of taking
post-images or pre-images. Although the satisfiability of the string
constraint language is generally undecidable, we show that our
approach is complete for the so-called straightline fragment. We
evaluate the performance of our string solver on over 195 000 string
constraints generated from an open-source RegEx library. The
experimental results show the efficacy of our approach, drastically
improving the existing methods (via symbolic execution) in both
precision and efficiency.