  We investigate the properties of formal languages expressible in terms of
formulas over quantifier-free theories of word equations, arithmetic over
length constraints, and language membership predicates for the classes of
regular, visibly pushdown, and deterministic context-free languages. In total,
we consider 20 distinct theories and decidability questions for problems such
as emptiness and universality for formal languages over them. First, we discuss
their relative expressive power and observe a rough division into two
hierarchies based on whether or not word equations are present. Second, we
consider the decidability status of several important decision problems, such
as emptiness and universality. Note that the emptiness problem is equivalent to
the satisfiability problem over the corresponding theory. Third, we consider
the problem of whether a language in one theory is expressible in another and
show several negative results in which this problem is undecidable. These
results are particularly relevant in the context of normal forms in both
practical and theoretical aspects of string solving.
