A symbolic algorithm for the case-split rule in solving word constraints with extensions (technical report)

string constraints, satisfiability modulo theories, regular model checking,
Nielsen transformation, finite automata, monadic second-order logic over strings

Case split is a core proof rule in current decision procedures for the theory of
string constraints. Its use is the primary cause of the state space explosion in
string constraint solving, since it is the only rule that creates branches in the
proof tree. Moreover, explicit handling of the case split rule may cause
recomputation of the same tasks in multiple branches of the proof tree. In this
paper, we propose a symbolic algorithm that significantly reduces such
a redundancy. In particular, we encode a string constraint as a regular language
and proof rules as rational transducers. This allows us to perform similar steps
in the proof tree only once, alleviating the state space explosion. We also
extend the encoding to handle arbitrary Boolean combinations of string
constraints, length constraints, and regular constraints. In our experimental
results, we validate that our technique works in many practical cases where other
state-of-the-art solvers fail to provide an answer; our Python prototype
implementation solved over 50% of string constraints that could not be solved by
the other tools.