The theory of sequences, supported by many SMT solvers, models program data types including bounded arrays and lists. Sequences are parameterized by the element data type and provide operations such as accessing elements, concatenation, forming sub-sequences and updating elements. Strings and sequences are intimately related; many operations, e.g., matching a string according to a regular expression, splitting strings, or joining strings in a sequence, are frequently used in string-manipulating programs. These operations are unfortunately not supported by existing SMT solvers, which only consider the generic theory of sequences. In this paper, we propose a theory of string sequences and study its satisfiability. We show that, while it is undecidable in general, the decidability can be recovered %is decidable for the straight-line fragment. This is shown by encoding a string sequence into a string and providing associated pre-image computation for various string sequence operations, to which existing decision procedure for strings and integer constraints can be applied. We implement the new decision procedure as a tool TOOLNAME and carry out experiments on benchmark constraints generated from both real-world and hand-crafted JavaScript programs. The experiments confirm the efficacy of our approach.