A Regular Matching Constraint for String Variables

1 Introduction

Regular expressions are a powerful and useful way of processing strings. Nowadays they are commonly used in languages such as Python, Java and JavaScript for data parsing and validation. The widespread use of regular expressions arguably coincides with the increasing development of web applications heavily using string operations both explicitly (i.e., by directly invoking string functions) and implicitly (i.e., by silently converting objects of different type into strings). Unsurprisingly, this led to the development of a number of both static and dynamic string analysis frameworks especially targeted to cybersecurity issues [Bultan et al., 2017].

In this paper we focus on the dynamic side of string analysis, and more precisely on string constraint solving [Amadini, 2021], to show how the Constraint Programming (CP) paradigm [Rossi et al., 2006] can be used to tackle string constraints where a pattern -be it a regular expression, an automaton or a grammar- denoting a regular language is matched against a string variable. The key practical motivation of this work is the constraint-based reasoning about string manipulating programs, e.g., JavaScript web applications, where match constructs, and related operations like string replacement, are heavily used.

CP is a well-established framework for general-purpose constraint solving and optimization. Handling constraints over regular expressions is not new to CP, having been introduced in the early 2000's by Pesant [2004] for fixed sequences of integer variables, and more recently retrofitted by Amadini et al. [2018]. However, these works refer to the constraint regular(x,R) which only considers the membership of x to the regular language L(R) denoted by the finitestate automaton R, and not what is, nowadays, probably the most common operation: using R as a pattern to be matched against x. Instead, in this paper we will show how to handle in CP the constraint match(x, ρ) returning the position in x of the leftmost possible match of a string of L(ρ). To our knowledge, at present no CP propagator exists for match.

To represent the finite domain of bounded-length string variables, we consider the dashed string abstraction as done in [Amadini et al., 2018]. Given a finite alphabet Σ and a maximum string length λ, dashed strings (over-)represent subsets of {w ∈ Σ∗ | |w| ≤ λ} through the concatenation of distinct sets of characters called blocks. Using blocks of characters prevents the eager unfolding of the domain of a string variable into O(λ) integer variables, which is definitely a big plus when λ is large.

We compared the performance of our approach against different state-of-the-art string solving technologies. Empirical results underline the importance of implementing native support for the match constraint.

2 Preliminaries

In this section we give the necessary background notions about strings, regular languages, constraint programming and (dashed) string solving.

2.1 Strings and Regular Languages

Let Σ be a finite, non-empty alphabet and Σ∗ the set of all its strings. A string w ∈ Σ∗ is a finite sequence of |w| ≥ 0 characters of Σ, where |w| is the length of w (the empty string is denoted with ϵ). We focus on bounded-length strings: fixed λ ∈ N, we only consider strings w ∈ Σ∗ such that |w| ≤ λ.

The concatenation of v, w ∈ Σ∗ is denoted by v ·w (or simply by vw) while wn is the iterated concatenation: w0 = ϵ and wn = wwn-1 for n > 0. Similarly, given V,W ⊆ Σ∗ , we denote by V · W = {vw | v ∈ V,w ∈ W} (or simply by VW) their concatenation and with W n the iterated concatenation (W 0 = {ϵ}). We adopt a 1-based array notation: w[i] is the i-th symbol of w, with 1 ≤ i ≤ |w|.

We define l..u = {x ∈ Z | l ≤ x ≤ u} and denote with w[i..j] the substring of w from character i to character j, i.e., w[i]w[i + 1] · · · w[j] (if i > j, then w[i..j] = ϵ).

A subset L ⊆ Σ∗ is called a language. A regular language can be defined in several equivalent ways. For example, as the language L(R) accepted by a finite-state automaton R, the language L(r) denoted by regular expression r, or the language L(Γ) generated by regular grammar Γ. 1 We call regular pattern (shortly, pattern) a formalism ρ describing a regular language L(ρ).

A deterministic finite-state automaton (DFA) is a tuple R = (Σ,Q, δ, q0, F) where: Σ is the alphabet, Q the finite set of states, δ : Q × Σ → Q the transition function, q0 ∈ Q the initial state and F ⊆ Q the accepting or final states. A computation for w ∈ Σ∗ is a sequence of transitions s0 → · · · → sn where n = |w| and s0, . . . , sn ∈ Q such that si = δ(si-1,w[i]) for i = 1, . . . , n. We denote with ̂ δ : Q×Σ∗ → Q the extension of δ to strings such that ̂ δ(q, w) = q′ if and only if q → · · · → q′ is a computation for w. A string w ∈ Σ∗ is accepted by R if ̂ δ(q0,w) ∈ F. The language of R is L(R) = {w ∈ Σ∗ | ̂ δ(q0, w) ∈ F}.

If δ is a total function, the DFA is complete. If δ is partial, we can get a complete DFA by extending Q to Q′ = Q ∪ {q⊥}, and δ to δ ∪ {(q, c, q⊥) | q ∈ Q′ , c ∈ Σ, δ(q, c) = ⊥}. The complement automaton R having L(R) = Σ∗ \ L(R) is easily computed from a complete DFA R by complementing its final states. If there does not exist a DFAR′ with less than |Q| states such that L(R′ ) = L(R), then R is minimal. Given a regular pattern ρ, we denote by DFA(ρ) the minimal and complete DFA such that L(ρ) = L(DFA(ρ)).

If R = (Q,Σ, δ, q0, F) is complete, a state q ∈ F is said universally accepting if all computations from q bring to a state q′ ∈ F. Dually, q ∈ Q \ F is universally rejecting if all computations from q bring to a q′ ∈ Q \ F. If R is minimal, it has at most one universally accepting state, and at most one universally rejecting state (if they have two or more universally accepting/rejecting states then those states can be merged, so R would not be minimal). We denote with minlen(R) the minimum length of a string accepted by R.

A well-known way to identify regular languages is using regular expressions. We define inductively the set RE of regular expressions, and the language L(r) denoted by each r ∈ RE, as: (i) ∅ ∈ RE, denoting L(∅) = ∅; (ii) if c ∈ Σ ∪ {ϵ}, then c ∈ RE denoting L(c) = {c}; (iii) if r, r′ ∈ RE, then r · r′ ∈ RE denoting L(r · r′ ) = L(r)L(r′ ), and r|r′ ∈ RE denoting L(r|r′ ) = L(r) ∪ L(r′ ); (iv) if r ∈ RE then r∗ ∈ RE denoting L(r∗ ) = L(r)∗ .

2.2 Constraint Programming and String Solving

Constraint programming [Rossi et al., 2006] solves Constraint Satisfaction Problems (CSPs), defined by a triple (X,D, C) where: X = {x1, . . . , xn} is a finite set of variables, D = {D(x1), . . . ,D(xn)} is a set of domains, where each D(xi) is the set of the values that xi can take, and C is a set of constraints over the variables of X defining the feasible assignments. The goal is to find an assignment of domain values to corresponding variables satisfying all of the constraints in C. To do so, CP heavily relies on propagators. A propagator for a constraint C defined over variables x1, . . . , xk is an algorithm that aims to prune the most inconsistent values fromD(x1), . . . , D(xk) according to the semantics of C. The level of pruning is a compromise between efficacy (how many values we prune) and efficiency. Most of the propagators are not complete: a fixpoint is reached even if the domains could in principle be further pruned.

1 We assume that these formalism are familiar to the reader.

Most CSPs are defined over finite domains, i.e., D only contains finite sets, and X only contains integer variables. In this work, we also consider constraints over bounded-length strings. Fixing a finite alphabet Σ and an upper bound λ ∈ N, a CSP with bounded-length strings contains k > 0 string variables {x1, . . . , xk} ⊆ X such that D(xi) ⊆ Σ∗ and |xi| ≤ λ. The set C may contain well-known string constraints, such as string length, (dis-)equality, concatenation, substring selection, and finding/replacing. We refer to constraint solving involving string variables as string (constraint) solving.

Different approaches to string constraint solving have been proposed, based on: automata [Li and Ghosh, 2013; Tateishi et al., 2013], word equations [Berzish et al., 2017; Barbosa et al., 2022], unfolding (using either bit-vector solvers [Kie˙zun et al., 2012; Saxena et al., 2010] or CP [Scott et al., 2017]), and dashed strings [Amadini et al., 2020]. In this work we focus on the latter approach, which can be considered the state-of-the-art for CP string solving.

Dashed strings are special cases of regular expressions, defined by k > 0 blocks Sl1,u1 1 Sl2,u2 2 · · · Slk,uk k , where Si ⊆ Σ and 0 ≤ li ≤ ui ≤ λ for i = 1, . . . , k and Σki=1 li ≤ λ. For each block Sl,u , we call S its base and l, u its lower/upper bound, respectively. We denote with maxlen(X) the sum of the upper bounds of each block of X, with X[i] the i-th block of a dashed string X, and with |X| the number of blocks of X. We consider only normalised dashed strings, where the adjacent blocks have distinct bases and the null block ∅0,0 occurs only to denote the empty string.

Let γ(Sl,u ) = {x ∈ S∗ | l ≤ |x| ≤ u} be the language denoted by block Sl,u . 2 We extend γ to dashed strings: γ(Sl1,u1 1 · · · Slk,uk k ) = (γ(Sl1,u1 1 ) · · · γ(Slk,uk k )) ∩ S, where the intersection with S = {w ∈ Σ∗ | |w| ≤ λ} excludes the strings with length greater than λ. Normalisation entails that each string w ∈ S has a unique dashed string X such that w = γ(X).

Given dashed strings X and Y we define the relation X ⊑ Y ⇔ γ(X) ⊆ γ(Y ) denoting a relation "is more precise than" between dashed strings. Unfortunately, the set of dashed strings does not form a lattice according to ⊑ [Amadini et al., 2020]. For example, there is no single "best" dashed string denoting {ab, ba} ⊆ Σ∗ : three maximally accurate but incomparable dashed strings that represent this set are {a, b}2,2 , {a}0,1 {b}1,1 {a}0,1 and {b}0,1 {a}1,1 {b}0,1 , each represents a different over approximation. This means that workarounds have to be used to preserve the soundness of propagation.

2 γ(Sl,u ) is the set of strings having length in l..u and characters in S. We use the notation γ(X) instead of L(X) to be consistent with the original dashed string definition [Amadini et al., 2020].

From a graphical point of view, we can see each block Sli,ui i as a solid segment of length li followed by a dashed segment of length ui - li. The solid segment indicates that exactly li characters of Si must occur in each string of γ(Sl1,u1 1 · · · Slk,uk k ), and defines the mandatory part Sli,li . The dashed segment indicates that n characters of Si, with 0 ≤ n ≤ ui - li, may occur and defines the optional part S0,ui-li i . Consider, e.g., the graphical representation of dashed string X = {B,b}1,1 {o}2,4 {m}1,1 {!}0,3 in Fig. 1. Each string of γ(X) starts with B or b, followed by 2 to 4 os, one m, then 0 to 3 !s.

A convenient way to refer a dashed string is through its positions. Given X = Sl1,u1 1 · · · Slk,uk k , we can define 1 + ∑ki=1 ui positions (i, j) where index i ∈ {1, . . . , k} refers to block X[i] and offset j indicates how many characters from the beginning of X[i] we are considering. To better represent the beginning (or the end) of a block, offsets are 0-based. In particular, (i, 0) refers to the beginning of block i, and can be equivalently identified with (i - 1, ui-1), i.e., the end of block i - 1 (see Fig. 1). For convenience, we also consider (k + 1, 0) to be equivalent to the position (k, uk), and (0, k) for any k to be equivalent to position (1, 0), the beginning of the dashed string.

Given X = Sl1,u1 1 · · · Slk,uk k and positions (i, j), (i′ , j ′ ), we denote with X[(i, j), (i′ , j ′ )] the region of X between (i, j) and (i′ , j ′ ), i.e., X[(i, j), (i′ , j ′ )] is equal to:

where ⪯ is the lexicographic ordering between pairs.

For example, with X as in Fig. 1, X[(2, 1), (4, 2)] = {o}1,3 {m}1,1 {!}0,2 . For brevity, we indicate with X[P, ...] the "suffix region" X[P, (k, uk)] between a position P and the last position (k, uk) of X, and with X[..., P] the "prefix region" between (0, 0) and P. For example, with X as in Fig. 1 and P = (2, 3) we have X[..., P ] = {B,b}1,1 {o}2,3 and X[P, ...] = {o}0,1 {m}1,1 {!}0,3 .

3 Matching Regular Expressions

In this section we show how we propagate the match constraint. To do so, we need to introduce some notions and properties exploited by our propagator.

Definition 1. Let Σ be a finite alphabet and ρ a pattern for Σ. For each w ∈ Σ∗ we define the set MI(w, ρ) ⊆ 0..|w| of matching indexes of ρ in w as:

In practice, MI(w, ρ) is the set of all the positions in w where ρ matches a substring w′ of w, i.e., w′ ∈ L(ρ). For example, if Σ = {a, b, c}, ρ = ab(a|c)∗ and w = cabbcab then MI(w, ρ) = {2, 6}. If instead w = caacb, then MI(w, ρ) = {0} because no match occurs. Note that with this definition if ϵ ∈ L(ρ) then for each w ∈ Σ∗ \ {ϵ} we have MI(w, ρ) = 1..|w| because w[i..i - 1] = ϵ ∈ L(ρ) for i = 1, . . . , |w|. In this way, we capture the fact that ϵ occurs at each position of a non-empty string, being the empty string substring of every string.

Let ρ be a regular pattern. The (full) wrapping of ρ is the minimal pattern ⋆ρ⋆ denoting the language Σ∗L(ρ)Σ∗ . We also define the left-wrapping ⋆r, denoting Σ∗L(ρ), and the right-wrapping r⋆, denoting L(ρ)Σ∗ . For example, if Σ = {a, b, c} and ρ = ab(a|c)∗ its wrapping is ⋆ρ⋆ = (a|b|c)∗ab(a|b|c)∗ , the left-wrapping is ⋆ρ = (a|b|c)∗ab(a|c)∗ and the right-wrapping is ρ⋆ = ab(a|b|c)∗ .

Lemma 1. Let ρ be a regular pattern with L(ρ) ̸= ∅, R = DFA(ρ) and ̂R = DFA(⋆ρ⋆). The following properties hold:

• (i) ̂R has no universally rejecting states
• (ii) ̂R has exactly one universally accepting state

Proof. (i): Suppose ̂R has a universally rejecting state q⊥. ̂R is minimal, so there is a ̂R-computation q0 → · · · → q⊥ for a certain w0 ∈ Σ∗ . Hence, for each w ∈ Σ∗ we would have w0w ̸∈ L( ̂R). In particular, if w ∈ L(R) we would have w0w ̸∈ L( ̂R) = L(⋆R⋆) ⊇ L(⋆R) which is impossible being w0w ∈ L(⋆R) = Σ∗L(R).

(ii): Because L(ρ) ̸= ∅, there is at least a final state. If ̂R has no universally accepting states, there exist two states qi ∈ F , qj ̸∈ F and a character a ∈ Σ such that δ(qi, a) = qj . So there is a w ∈ L( ̂R) such that wa ̸∈ L( ̂R) which is impossible being L( ̂R) = Σ∗L(R)Σ∗ closed under concatenation. So, ̂R has at least a universally accepted state. Because it is minimal, it must have at most one universally accepting state. So, ̂R has exactly one universally accepting state.

Lemma 2. Let ρ be a regular pattern with ϵ ̸∈ L(ρ) and R = DFA(⋆ρ⋆) = (Σ,Q, δ, q0, F). For each w ∈ Σ∗ , if ̂ δ(q0, w) = q0 then w ̸∈ L(ρ).

Proof. Let w ∈ Σ∗ such that ̂ δ(q0, w) = q0 and suppose w ∈ L(ρ). Because L(ρ) ⊆ L(⋆ρ⋆), then w ∈ L(⋆ρ⋆) = L(R) so it must be q0 ∈ F and thus ϵ ∈ L(⋆ρ⋆). Because by hypothesis ϵ ̸∈ L(ρ), it must be ϵ ∈ L(⋆ρ⋆) \ L(ρ) which is impossible.

3.1 Propagating match

Let us now explain how we propagate i = match(x, ρ), which semantics is i = min(MI(x, ρ)). We represent the domain of x with a dashed string. However, this propagator also works when D(x) is a fixed sequence of integer variables as in [Pesant, 2004; Scott et al., 2017]. In fact, the sequence x1 · · · xn where D(xi) ⊆ Σ (xi = j iff x[i] is the j-th symbol of Σ) corresponds to dashed string D(x1)1,1 · · · D(xn)1,1 .

It is also important to note that, because we assume ϵ occurring at each position of a string, we have ϵ ∈ L(ρ) ⇒ match(x, ρ) = 1 for any string variable x. Hence, before propagating match we should check if ϵ ∈ L(ρ). If so, we can simply rewrite i = match(x, ρ) into i = 1. Because we focus on the more interesting cases, in the following we consider only patterns ρ such that ϵ ̸∈ L(ρ).

A specialized match propagator is not strictly necessary, e.g., we can impose 0 ≤ i ≤ |x| and rely on the regular propagator to rewrite i = match(x, ρ) into:

⎧⎪⎪⎨⎪⎪⎩ ¬regular(x, DFA(⋆ρ⋆)) if i = 0 ¬regular(x[1..i - 1], DFA(⋆ρ⋆)) ∧ regular(x[i..|x|],DFA(ρ⋆)) ∧ ∀j ∈ 1..i -1 : ¬regular(x[j..|x|],DFA(ρ⋆)) if i ̸= 0 (1)

This rewriting, especially when i is not fixed, is inefficient, as it involves a universal quantification over 1..i-1 and many reifications. 1 This implies a rather weak propagation. Note that ¬regular(x[1..i - 1],DFA(⋆ρ⋆)) is redundant, but it enables a stronger propagation. The universal quantification is instead necessary. Imagine, e.g., ρ = aa and x = baaa. Without ∀j ∈ 1..i - 1 : ¬regular(x[j..|x|],DFA(ρ⋆)), the solution (x = baaa, i = 3) would be sound: x[1..2] = ba ̸∈ L(⋆aa⋆) and x[3..4] = aa ∈ L(aa⋆). But it must be match(baaa, aa) = 2.

PROPMATCH

Let us now describe with pseudo-code our propagator. The function PROPMATCH described by Algorithm 1 propagates i = match(x, ρ). It is called after the constraint is posted and anytime the domain of x or i gets updated. It takes as input the variables x and i, the automata R = DFA(⋆ρ⋆) and S = DFA(ρ⋆), and the minimal length r = minlen(ρ) of a word of L(ρ), computed with a breadth-first search over the states of DFA(ρ). It returns a pair (X, I) of possibly refined domains for x and i, i.e., γ(X) ⊆ D(x) and I ⊆ D(i).

At line 2 we initialize X and I with the domains of x and i, respectively. At line 3 we possibly refine the upper bound of I, which cannot be bigger than the length of the longest string of γ(X) minus the length of the shortest string accepted by ρ plus one (we recall that, in our notation, the i-th leftmost character of a string has index i). The function CHECK (A) throws a failure if A = ∅, otherwise A is returned. The 'if' statement at line 4 handles a particular case: if i is fixed and its value is at most 1, then we can safely rewrite match into a single regular constraint.

The while loop starting at line 12 calls CHECKBLOCK (explained below) on the blocks of X to get a pair (Qi, j), where Qi is the set of states reachable after consuming blocks X[1] · · ·X[i], and j is the offset within X[i] such that if Qi = {q0} then γ(X[..., (i, j)]) ∩ L(ρ) = ∅. Indeed, if

1 The reified version of regular is b ⇔ regular(x, R) where b is a Boolean variable. If b = false, this is equivalent to regular(x,R), where R is the complement of R.

Algorithm 1 PROPMATCH function.

1: function PROPMATCH(x, i, R = (Σ,Q, δ, q0, {qF}), S, r) 2: X ←D(x), I ←D(i) 3: I ← I ∩ CHECK (0..maxlen(X) - r + 1) 4: if I = {k} ∧ k ≤ 1 then ▷ i = 0 ∨ i = 1 5: if k = 0 then 6: REWRITE(¬regular(x, R)) ▷ x ̸∈ L(R) 7: else 8: REWRITE(regular(x, S)) ▷ x ∈ L(S) 9: return X, I 10: i ← h ← k ← 0, n← |X| 11: Q0 ← {q0} 12: while i < n ∧ qF ̸∈ Qi do 13: i ← i + 1 14: (Qi, j) ← CHECKBLOCK(X[i], Qi-1, R) 15: if Qi = {q0} then 16: (h, k) ← (i, j) 17: if qF ̸∈ Qi then ▷ No match 18: I ← CHECK (I ∩ {0}) 19: return X, I 20: if Qi = {qF } then ▷ Surely a match 21: I ← CHECK (I ∩ 1.. max(I)) 22: if i < n then 23: I ← CHECK �I ∩ 1.. ∑ij=1 uj - r + 1� 24: ℓ ← ∑h-1 j=1 lj +k +1 25: if 0 ∈ I then 26: return X, {0} ∪ (I ∩ ℓ.. max(I)) 27: if ℓ < min(I) then 28: h ← 1, k ← min(I) - 1 ▷ Update (h, k) 29: while h ≤ n ∧ k ≥ uh do 30: (h, k) ← (h + 1, k - uh) 31: X′ ← PROPAGATE (¬regular(X[..., (h, k)], R)) 32: if |I| > 1 then 33: X′′ ← PROPAGATE (regular(X[(h, k), ...], R)) 34: else 35: I ← CHECK (I ∩ ℓ.. max(I)) 36: X′ ← X[..., (h, k)], X′′ ← X[(h, k), ...] 37: if |I| = 1 then 38: X′′ ← PROPAGATE (regular(X[(h, k), ...], S)) 39: X ← NORMALIZE(X′ · X′′ ) 40: return X, I ∩ CHECK (1..maxlen(X) - r + 1)

Qi = {q0} and (Qi, j) is returned by CHECKBLOCK, then ̂ δ(q0,w) = q0 for each w ∈ γ(X[..., (i, j)]). By Lemma 2, this means that no w ∈ γ(X[..., (i, j)]) can be in L(ρ). In other terms, if we feed R with any string w ∈ γ(X[..., (i, j)]) we always go back to the initial state. Position (h, k) is meant to be the leftmost position where ρ can match X, as anytime we find that Qi = {q0} at line 16 we update (h, k) with (i, j).

We exit the while loop if all the X-blocks are consumed, or the unique and universally accepting state qF (see Lemma 1) is reached. If qF is never reached, it must be match(x, ρ) = 0 (line 17). If instead Qi = {qF}, then surely match(x, ρ) ≥ 1 (line 20). In this case, we may also refine the upper bound of I because we know that w ∈ L(ρ) for each w ∈ γ(X[..., (i, ui)]), hence the match cannot happen after position ∑ij=1 uj -r+1 (line 23). Note that if qF is not the only reachable state we cannot refine the bounds of I: there may be no match.

A more general, and computationally expensive, way of refining the upper bound of I would be to reverse X and R to get X-1 = X[n] · · · X[1] and the non-deterministic automaton R-1 = (Σ,Q, {qF}, {(q′ , c, q) | (q, c, q′ ) ∈ δ}, {q0}) having qF as initial state and q0 as the only final state. In this way, by running the propagator in reverse, we can find the rightmost position where ρ can match x and therefore an upper bound for I. However, the benefits of this approach are overshadowed by its higher computational cost, and the fact that refining the upper bound of I is not that important as we are seeking the smallest index inMI(x, ρ).

In line 24 from (h, k) we get the leftmost position ℓ = ∑h-1 j=1 lj +k+1 where a match can occur. Then, if we cannot refine X because 0 ∈ I, we may still refine I by removing all the values in 1..ℓ - 1 (line 26). If ℓ < min(I) we cannot refine I (line 27) but we can impose that no match occurs before min(I) by considering the prefix region X[..., (h, k)]. The while loop at line 29 computes the rightmost position (h, k) such that |w| < min(I) for each w ∈ γ(X[..., (h, k)]). Then, we impose that no string of γ(X[..., (h, k)]) belongs to L(R) by applying a regular filtering algorithm returning a possibly refined prefix X′ (line 31). Here we deliberately allow flexibility about which regular algorithm to use, e.g., it may be the one defined in [Pesant, 2004], where D(x) is a fixed-size array of integer variables, or the one by [Amadini et al., 2018], where D(x) is a dashed string.

Similarly, at line 33 we may propagate regular over the suffix X′′ with R = DFA(⋆ρ⋆). This is sound, but only applied when I is not fixed (otherwise we can do better, as explained below) and ℓ < min(I), i.e., the lower bound of I is greater than the position of the leftmost possible match. In this case, it makes sense to look "to the right" of position min(I) to basically check for inconsistencies. Indeed, this propagation will hardly result in a refinement of X[(h, k), ...] because any character of Σ can occur in a string of L(R), which implies a likely weak propagation at the expense of a higher computational cost. This is why if ℓ ≥ min(I) we do not apply this reasoning: we already know that ρ can match x at position ℓ. In this case we possibly refine I (line 35) and we only use (h, k) as a pivot to split X into X′ and X′′ (line 36).

At line 38, we possibly perform a stronger suffix propagation by applying regular on L(S) = L(ρ⋆). But this is only sound when |I| = 1, i.e., i is fixed to a certain value. If instead |I| > 1, we cannot know at which position in I the match should happen, and therefore we cannot invoke regular on S. For example, if X = {a, b}0,5 , ρ = a and I = 3..5 then the leftmost position for a match is (1, 2). Propagating ¬regular(X[..., (1, 2)], ⋆a⋆) fixes prefix X′ to {b}2,2 . However, propagating regular(X[(1, 2), ...], a⋆) sets suffix X′′ to {a}1,1 {a, b}0,2 . This refines X to {b}2,2 {a}1,1 {a, b}0,2 , and so i must be 3, which is in general not sound as the leftmost occurrence of character a could also be at position 4 or 5 depending on the actual prefix of x.

At line 39 we concatenate the blocks of X′ and X′′ . If the last block of X′ and the first block of X′′ have the same base, or ∅0,0 occurs in X' or X′′ , then a normalization is performed via the NORMALIZE function. Finally, we return the possibly

Algorithm 2 CHECKBLOCK function.

1: function CHECKBLOCK(Sl,u , Qin, R = (Σ, Q, δ, q0, {qF })) 2: δS ← {q ↦→ {δ(q, a) | a ∈ S} | q ∈ Q} 3: Q0 ←Qin, j ← 0 4: for i ∈ 1, 2, . . . , l do ▷ Mandatory region 5: Qi ← ⋃q∈Qi-1 δS(q) 6: if Qi = {q0} then 7: j ← i ▷ All paths lead to q0 8: else if qF ∈ Qi then 9: return (Qi, j) ▷ Final state reached 10: if Qi = Qi-1 then 11: if Qi = {q0} then ▷ Fixpoint 12: return (Qi, l) 13: else 14: return (Qi, j) 15: dist ← §q ↦→ l if q ∈ Ql +∞ if q ∈ Q-Ql " 16: U ← QUEUE(Ql) ▷ U = queue of all the states in Ql 17: while U ̸= [ ] do 18: q ← POP(U) ▷ Breadth-first search. 19: d ← dist[q] + 1 20: if d ≤ u then 21: for q′ ∈ δS(q) where dist[q′ ] > d do 22: PUSH(U, q′ ) 23: dist[q′ ] = d 24: if qF ∈ δS(q) then ▷ Final state reached 25: break 26: return ({q ∈ Q | dist[q] ≤ u}, j)

refined domains.

CHECKBLOCK

The function CHECKBLOCK described by 2 is similar to the forward pass of the regular propagator described in [Amadini et al., 2018], because it explores the sets Qi of states reachable from Qin after consuming i characters of block Sl,u . However, here we are not interested in recording Q0, . . . ,Ql+1 for each block because no backward pass is needed, while in [Pesant, 2004; Amadini et al., 2018] the domains' refinement is performed "backwards" starting from a feasible set of reachable states. Moreover, here we stop as soon as a candidate match is found, i.e., qF ∈ Qi. Furthermore, CHECKBLOCK keeps track of the offset j within block Sl,u so that if Sl,u is the k-th block of dashed string X and ( , j) is returned, then no match can occur in X[..., (k, j)].

The function δS : Q → P(Q) at line 2 returns the set of states reachable from a given state after consuming any of the characters in S. We explore the reachable states Qi for each of the l mandatory characters of input block Sl,u , and we stop earlier when either the final state qF (line 9) or a fixpoint Qi (line 10) is reached. At each step, we update j with i if we find that Qi = {q0} (line 7), i.e., all the possible paths we get from a state of Qin by consuming i characters of S lead to q0. In this way, if Sl,u = X[k] and Qin is the set of states reachable after consuming the prefix X[..., (k, 0)], then by Lemma 2 no string of L(R) can match γ(X[..., (k, j)]).

The second part of CHECKBLOCK, from line 15, performs a breadth-first search over the optional part S0,u-l to possibly update the set of reachable states. If we reach the final state, we interrupt the search (line 24). The returned set will be the input set of states of CHECKBLOCK when called by PROPMATCH on the following block. To be sound, we can only update the offset j when considering the mandatory part of the block because, by definition, the optional part may not be present.

Example 1. Consider Σ = {a, b, c, d}, ρ = (ab|c), X = {d}2,3 {c}0,5 {a, b}3,5 and I = 10..100. Then, maxlen(X) = 3 + 5 + 5 = 13, R = DFA(⋆ρ⋆) as in Fig. 2, and r = minlen(R) = 1. Hence, I is refined into 10..13. The call of CHECKBLOCK on X[1] returns ({q0}, 2). The call on X[2] returns ({q0, q2}, 0). So, after the while loop of PROPMATCH we have (h, k) = (1, 2) and at line 24 we get ℓ = 3. Because ℓ < min(I) = 10 we update (h, k) to (3, 1) and propagate ¬regular({d}2,3 {c}0,5 {a, b}1,1 ,R) to get X′ = {d}2,3 {a, b}1,1 . Because |I| > 1, we also propagate regular(X[(3, 1), ...],R), but in this case the propagation has no effect so X′′ will be X[(3, 1), ...] = {a, b}2,4 .

We cannot further refine the suffix, so X becomes NORMALIZE({d}2,3 {a, b}1,1 {a, b}2,4 ) = {d}2,3 {a, b}3,5 . Now, maxlen(X) = 8, hence CHECK (10..8-1+1) = CHECK (∅) will throw a failure before returning.

Example 2. Let Σ and ρ as in Example 1, I = 0..10, and X = {b, d}2,5 {a, c}0,3 . Then I is refined into 0..8. The call of CHECKBLOCK on X[1] returns ({q0}, 2) so (h, k) = (1, 2). The call on X[2] returns ({q1, q2}, 0) so (h, k) is not updated. So again ℓ = 3, but in this case we cannot refine X because 0 ∈ I. However, we can refine I into {0} ∪ 3..8.

Example 3. Let Σ, ρ and X as in Example 2, and I = {3}. As above, (h, k) = (2, 1) and ℓ = 3. But this time ℓ = min(I), so we do not update (h, k) and we split X into X′ = {b, d}2,2 and X′′ = {b, d}0,3 {a, c}0,3 . Finally, |I| = 1 so we can safely propagate regular(X[(2, 1), ...], (ab|c)⋆) to refine X′′ into {c}1,1 {a, c}0,2 . Then, we update X to {b, d}2,2 {c}1,1 {a, c}0,2 .

3.2 Complexity and Consistency

Let us analyze the worst case complexity of PROPMATCH. The cost of the first part of the algorithm (lines 1-26) is dominated by the while loop at line 12, which calls CHECKBLOCK at most n = |X| times. Each call to CHECKBLOCK considers each transition of δ at most l + 1 times (one for each of the l mandatory characters of block Sl,u , plus one for the BFS over the optional part of Sl,u ). So, the worst case time complexity of CHECKBLOCK is O((l+1)×|δ|). If X = Sl1,u1 1 · · · Sln,un n the overall complexity of the first part of PROPMATCH is therefore O(∑ni=1 li × |δ|), which depends on the characters that must occur (the mandatory part of each block) but not on those that may occur (the optional part).

The complexity of the second part of PROPMATCH (from line 27) depends on the regular propagator adopted, which is called at most twice. It is however reasonable to assume that regular complexity is also bounded by O(∑ni=1 li × |δ|), as in [Amadini et al., 2018].

Unfortunately, we can say very little about the consistency notions ensured by the propagator. This is because, in general, dashed strings cannot guarantee a unique best representation of a set of strings (see the example in Sect. 2). Hence, it is infeasible to maintain consistency notions such as, e.g. the generalized arc-consistency.

4 Validation

We implemented our match propagator in G-STRINGS, a string solver based on CP solver GECODE [Gecode Team, 2023]. We compare its performance against the approach using decomposition (1), which we will call G-STRINGSdec. We also include in the evaluation the state-of-the-art SMT solvers CVC5 [Barbosa et al., 2022] and Z3 [de Moura and Bjørner, 2008]. Although these solvers support the theory of strings, they do not natively support the match constraint, so we had to use some workarounds.

4.1 Latin Square

We first compared the above approaches on a "stringy" version of the latin square problem: given n > 1, generate a n × n latin square over alphabet {a1, . . . , an} using string variables only. We use 2n string variables: r1, . . . , rn for the rows and c1, . . . , cn for the columns, and we impose for k = 1, . . . , n that:

• |rk| = |ck| = n and rk, ck ∈ L(a1| . . . |an)∗
• match(ri, ak) > 0 for i = 1, . . . , n
• match(cj , ak) > 0 for j = 1, . . . , n
• match(ri, ak) = j ⇔ match(cj, ak) = i for i, j = 1, . . . , n

We encoded the problem in MiniZinc [Nethercote et al., 2007] for G-STRINGS and G-STRINGSdec, while for SMT solvers we used the SMT-LIB [Barrett et al., 2010] language. For SMT solvers, we replaced each match constraint with a corresponding str.indexof function, returning the first occurrence of a pattern string in a target string (we can soundly use str.indexof because in this case the patterns are always fixed strings a1, . . . , ak of length 1). 1

Fig. 3 shows the runtimes in seconds for n = 2, 3, . . . , 26. Z3 is not included because it could not find any solution. CVC5 can only solve small size instances (n ≤ 8). As n gets bigger the performance of G-STRINGSdec clearly deteriorates: for n ≥ 20 it cannot solve the problem within the

1 We used CVC5 1.0.2 and Z3 4.11.2 with Z3str3 string solver (we also tried Z3seq, which did not improve Z3's performance). We run all the experiments on a Ubuntu 22.04 machine with 8 GB of RAM and 1.60 GHz Intel i5 CPU, with a timeout of 300s. We will disclose the source code in case of acceptance of the paper.

300s timeout (note that we are not charging for the flattening time into FlatZinc). Conversely, G-STRINGS equipped with match propagator can solve all the problems within 32s.

4.2 Shortest Matching Superstring

The second problem we consider is the shortest matching superstring: given patterns ρ1, . . . , ρn, the goal is to find the shortest string matched by all patterns, i.e., a minimal-length string x such that match(x, ρi) > 0 for i = 1, . . . , n. For the SMT solvers, instead of match we used the regular expression membership function str.in re applied to each wrapped pattern ⋆ρi⋆ for i = 1, . . . , n.

We generated 16 sets Sl,n of patterns for n ∈ {32, 64, 128, 256} and l ∈ {5, 10, 15, 20}. Each Sl,n contains n random patterns such that there exists a string of length l matched by all patterns (but there could be a shorter one). So, l is an upper bound on the length of the shortest string matched by all patterns. We use this information to provide an initial bound for each problem.

The results are shown in Tab. 1, showing for each solver the percentage of problems: solved to optimality (opt), where a solution was found (sat), no solution was found (unk). Then it reports the average time to first solution (ttf) when one is found, and solve time (which equals the time limit for unknown cases). Last two columns are comparative scores: score gives 0 for finding no solution, 0.25 for finding the worst known solution, 0.75 for finding the best known solution, a linear scale value in (0.25, 0.75) for finding other solutions, and 1 for proving the optimal solution. borda is the MiniZinc Challenge score [Stuckey et al., 2014], which gives a Borda score where each pair of solvers is compared on each instance, the better solver gets 1, the weaker 0, and if they are tied the point is split inversely proportional to their solving time.

SMT solvers perform better on this problem, but GSTRINGS still achieves the best results. It is the quickest to find solutions and the most robust overall, always finding a solution and proving optimality more often than other approaches. The score shows that its solutions are significantly better than other approaches, while borda shows that CVC5 is effectibely dominated by the other approaches. It is important to note the performance difference between G-STRINGS with G-STRINGSdec, which is not in Tab. 1 because it could not find any solution. This witnesses the scalability issues of the decomposition approach, and hence the importance of having a specialized match propagator.

5 Conclusions

We introduce a propagation algorithm for the constraint match(x, ρ), returning the position in x of the leftmost possible match of a string belonging to the language denoted by the regular pattern ρ. This generalizes existing propagators and decision procedures for the regular constraint, which only enforce the membership of a string variable to the language denoted by a regular pattern. We provided empirical evidence demonstrating the benefits of a specialized propagator for match, in contrast to a less efficient rewriting of this constraint in terms of regular.

Possible future directions include the extension of the replace constraint where the string to be replaced is defined by a regular pattern instead of a string variable, and other harder constraints such as, e.g., finding and replacing all the occurrences or considering non-regular patterns such as backreferences.

Acknowledgments

Research partly funded by PNRR - M4C2 - Investimento 1.3, Partenariato Esteso PE00000013 - "FAIR - Future Artificial Intelligence Research" - Spoke 1 "Human-centered AI", funded by the European Commission under the NextGeneration EU programme. This research was partially funded by the Australian Government through the Australian Research Council Industrial Transformation Training Centre in Optimisation Technologies, Integrated Methodologies, and Applications (OPTIMA), Project ID IC200100009.