Checking Regular Expressions in Cvc5 Proofs

Abstract

cvc5 is a state-of-the-art proof-producing SMT solver, capable of solving formulas over a myriad of theories, including Unicode strings. Matching regular expressions against concrete strings is done numerous times during the solving process, and forms a bottleneck in proof-checking for unsatisfiable formulas. We describe three approaches for checking regular expressions in the Eunoia proof-checking framework, and evaluate them on proofs produced by cvc5.

B. Dutertre—This work does not relate to the author’s position at Amazon.

1 Introduction

This work is part of a research program to efficiently check unsatisfiability proofs produced by Satisfiability Modulo Theories (SMT) solvers [4]. We focus on the ${\text {cvc5}}$ [2] SMT solver and the Eunoia [10] proof framework. We implement checking procedures for a common reasoning step in the SMT-LIBtheory of strings: matching regular expressions. These are implemented as side conditions: Eunoiaprograms that are defined in proof rules executed during proof checking.

Solving string constraints involves matching many concrete strings and regular expressions, to the point that verifying these matching steps becomes a bottleneck in proof checking. Implementing standard algorithms for regular expression checking as side conditions in Eunoiais challenging, because Eunoiaoffers limited support for standard data structures and control flow commands.

We have implemented three approaches. The first and simplest is based on backtracking. However, this basic approach does not perform well in many cases. The second follows Thompson’s construction, and the third adopts Brzozowski’s derivatives [5]. Our experiments show that the derivatives-based approach performs best and is therefore now the default in ${\text {cvc5}}$’s main branch.

Section 2 presents necessary background. Section 3 to 5 survey the three approaches. We evaluate them in Sect. 6,¹ and conclude in Sect. 7.

Related Work. The collection of proof rules for checking ${\text {cvc5}}$ proofs is described in [9]. Recent work [12] provides a solver whose calculus is verified in Lean. We focus on independent proof-checking for unsatisfiability results.

2 Preliminaries

Table 1 shows a sub-signature of the theory of strings [3], focusing on regular expressions (regexes). The sorts of strings and regular languages are $\mathcal {S}$ and $\mathcal {R}$, respectively. Operators noneand to_rerepresent the empty language and string literals (w.l.o.g., of length 1), respectively, while $\epsilon$ denotes the empty string. Other constructors include $\textit{comp}$ (complementation), $\textit{star}$ (Kleene closure), $\textit{rcon}$ (concatenation), $\textit{union}$ (union), and $\textit{inter}$ (intersection). The signature includes all string literals, denoted with double quotes. We often use standard regex notation, e.g., writing $a^*b$ instead of $\textit{rcon}({\textit{star}({\textit{to}\_\textit{re}({''{a}''})})},{\textit{to}\_\textit{re}({''{b}''})})$. The implementation supports additional ${\text {SMT-LIB}}$ operators (e.g. character ranges).

Table 1. Fragment of ${\text {SMT-LIB}}$ theory of strings.

Table 2. Builtins in Eunoia.

Eunoiais a logical framework for proofs, equipped with the ${\text {Ethos}}$ proof checker [8, 10], which supports dagification of terms and memoization of programs. Variadic terms are called lists. Internally, lists are LISP-style expressions. Eunoiaincludes a minimal standard library for lists and strings, which implements common operations natively for efficiency, such as the ones listed in Table 2. Eunoiaallows defining side conditions in the form of functional programs. The most direct rule that relies on regex matching is str-​in-​re-​eval, which matches a string against a regex. Other rules include, e.g., re-​inter-​inclusion and str-​replace-​re-​eval, that use matching for complex regex queries.

A nondeterministic finite automaton (NFA) $(\mathcal {Q}, \Sigma , \Delta , q_s, q_a)$ consists of finite sets $\mathcal {Q}$ and $\Sigma$ of states and letters, with $\epsilon \notin \Sigma$, $\Delta : \mathcal {Q}\times (\Sigma \cup \{\epsilon \}) \rightarrow \mathcal {P}(\mathcal {Q})$, the transition function, and $q_s,q_a\in \mathcal {Q}$, the start and accepting states. The $\epsilon$-closure of q is the set of states reachable from q by $\epsilon$-transitions.

3 Backtracking-Based Approach

Backtracking works by analyzing the regular expression and applying sub-queries recursively. Pseudocode for this approach is given in Algorithm 1. Function $\textsc {BtRec}$ takes a string s, index n, and two regular expressions $r_1$ and $r_2$. It determines whether s conforms to the pattern defined by regex $r_1$ followed immediately by regex $r_2$. Parameter n specifies the minimum size of the prefix of s that must be consumed by $r_1$. We use $\textit{null}$ as an internal marker for invalid regexes. When first calling $\textsc {BtRec}$, n is passed as 0 and $r_2$ as $\textit{null}$. Some cases require considering every partition of the string (lines 3–6). If a match fails in the recursion, the algorithm backtracks, causing an exponential growth in execution time. We show a snippet from the Eunoiacode of $\textsc {BtRec}$ in Figure 1.

Algorithm 1

Backtracking algorithm for regex matching.

Fig. 1.

Eunoia code for $\textsc {BtRec}$.

Example 1

Consider the execution of $\textsc {BtRec}(''{aab}'',0,a^{*}b,\textit{null})$ to determine whether "aab" matches regex $a^{*}b$. Since $r_2=\textit{null}$, we skip the conditional. Then, we recurse on line 13, calling $\textsc {BtRec}(''{aab}'',0,a^*,b)$. In the recursive call, $r_2\ne \textit{null}$, and so we enter the conditional. There, we consider all splits of $''{aab}''$ into two strings. When $i=2$, the match succeeds.

4 NFA-Based Approach

The second approach is based on Thompson’s construction of NFAs [11]. It requires the construction of an automaton and then the simulation of the automaton on the input string. We only use this approach on regexes that exclude $\textit{comp}$ and $\textit{inter}$, as these operators require expensive transformations. For regexes including these operators, we fall back to backtracking.

Eunoiacannot naturally represent NFAs as directed graphs, due to its strict bottom-up evaluation that does not support cycles. Instead, we represent an NFA as a list of transitions of the form $(q,\alpha ,q')$, where q and $q'$ are states and $\alpha$ is a character or $\epsilon$. The states are represented by string identifiers. To ensure uniqueness, we use a path-based identifier scheme. Each recursive call carries a string that encodes its position.

Algorithm 2

Function $\textsc {BNR}$ for constructing automata from regexes.

The construction is described in Algorithm 2. Function $\textsc {BNR}$ takes a regular expression r without $\textit{comp}$ and $\textit{inter}$, and computes an equivalent NFA. For that, it takes additional arguments: (string identifiers for) start and accept states ($q_s$ and $q_a$, respectively), a list $\delta$ of transitions, and a path context $\sigma$. It is called with a start state $''{s}''$, accepting state $''{a}''$, an empty transition list, and an empty path context. The result is a transition list that represents an NFA.

Fig. 2.

The NFA for $a^*b$ from the transition list generated by $\textsc {BNR}$.

Example 2

Running $\textsc {BNR}$ (Algorithm 2) on regular expression $r = a^*b$ with $q_s:=''{s}''$, $q_a:=''{a}''$, $\delta := [ ]$, and $\sigma := ''{}''$, we identify expression $a^*b$ as a concatenation and generate a unique intermediate identifier based on the current path $\sigma$: $q_{mid} = \textit{sconcat}({\sigma },{''{m}''}) = ''{m}''$. The problem is then split into two recursive calls. Eventually, we obtain four transitions: $(''{s}'', \epsilon , ''{lh}'')$, $(''{lh}'', ''{a}'', ''{lh}'')$, $(''{lh}'', \epsilon , ''{m}'')$, and $(''{m}'', ''{b}'', ''{a}'')$. A graphical representation is in Fig. 2.

After construction, we simulate the NFA on the input string. For each letter, we identify the list of reachable states by scanning the transition list, which can be costly. The algorithm updates the reachable states while scanning the input, and accepts if the final set contains the accepting state.

Example 3

Simulating the NFA of Example 2 with string $s = ''{aab}''$, the $\epsilon$-closure of the initial state $''{s}''$ consists of $''{s}''$, $''{lh}''$, and $''{m}''$. The first character to match is $\text {"a"}$. States $''{s}''$ and $''{m}''$ yield no transitions for $\text {"a"}$. State $''{lh}''$ transitions to $''{lh}''$, so $''{lh}''$ is added as a reachable state. The algorithm continues until letter $\text {"b"}$ is consumed, at which point $q_a$ belongs to the reachable states.

4.1 Optimizations

To avoid quadratic simulation, we represent the automaton hierarchically, each letter points to a nested transition list. Due to term dagification in ${\text {Ethos}}$, this tree-shaped structure is stored as a DAG. Simulation shifts from global scanning to walking a decision tree. Since the underlying representation is acyclic, we implement cycles using an execution stack. The marks $\textit{LoopEntry}$ and $\textit{LoopExit}$ serve as control instructions that do not consume input and are used to simulate NFA loops. For a Kleene-star expression, the construction places a $\textit{LoopEntry}$ before the body and a matching $\textit{LoopExit}$ after it. When execution reaches a $\textit{LoopEntry}$, it pushes a reference to this entry point onto the stack and proceeds into the loop body. When execution reaches the corresponding $\textit{LoopExit}$, it pops this reference and branches nondeterministically.

Example 4

The optimized construction for $a^*b$ results in the following hierarchical representation, which is illustrated in Fig. 3. Notice that the top level only contains two mappings, one for $\textit{LoopEntry}$ and one for b.

$$ [{\textbf {(}}\textit{LoopEntry},[(a,[(\textit{LoopExit},[(b,[\textsc {Accept}])])])]{\textbf {)}}, {\textbf {(}}b,[\textsc {Accept}]{\textbf {)}}] $$

Fig. 3.

Hierarchical representation for the optimized NFA construction of $a^*b$.

5 Derivatives-Based Approach

Algorithm 3

Function $\textsc {Der}$ for computing derivatives.

Our last approach is based on Brzozowski derivatives [5], as outlined in Algorithm 3. It uses function $\textsc {Nlbl}$, which checks if a regex accepts $\epsilon$. Function $\textsc {Der}$ computes the regex remaining after matching a character, which is called a derivative. For $\emptyset$ and $\epsilon$, this is none. For single characters, the derivative is $\epsilon$ if the current character matches. Boolean operators and $\textit{star}$ are handled recursively. The derivative of a concatenation $r_1 r_2$ splits according to whether $r_1$ accepts $\epsilon$. The string is accepted if the final derivative accepts $\epsilon$.

Example 5

For string $''{aab}''$ and regex $a^*b$, Algorithm 3 computes the derivative for $\text {"a"}$, transforming $a^*b$ to $\emptyset \cup (\epsilon \cdot a^*) \cdot b$, as $a^*$ accepts $\epsilon$. After the derivative for ‘b’ is computed, the string is accepted because the final expression is nullable. Notice that the final derivative is quite involved, even for this simple case, namely:

$$ \emptyset \cup \left( \emptyset \cup \left( \epsilon \cup \left( \left( \left( (\emptyset \cdot a^*) \cup (\emptyset \cdot a^*) \right) \cup (\emptyset \cdot a^*) \right) \cdot b \right) \right) \right) $$

5.1 Optimizations

The naive implementation frequently involves redundant expressions (e.g., $\emptyset \cup r$, $r \cup r$, or $\epsilon \cdot r$), leading to an unnecessary growth in the size of the regular expression. To mitigate this, we enforce the algebraic simplification rules from [5, 6] during the construction of the derivative, which flatten and normalize applications of union, interand rcon, while also eliminating unnecessary occurrences of $\epsilon$ and none. Crucially, we keep terms normalized during construction, relying on this invariant and Eunoia’s native list operators (e.g., lconcatand diff).

Example 6

With the simplification, the partial derivative for $\text {"a"}$ remains $a^*b$, without any $\epsilon$ or none. The final derivative is simply $\epsilon$, which is trivially nullable, and significantly shorter than the equivalent derivative computed in Example 5.

6 Evaluation

We use a cluster of 23 machines with Intel Xeon Gold 6348 CPUs. Proofs are generated with ${\text {cvc5}}$ 1.3.2 using limits of 60 s and 8GB, and are checked separately with ${\text {Ethos}}$ 0.2.2 using the same limits. There are 103,405 benchmarks in logics $\text {QF}\_\text {S}$, $\text {QF}\_\text {SLIA}$, and $\text {QF}\_\text {SNIA}$ of the 2024 release of the ${\text {SMT-LIB}}$ benchmark library [7]. Within the given resources, ${\text {cvc5}}$ is able to determine that 38,765 are unsatisfiable. 3,118 unsatisfiability proofs apply rule str-​in-​re-​eval. These proofs comprise our ${\textbf {Organic}}$ benchmark set. The second set consists of 35,627 ${\textbf {Synthetic}}$ proofs, obtained by logging a sequence of calls to the regex matching rule, applied to all regex checks performed during solving. These are not unsat proofs, but sequences of calls to rule str-​in-​re-​eval.

Our configurations are listed on the left of Table 3, which summarizes the results. In ${{\textbf {LB}}}$ the regex matching rule accepts each application immediately. It provides a lower bound for checking time. For the other configurations, we list the relevant section and the number of lines of code (LOC). $\textbf{NFA}^{+}$ has fewer LOCs than ${{\textbf {NFA}}}$ because it does not need to maintain unique string identifiers.

The number of proofs commonly checked by all approaches is in parentheses. Total run-times (T) and memory usage (M) are given for the set of commonly checked proofs. Number of checked proofs (# S) is also given. On ${\textbf {Organic}}$, $\textbf{DER}^{+}$ is nearly optimal, taking just 8 s more than ${{\textbf {LB}}}$. The results also show that the optimizations of the NFA and derivatives approaches are crucial.

On ${\textbf {Synthetic}}$, ${{\textbf {BT}}}$ checks slightly more proofs than the optimized approaches. These proofs originate from the sub-family redos_attack_ detection of $\text {QF}\_\text {SLIA}$ and share a similar pattern with extremely long strings. On these, the default search order of ${{\textbf {BT}}}$ guides it to an early termination of the loop in Algorithm 1, avoiding an exhaustive search. Thus, ${{\textbf {BT}}}$ remains a viable alternative with performance complementary to the others on such benchmarks.

When considering commonly checked proofs, the results are similar to set ${\textbf {Organic}}$. Configurations ${{\textbf {NFA}}}$ and $\textbf{NFA}^{+}$ fall back to ${{\textbf {BT}}}$ on $\sim$5% of the checks. Finally, we remark that configuration ${{\textbf {BT}}}$ is sensitive to the order in which the splits into two strings are considered in Algorithm 1. For example, when we reverse the order of the splits, its performance significantly degrades.

Table 3. Summary of configurations and results.

7 Conclusion

We have implemented and evaluated several approaches for checking regular expression membership in the ${\text {Ethos}}$ checker for ${\text {cvc5}}$ proofs. The primary obstacle was reconciling efficiency with the strict architectural constraints of Eunoia. Future work includes further optimizing the derivatives and NFA approaches, and implementing similar support in Carcara [1].