SMTQuery: Analysing SMT-LIB String Benchmarks

Constraint satisfaction problems involving strings have been a subject of theoretical study for decades, but it is only in recent years that practical solving methods have begun to emerge. This increasing interest in solving string constraints led to the development of various techniques and solvers, often accompanied by specific benchmark sets. As a result, there is now a substantial corpus of publicly available, yet largely unclassified, such benchmarks. In this context, we present SMTQuery, a framework for maintaining and analyzing benchmarks for SMT string problems. SMTQuery enables the execution of user-defined queries to extract domain-specific information from these benchmarks, facilitating a deeper analysis of the underlying problems. We demonstrate its utility by analyzing over 100,000 benchmarks and training an algorithm selection model to match benchmarks with suitable solvers.