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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

SMTQuery: Analysing SMT-LIB String Benchmarks

  • Mitja Kulczynski,
  • Kevin Lotz,
  • Florin Manea,
  • Danny Bøgsted Poulsen,
  • Paul Sarnighausen-Cahn

摘要

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.