s2s: An Eager SMT Solver for Strings

String constraint solving describes the problem of determiningt he satisfiability of first-order formulas where variables range overs trings.Automated procedures fors olving these problems areknown as string solvers.Most existing solvers adopt al azy SMT approach, where aS AT solver handles the Boolean structureofthe formula and alternates with aspecialized string reasoninge ngine, following the CDCL(T) paradigm.An alternative strategy,c alled eager SMT solving, reduces the entire problem to Boolean satisfiability,a llowing it to be handled directly by aSAT solver.While successful eager approaches have been proposed, current implementations either lack expressiveness or aren ot publicly available.Here, we present an ew eager string solver based on existing techniques, capable of solving Boolean combinations of word equations, regular constraints,and linear arithmetic overs tring lengths.An evaluation on the SMT-LIB string benchmarks shows that our approach is competitive on ab road set of problems compared to state-of-the-art solvers, and even outperformst hem in many cases.In particular, our solver demonstrates close to best-in-class performance on the SMT-COMP pures tring benchmarks.