SMTQuery: A Novel Tool for Analyzing SMT-LIB String Benchmarks

Constraint satisfaction problems involving strings have been a subject of theoretical study for decades, but the recent years have seen an increased interest in the development of practical solving methods. This 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.