2020/10/14 by Murphy Berzish, Mitja Kulczynski, Berzish, Murphy +11 · 4 citations
Computer Science · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Natural Language Processing Techniques #Network Packet Processing and Optimization #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.2010.07253
openalex publication_date 2020/10/14 · openalex created_date 2022/07/25 · openalex updated_date 2026/07/28
We present a novel length-aware solving algorithm for the quantifier-free\nfirst-order theory over regex membership predicate and linear arithmetic over\nstring length. We implement and evaluate this algorithm and related heuristics\nin the Z3 theorem prover. A crucial insight that underpins our algorithm is\nthat real-world instances contain a wealth of information about upper and lower\nbounds on lengths of strings under constraints, and such information can be\nused very effectively to simplify operations on automata representing regular\nexpressions. Additionally, we present a number of novel general heuristics,\nsuch as the prefix/suffix method, that can be used in conjunction with a\nvariety of regex solving algorithms, making them more efficient. We showcase\nthe power of our algorithm and heuristics via an extensive empirical evaluation\nover a large and diverse benchmark of 57256 regex-heavy instances, almost 75%\nof which are derived from industrial applications or contributed by other\nsolver developers. Our solver outperforms five other state-of-the-art string\nsolvers, namely, CVC4, OSTRICH, Z3seq, Z3str3, and Z3-Trau, over this\nbenchmark, in particular achieving a 2.4x speedup over CVC4, 4.4x speedup over\nZ3seq, 6.4x speedup over Z3-Trau, 9.1x speedup over Z3str3, and 13x speedup\nover OSTRICH.\n