Z3str4: A Solver for Theories over Strings

Abstract

Satisfiability Modulo Theories (SMT) solvers supporting rich theories of strings have facilitated numerous industrial applications with the need to reason about string operations and predicates that are present in many popular programming languages. Constraints encountered in practical applications have immense value in inspiring new algorithms and heuristics that string solvers can take advantage of to tackle new, more difficult problems. This is especially relevant as the combinations of operators typically supported by string solvers, or that are encountered in program analysis constraints, quickly result in theories whose satisfiability problems are undecidable.

I present a number of theoretical and practical contributions in the domain of string solving. On the theoretical side, I illustrate decidability and undecidability results related to different relevant theories which include strings. On the practical side, I describe a collection of algorithms and heuristics designed to address challenges encountered in applications of string solvers, culminating with the introduction of Z3str4, a state-of-the-art solver for theories over strings. Z3str4 incorporates many improvements over its predecessor Z3str3, including an algorithm selection architecture that takes advantage of multiple solving algorithms in order to leverage the strengths of diverse string solving procedures against formulas they are predicted to be able to solve efficiently. I also present a back-end model construction algorithm for Z3str4 which is a hybrid between word-based and unfolding-based algorithms. Furthermore, I showcase the power of Z3str4 against other state-of-the-art tools in an empirical evaluation over a large and diverse collection of benchmarks. Additionally, I describe algorithms and heuristics specific to solving regular expression constraints, and demonstrate their effectiveness in a detailed and focused empirical evaluation.