We describe a uniform and efficient framework for checking the
satisfiability of a large class of string constraints.  The framework
is based on the observation that both satisfiability and
unsatisfiability of common constraints can be demonstrated through
witnesses with simple patterns.  These patterns are captured using
flat automata each of which consists of a sequence of simple loops. We
build a Counter-Example Guided Abstraction Refinement (CEGAR)
framework which contains both an under- and an over-approximation
module. The flow of information between the modules allows to increase
the precision in an automatic manner. We have implemented the
framework as a tool and performed extensive experimentation that
demonstrates both the generality and efficiency of our method.