  We introduce a flexible class of well-quasi-orderings (WQOs) on words that
generalizes the ordering of (not necessarily contiguous) subwords. Each such
WQO induces a class of piecewise testable languages (PTLs) as Boolean
combinations of upward closed sets. In this way, a range of regular language
classes arises as PTLs. Moreover, each of the WQOs guarantees regularity of all
downward closed sets. We consider two problems. First, we study which (perhaps
non-regular) language classes permit a decision procedure to decide whether two
given languages are separable by a PTL with respect to a given WQO. Second, we
want to effectively compute downward closures with respect to these WQOs. Our
first main result that for each of the WQOs, under mild assumptions, both
problems reduce to the simultaneous unboundedness problem (SUP) and are thus
solvable for many powerful system classes. In the second main result, we apply
the framework to show decidability of separability of regular languages by
$\mathcal{B}\Sigma_1[<, \mathsf{mod}]$, a fragment of first-order logic with
modular predicates.
