A Constraint Solving Approach to Parikh Images of Regular
Languages
AMANDA STJERNA, Uppsala University, Sweden
PHILIPP RÜMMER, University of Regensburg, Germany and Uppsala University, Sweden
A common problem in string constraint solvers is computing the Parikh image, a linear arithmetic formula that
describes all possible combinations of character counts in strings of a given language. Automata-based string
solvers frequently need to compute the Parikh image of products (or intersections) of ﬁnite-state automata,in particular when solving string constraints that also include the integer data-type due to operations likestring length and indexing. In this context, the computation of Parikh images often turns out to be bothprohibitively slow and memory-intensive. This paper contributes a new understanding of how the reasoning
about Parikh images can be cast as a constraint solving problem, and questions about Parikh images beanswered without explicitly computing the product automaton or the exact Parikh image. The paper shows
how this formulation can be eﬃciently implemented as a calculus, PC*, embedded in an automated theorem
prover supporting Presburger logic. The resulting standalone tool Catra is evaluate on constraints produced by
the Ostrich+ string solver when solving standard string constraint benchmarks involving integer operations.
The experiments show that PC* strictly outperforms the standard approach by Verma et al. to extract Parikh
images from ﬁnite-state automata, as well as the over-approximating method recently described by Janků andTuroňová by a wide margin, and for realistic timeouts (under 60 s) also the nuXmv model checker. When added
as the Parikh image backend of Ostrich+ to the Ostrich string constraint solver’s portfolio, it boosts its
results on the quantiﬁer-free strings with linear integer algebra track of SMT-COMP 2023 (QF_SLIA) enoughto solve the most Unsat instances in that track of all competitors.
CCS Concepts: • Theory of computation → Quantitative automata; Regular languages; Automatedreasoning; Program veriﬁcation; Veriﬁcation by model checking.
Additional Key Words and Phrases: Parikh images, string solvers, model checking
ACM Reference Format:
Amanda Stjerna and Philipp Rümmer. 2024. A Constraint Solving Approach to Parikh Images of Regular
Languages. Proc. ACM Program. Lang. 8, OOPSLA1, Article 138 (April 2024), 29 pages. https://doi.org/10.1145/
3649855

1 INTRODUCTION
Extending automated theorem provers and SMT solvers with support for rich string constraints
is important for program analysis, particularly to detect cross-site scripting vulnerabilities andother string manipulation bugs [Bultan et al. 2017]. To check the satisﬁability of a formula like𝑥 ∈ L 1 ∧𝑦 ∈ L 2 ∧|𝑥 | > |𝑦|, with string variables 𝑥, 𝑦 and regular languages L 1, L 2 , it is necessary
to reason about the possible lengths of 𝑥, 𝑦 that are admitted by L 1, L 2 , respectively. The set ofword lengths {|𝑤 | | 𝑤 ∈ L} in a language L is a special case of the Parikh image of a regular
Authors’ addresses: Amanda Stjerna, Department of Information Technology, Uppsala University, Lägerhyddsvägen 1,
hus 10, Uppsala, Sweden, amanda.stjerna@it.uu.se; Philipp Rümmer, Faculty of Informatics and Data Science, Universityof Regensburg, Bajuwarenstraße 4, Regensburg, 93053, Germany, philipp.ruemmer@ur.de, Department of Information
Technology and Uppsala University, Lägerhyddsvägen 1, hus 10, Uppsala, Sweden, philipp.ruemmer@it.uu.se.

This work is licensed under a Creative Commons Attribution 4.0 International License.
© 2024 Copyright held by the owner/author(s).
ACM 2475-1421/2024/4-ART138
https://doi.org/10.1145/3649855
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

138:2

Amanda Stjerna and Philipp Rümmer

language. This required combined reasoning about strings and string length has long been identiﬁed
as a major bottleneck in string solvers [Abdulla et al. 2015; Berzish et al. 2017, 2021; Janků andTuroňová 2020]. Other string solvers make use of Parikh automata [Klaedtke and Rueß 2002], andthus Parikh images in the general case, to handle operations that combine strings and integers(including str.substr and str.at), which comes at an even higher price in terms of computational
complexity [Chen et al. 2020].
The Parikh image, more broadly, is a characterisation of formal languages in terms of theircharacter counts. Given a language L over an alphabet {𝑎 1, . . . , 𝑎𝑘 }, the Parikh image is a setof 𝑘-dimensional vectors that contains some vector [𝑚 1, . . . , 𝑚𝑘 ] if and only if the language L
contains a word in which each 𝑎𝑖 occurs 𝑚𝑖 times. It is a classical result that the Parikh imageof every context-free language (and, thus, also of every regular language) is a semilinear set, i.e.,
Presburger-deﬁnable [Parikh 1966]. In fact, it is possible to compute an existential Presburger
arithmetic formula describing the Parikh image of any context-free language in linear time [Vermaet al. 2005] in the size of the grammar describing the language. For the special case of regular
languages, this result was also stated in [Seidl et al. 2004].
In applications, it is often necessary to consider the Parikh image not only of a single regular
language, but of the intersection of multiple languages. This happens in string solvers in particular,
as conjunctions of string constraints lead to the computation of length images of intersectionsof regular languages represented as ﬁnite-state automata. On the other hand, we are often notinterested in a closed-form description of the complete Parikh image, but rather in checking whether
the Parikh image contains vectors satisfying some given properties. The main problem considered inthis paper is the following:
Joint satisﬁability of Parikh images modulo Presburger arithmetic constraints
Given regular languages L 1, . . . , L𝑛 over a common alphabet {𝑎 1, . . . , 𝑎𝑘 }, anda Presburger arithmetic formula 𝜙 (𝑥 1, . . . , 𝑥𝑘 ), decide if there is a word 𝑤 ∈L 1 ∩ · · · ∩ L𝑛 whose Parikh vector [𝑚 1, . . . , 𝑚𝑘 ] satisﬁes 𝜙.
The problem can be solved using the classical construction of Parikh images [Seidl et al. 2004;
Verma et al. 2005] by ﬁrst computing the product of ﬁnite-state automata accepting the languages L 1, . . . , L𝑛 , then extracting a Presburger arithmetic formula 𝜌 describing the Parikh imageof the product automaton, and ﬁnally checking the satisﬁability of 𝜙 ∧ 𝜌.
While theoretically elegant, this construction has several disadvantages that easily turn into
bottlenecks when reasoning about Parikh images in algorithms or applications.
Firstly, computing the product automaton is often prohibitively expensive in both memory andCPU time. In several instances we have observed while solving real-world string constraints, thecomputation of the product of automata exhausts the memory of any machine available due tothe exponential blow-up in size of the product, quickly becoming intractable as the number of
automata in the product increases.
Secondly, the constructed Presburger arithmetic formula 𝜌 contains a linear number of existential
quantiﬁers in the size of the product automaton, as well as complex Boolean structure, which isneeded to express the connectedness of paths considered in the construction. Solving formulas ofthis kind generally tends to be taxing for solvers [Chen et al. 2020]; in the present case, since theproduct automaton itself is exponentially big, also formula 𝜌 has exponential size in the number ofconsidered regular languages, and can easily become too complex for today’s Presburger arithmetic
solvers to handle.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

A Constraint Solving Approach to Parikh Images of Regular Languages

138:3

The current best published mitigation for this problem relies on the observation that the Parikh
image of an intersection of languages can be over-approximated by the conjunction of the Parikh
images of the individual languages. Such over-approximation can be used to derive that no word
exists whose Parikh vector satisﬁes a formula 𝜙, falling back to computing the intersection of thelanguages (or of some subset of the languages) for the satisﬁable cases [Janků and Turoňová 2020].
Addressing these concerns, we have developed a calculus for Parikh images of intersections ofregular languages that we call PC*. It allows us to interleave the computation of product automata
with the derivation of the Parikh image. This enables the two calculations to inform each other,eliminating unnecessary work, and pruning the size of the partial products considered in thecomputation for a smaller memory footprint. Moreover, our approach allows us to do this precisely,
without the expensive fallbacks when approximations fail as in the case of [Janků and Turoňová
2020]. Our calculus is applicable not only to Parikh images, but can be used for reasoning about theimage of regular languages under arbitrary homomorphisms into commutative monoids. Besides
Parikh images, this includes the length abstraction of regular languages commonly used in string
solvers.
Our primary inﬂuence for this work is the operation of (ﬁnite-domain) constraint programming(CP) solvers [Marriott and Stuckey 1998]. CP solvers typically employ a combination of lazy
enforcement of constraints through propagation, pruning values from decision variable domainsthat do not satisfy the constraints during solving, and branching, splitting proofs by cases in a waythat will encourage maximum propagation.
For our problem, the constraints are automata connectivity and linear equations (Presburger
arithmetic formulas). We use propagation to lazily enforce connectivity of automata, removing
transitions as they become unreachable during solving or are eliminated by constraints in the
Presburger formula. We also branch on the presence or absence of transitions to encourage propagation of the connectivity constraint. This allows us to whittle down the automata (includingintermittent products) before moving on with potentially explosive product construction. The
underlying observation is that though the domain of our integer variables is inﬁnite, the number ofsimple paths through the automata (and their product) is ﬁnite. In summary, the key ideas are:
Key paradigms in PC*• Enforce automata connectivity constraints lazily;• Use propagation of constraints on the Parikh image to prune transitions
from the automata that are incompatible with constraints;• Intelligently branch on the presence or absence of key transitions to drive
propagation of the connectivity constraint;• Compute products of automata lazily, after pruning transitions that violate
constraints using propagation.
We implement PC* as a plug-in theory for the Princess automated theorem prover [Rümmer
2008], and additionally wrap the Parikh image solver as a stand-alone tool, Catra. Catra also
supports a variant of the approximate method of [Janků and Turoňová 2020], its fall-back variant
adapted from [Verma et al. 2005], and an adapter for the nuXmv model checker [Cavada et al.
2014]. Using Catra, we compare PC* to the other back-ends on 37 497 distinct Parikh automata
intersection problems generated by Ostrich+ when solving the PyEx string constraint benchmark
suite involving string length constraints [Reynolds et al. 2017], ﬁnding that PC* outperforms bothnuXmv and the baseline method, allowing PC* to solve every problem solved by baseline within 30 s
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

138:4

Amanda Stjerna and Philipp Rümmer

in under 5 s. PC* in particular outperforms nuXmv on unsatisﬁable instances, more than doubling
the number of unsatisﬁable results found within a 30 s timeout.
We also extend the Ostrich string solver [Chen et al. 2019] with a new back-end based on Catraas the Parikh image intersection solver of the Ostrich+ algorithm, obtaining improvements inboth Sat and Unsat performance in Ostrich’ results from SMT-COMP 2023, crucially allowing
Ostrich to win the unsatisﬁable category of the track of quantiﬁer-free, linear constraints overstring logic (QF_SLIA) and increasing the number of Sat results by 3% on the same track.
In summary, we contribute:• The PC* calculus to eﬃciently check the satisﬁability of the Parikh image of an intersectionof regular languages modulo Presburger arithmetic side conditions.
• Techniques to eﬃciently implement PC* in a modern automated theorem prover, including
strategies for case splitting, clause learning, and constraint propagation for connectedness.
• The Catra tool for solving such instances, containing an implementation of PC*, the overapproximation described in [Janků and Turoňová 2020], and an adapter for the nuXmv model
checker [Cavada et al. 2014].
• Experiments illustrating the performance of PC* on real-world examples from string solving,
including 37 497 instances in a standardised format made available for future study.
1.1 Related Work
The problem of satisfying Parikh images over products of regular languages, modulo Presburger
arithmetic side conditions, amounts to checking emptiness of products of Parikh automata. Parikh
automata are regular automata extended with integer counters with given increments and decrements for each transition, where we allow checking a set of linear constraints on the ﬁnal values of
the counters (but not their intermittent values) [Klaedtke and Rueß 2002]. Parikh automata without
constraints on the ﬁnal values on their registers are also sometimes called cost-enriched automata,weighted automata, or counter automata, depending on exact deﬁnitions and side constraints. The
decision problem tackled in this paper, determining the emptiness of an intersection of Parikh
automata, was shown to be PSPACE-complete [Figueira and Libkin 2015].
Parikh image computations, as well as Parikh automata, feature extensively in string solvers,
including as mentioned above Ostrich and Ostrich+ [Chen et al. 2020, 2019], but also forms
the basis of Trau [Abdulla et al. 2017], and occurs in Sloth [Holík et al. 2017]. Parikh images
frequently appear when introducing cardinality constraints like length or string indexing. While
relying on Parikh images (or on being able to check the emptiness of Parikh images under givenside constraints), the mentioned papers do not propose any techniques to compute Parikh images.
Seidl et al. and Verma et al. deﬁne a closed-form description of the Parikh image of any regular
language as an existential Presburger arithmetic formula. An approach to optimise the construction
is to over-approximate the Parikh image of a product of 𝑘 automata 𝜓 (L (A1 ) ∩ . . . ∩ L (A𝑘 ))Ówith the conjunction of the Parikh images, 𝑘𝑖=1 𝜓 (L (A𝑖 )) [Janků and Turoňová 2020]. Due tothe over-approximation, this approach is primarily useful for unsatisﬁable instances, and requires
falling back to computing the product of the automata before using the standard approach forﬁnding its image originally presented in [Verma et al. 2005]. Our calculus PC*, in a somewhat
similar but more ﬁne-grained manner, utilises laziness to postpone or avoid the most expensive
steps in the computation of Parikh images of the intersection of regular languages.
Our calculus PC* is also similar in spirit to the work of Stanford et al., who tackle the exponential
blow-up resulting from Boolean combinations of ﬁnite-state automata in SMT string solvers
through the use of symbolic derivatives [Stanford et al. 2021]. The research by Stanford et al. does
not consider Parikh images, however. In addition to presenting a decision procedure for lazily
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

A Constraint Solving Approach to Parikh Images of Regular Languages

138:5

dispatching constraints, we similarly also allow for symbolic labelling of automata to handle largealphabets.
Beyond the ﬁeld of string solving, Parikh image computation is used as an elementary building
block in a variety of areas. For instance, Parikh automata have been proposed as the basis of queries
in graph databases [Figueira and Libkin 2015]; Parikh images are used for handling cardinalities
in parameterised model checking for epistemic logic [Stan and Lin 2021]; or for handling summation constraints in expressive array logics [Raya 2023]. Our calculus PC*, and the stand-alone
solver Catra, are potentially useful in all such applications.
Other generalisations of the Parikh image than the projections we use here have been studied.
Prominent examples include generalising the Parikh map to segments of a ﬁxed length [Karhumäki
1980] and the more general Parikh matrix, which contains not only the Parikh vector, but also
information about the order of letters. Another notable generalisation is the p-vector, introduced
in [Siromoney and Rajkumar Dare 1985], which denotes the position of each letter in the wordrather than the number of their occurrences and allows for generalisations into inﬁnite alphabets.
All of these in some sense extend the Parikh map. By contrast, the main utility of the formulation
introduced here is to reason about Parikh images lazily, thereby potentially obtaining answers
more quickly. We expect that our calculus PC* can be generalised to the mentioned functions onformal languages as well, but leave such investigations to future work.
2 AN INTUITION FOR OUR APPROACH
In this section, we will introduce an intuition for how a string constraint problem in an automatabased solver like Ostrich+ is translated to a Parikh automata intersection problem, and solved
using PC*.
We use PCRE regular expression notation here and throughout the paper, writing them like this.
This means that | is alternation, ∗ the Kleene star, and . matches any single character. For the lengthof a string 𝑠, we write |𝑠 |. All number variables in this example are in N with 0.
Example 2.1. Consider the following set of string constraints over string variables 𝑠 1, 𝑠 2 andinteger variables 𝑛, 𝑖:(i): 𝑠 1 ∈ L (c|dd).
(ii): 𝑠 2 ∈ L (B), the language accepted by automaton B of Fig. 1b (ignoring the registers 𝑙𝐵 ).
(iii): 𝑠 1 = substring(𝑠 2, 𝑖, 𝑛), that is 𝑠 1 is an 𝑛-length substring of 𝑠 2 starting at oﬀset 𝑖.
(iv): 𝑛 > 𝑖, that is what comes before 𝑠 1 in 𝑠 2 is shorter than 𝑠 1 .
(v): 𝑖 > 0 ∧ |𝑠 2 | − 𝑖 − 𝑛 > 0, that is there is at least one character in 𝑠 2 before and after 𝑠 1 .
Although the constraints are simple, it should be noted that decidability results for string
constraints involving integers are notoriously hard to obtain; many state-of-the-art string solvers,
for instance Z3 [de Moura and Bjørner 2008], diﬀerent versions of Z3-str [Mora et al. 2021; Zheng
et al. 2013], or cvc5 [Barbosa et al. 2022] are not guaranteed to be complete or to terminate on such
constraints (but, of course, they often achieve very good performance in practice).
A decision procedure for a fragment of string constraints with integers, covering our constraints
is deﬁned in [Chen et al. 2020]. We will ﬁrst perform translation into Parikh automata, then break
down how the constraints will be handled by PC*. This example will recur in a more formal fashion
in Section 4, which can be read in parallel if (even) more detail is desired.
2.1

Translating the Constraints into a Parikh Automata Intersection Problem

By a Parikh automaton we mean a standard non-deterministic ﬁnite automaton (NFA) with a setof integer registers (Parikh registers) that are incremented (or decremented) at each transition. A
formal deﬁnition can be found in Deﬁnition 4.1.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

138:6

Amanda Stjerna and Philipp RümmerΣ/ lA+

Σ/ lA+ i+IA
c/ lA+ n+
d/ lA+ n+FA
d/ lA+ n+D(a) The automaton 𝐴′ , whose Parikh registers count the length of the string acceptedby the automaton (register 𝑙𝐴 ), the start oﬀset of the substring (𝑖) and length (𝑛) of thesubstring matching c|dd. Note the symbolic transitions in the starting and accepting
states matching any symbol in the alphabet!


c/ lB+IB
a/ lB+A
a/ lB+


b/ lB+


c/ lB+


c/ lB+


b/ lB+B

FB(b) The automaton 𝐵, where the Parikh registers count the length of thestring in register 𝑙𝐵 .
Fig. 1. The collection of automata we use as running examples, both derived from Example 2.1.

To solve Example 2.1 using PC* in a theorem proving context, Constraint (i) to Constraint (iii)
can be translated to the product of Parikh automata B × A ′ . Automaton B is given in Fig. 1b.
Automaton A ′ (Fig. 1a) is an automaton deﬁning the pre-image of L (c|dd) under the substring
function, and obtained by applying the construction described in [Chen et al. 2020]. Intuitively, A ′describes all tuples (𝑠 2, 𝑖, 𝑛) such that substring(𝑠 2, 𝑖, 𝑛) is in L (c|dd). To this end, A ′ contains
registers 𝑙𝐴 , 𝑖, 𝑛, which counts the length of the overall string read, the length of the preﬁx before
the extracted substring, and the length of the substring, respectively. Registers are assumed to startfrom zero in each automaton run.
 
In the automata of Fig. 1, we use the notation 𝑎/ 𝑥 + to mean that a transition reads an input
character 𝑎 and increments register 𝑥 by one. We will omit zero-valued increments and assume
that all registers are scoped to their automaton. The increments are usually represented
  as a vector(hence the brackets), but as it is mostly sparse here, we use the symbolic notation 𝑥 1+ rather thanthe more cumbersome [0, 1, 0, . . . , 0].
Note that the labels of transitions can be ranges of characters with Σ representing any characterin the alphabet.
Intuitively, Example 2.1 is unsatisﬁable. By inspecting the automata, we realise that the pathusing dd in A ′ is unusable since are no d-labelled transitions in B. This means that 𝑠 1 = c, and thus𝑛 = 1. That means that Constraint (iv) implies that 𝑖 = 0. However, no path through 𝐵 passes by a c
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

A Constraint Solving Approach to Parikh Images of Regular Languages

138:7

without a preceding character. Therefore, already Constraint (i), Constraint (iii) and Constraint (iv)
together are unsatisﬁable.
An eager approach to ﬁnding the Parikh image, as described in [Verma et al. 2005], would
start by computing the product A ′ × B, translating it to a Presburger formula with 𝑖, 𝑛, etc., as
free variables, and then adding Constraint (iv) and Constraint (v) to the resulting set of linear
inequalitites. Scalability of this construction is limited due to the size of the product automata to becomputed, and the complexity of the resulting Presburger formula.
2.2 Solving the Parikh Automata Intersection Problem Using PC*
We will now proceed to show how our calculus PC* can lazily prove the unsatisﬁability of therunning example. The calculus interleaves several reasoning principles, which we will later deﬁne
precisely as calculus rules: (i) Similarly, as in [Verma et al. 2005], we ﬁrst describe each automaton
as a ﬂow network, counting how often each transition is taken in a run of the automaton. The ﬂow
constraints are an over-approximation of the possible accepting runs of an automaton. (ii) We use
a linear integer solver to simplify the ﬂow constraints and prune away paths through the automata
that are not feasible. (iii) We use a tailor-made propagation algorithm to identify disconnectedtransitions of the automata that can never be taken and lazily add the corresponding constraints.
(iv) When propagation cannot infer further constraints, we use case splitting to subdivide theproblem into smaller parts. (v) Once the constituent automata of a product have become suﬃciently
small, we compute the precise product automaton.
2.2.1 Approximating Paths Through Automata Using Flow Analysis. We associate each transition 𝑡of A ′ and B with a fresh variable 𝑥𝑡 ranging over natural numbers (i.e., non-negative integers).
These variables represent how many times each transition is taken. Hence, the ﬁnal value forregisters 𝑟 1, . . . , 𝑟𝑘 of each automaton is the element-wise sum:𝑟 1   Õ
 .. 
𝑥𝑡 · 𝐾¯𝑡 where 𝐾¯𝑡 are the increments of transition 𝑡 .
(1)
.=
 
𝑡
𝑟𝑘 
 
We proceed by adding linear constraints requiring transition variables to represent a ﬂow throughtheir automaton by adding linear constraints stating that the number of incoming transitions isequal to the number of outgoing ones. E.g., state 𝐵 of automaton B would have the sum𝑥 ⟨𝐵,c,𝐵⟩𝑥 ⟨𝐵,c,𝐵⟩(2)✘✘ + 𝑥 ⟨𝐼𝐵 ,b,𝐵⟩ = ✘✘✘ + 𝑥 ⟨𝐵,c,𝐹𝐵 ⟩ + 𝑥 ⟨𝐵,b,𝐼𝐵 ⟩✘where we let 𝑥 ⟨𝑞,𝑙,𝑞 ′ ⟩ refer to the integer variable associated with a transition from state 𝑞 to state 𝑞 ′with label 𝑙. The initial state of the automaton receives an additional inﬂow of 1, and accepting states
have an additional common outﬂow of 1. Note that self-loops cancels themselves out. Therefore,
when a loop can become unreachable, additional constraints are required to ensure consistency.
2.2.2 Arithmetic Flow Simplification. We then use linear arithmetic reasoning on the register
equations (1) and ﬂow equations (2) to simplify the counters associated with transitions. As an
example, we start with A ′ . Substituting back solutions to the equations for A ′ to the automaton,
we obtain the automaton in Fig. 2, where the notation 𝑎/𝑡 now denotes a transition that accepts
letter 𝑎 and is taken 𝑡 times. In this case, the transitions of the automaton can be speciﬁed purely interms of the free variables we care about representing: the length of the accepted word (𝑙𝐴 ), thestart of the substring (𝑖), and the length of the substring (𝑛).
Having obtained this representation, we conclude that 1 < 𝑛 ≤ 2 from Constraint (iv) and Constraint (v). The lower bound directly follows from Constraint (iv) and Constraint (v), whereas theupper bound is obtained by the following reasoning. Since all transition variables are non-negative
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

138:8

Amanda Stjerna and Philipp Rümmer

Σ/lA − i − n

Σ/i
1

D

d/n − 1d/n − 1c/2 − nIA

FA

Fig. 2. A ′ after even more simplification using linear algebra, with most transitions expressed in terms of 𝑛.
Intuitively, this version captures the fact that 𝑛 is given by distributing the incoming flow of 1 across the twooutgoing transitions from 𝐼𝐴′ , the initial state.

Σ/lA − 3

Σ/1

D

d/1

d/1

c/0

IA

FA

(a) A ′ with its associated transition variables in symbolic form.

c/lA − x9 − 2x11 − 2x12
a/x11

IB

A

a/x11

b/x12

c/x9

c/1 − x11

b/x11 + x12 − 1BFB(b) B with its associated transition variables in symbolic forms. The large number of
implicitly existentially quantified variables 𝑥𝑖 on transitions suggest that this automaton
has a more complex structure with relation to its (free) target variable representing thestring length than A ′ .
Fig. 3. The automata after arithmetic simplification.

integers (a transition cannot be used a negative amount of times), 𝑛 ≤ 2 from the 𝐼𝐴 to 𝐹𝐴 transition.
Therefore, it follows that 𝑛 = 2, which implies that the 𝐼𝐴 to 𝐹𝐴 transition can never be used underthese constraints and that we must use the two d-labelled transitions, both now taken 𝑛 − 1 = 1
times. Substituting the derived value of 𝑛 and applying similar reasoning to automaton B, we arriveat the simpliﬁed automata in Fig. 3.
Note that the per-automata length counting registers have been assigned the same solver variable 𝑙𝐴 . Since they have to be equal, either one can be used in both automata through similar
applications of equality elimination rules.
2.2.3 Case Splitting and Connectivity Propagation. We now have a choice of two paths throughautomaton B; the upper through state 𝐴 or the lower through state 𝐵. Since arithmetic reasoning
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

A Constraint Solving Approach to Parikh Images of Regular Languages

138:9

and propagation are not able to resolve this choice, we perform a case split by selecting a transition
variable that would disconnect some strongly connected component of automaton B, in this casethe transition from 𝐼𝐵 to state 𝐵 guarded by variable 𝑥 12 . We split the reasoning into the cases
𝑥 12 > 0 (transition used) and 𝑥 12 = 0 (transition unused). For presentation, we focus on the latter
case, as the former can be handled in a similar way.
In the case 𝑥 12 = 0, we can conclude that the state 𝐵 is now unreachable, which means that its
outgoing transitions are now unusable. Propagation can therefore infer the additional equations
𝑥 9 = 0 and 𝑥 11 = 1.
2.2.4 Computing Products. After discounting all transitions that can no longer be taken, we areleft with two (small) ﬂat automata, and can compute their product with relative ease. By putting oﬀ
computing the product B × A ′ until after performing linear reasoning, and using that to prunetransitions, we have computed a smaller product than we would have with an eager approach.
Computing the product, we will immediately notice that the d-labelled transition of automaton
A ′ has no correspondence in B, leading to an empty product. We can close the proof goal andbacktrack, and we will eventually derive that the imposed constraints are unsatisﬁable by repeating
the same process on the other branch.
3 PRELIMINARIES
We ﬁrst survey some of the required background on ﬁnite-state automata and the Parikh image. In
addition, we assume basic familiarity with ﬁrst-order logic, Presburger arithmetic, and the classicalsequent calculus; for reference, see e.g. [Fitting 1996].
3.1

Monoids

A monoid 𝑀 = ⟨𝑋 ; ⊕; 0𝑀 ⟩ is an algebraic structure consisting of the non-empty carrier set ofelements, 𝑋 ; an associative binary operation 𝑋 × 𝑋 → 𝑋 denoted as ⊕, that is where for all𝑎, 𝑏, 𝑐 ∈ 𝑋 , (𝑎 ⊕ 𝑏) ⊕ 𝑐 = 𝑎 ⊕(𝑏 ⊕ 𝑐); and an identity element 0𝑀 ∈ 𝑋 such that 0𝑀 ⊕ 𝑎 = 𝑎 ⊕ 0𝑀 = 𝑎
for every 𝑎 ∈ 𝑋 . We sometimes use integer multiplication to represent a repeated application of ⊕,e.g. 3𝑎 = 𝑎 ⊕ 𝑎 ⊕ 𝑎, for 𝑎 ∈ 𝑋 . 𝑀 is called commutative if ⊕ also commutes, that is if 𝑎 ⊕ 𝑏 = 𝑏 ⊕ 𝑎
for all 𝑎, 𝑏 ∈ 𝑋 .
A homomorphism is a structure-preserving map between two monoids 𝑀 = ⟨𝑋 ; ⊕; 0𝑀 ⟩ and𝑀 ′ = ⟨𝑋 ′ ; ⊕ ′ ; 0𝑀 ′ ⟩, that is a map ℎ : 𝑋 1 → 𝑋 2 such that ℎ(𝑎 ⊕ 𝑏) = ℎ(𝑎) ⊕ ′ ℎ(𝑏) and ℎ(0𝑀 ) = 0𝑀 ′ .
3.2

Languages, Finite-State Automata and Their Products

We deﬁne an alphabet as a ﬁnite set of symbols Σ with words Σ∗ , and the concatenation operation
as 𝑠 1 ◦ 𝑠 2 over two strings 𝑠 1, 𝑠 2 . Note that Σ∗ = ⟨Σ; ◦ ; 𝜖⟩, is a non-commutative monoid, referred toas the free monoid on Σ. The string length function, |𝑠 | is an example of a homomorphism betweenΣ∗ and Z.
A ﬁnite-state automaton A with alphabet Σ is a tuple ⟨𝑄, 𝑞𝐼 , 𝐹, 𝛿⟩, where 𝑄 is the set of states, 𝑞𝐼
the initial state, 𝐹 the set of accepting states, and 𝛿 ⊆ 𝑄 × Σ × 𝑄 the transition relation. We write𝑙a transition 𝑡 = ⟨𝑞, 𝑙, 𝑞 ′ ⟩ ∈ 𝛿 as 𝑡 = 𝑞 →− 𝑞 ′ . Similarly, we use the notation 𝑞 →− to refer to the setof transitions starting in 𝑞, and →− 𝑞 to refer to the set of transitions coming into 𝑞, whenever the
automaton is clear from the context.
We will let variables 𝑡, 𝑡 ′, 𝑡 1, . . . , 𝑡𝑛 , etc., denote transitions, 𝑞, . . . , 𝑞𝑛 states, and A, . . . , A𝑛 automata, and use subscript indexing (𝛿 A ) to refer to the transitions, states, etc., of a given automaton.
A path 𝑝 = ⟨𝑞 0𝑙 1𝑞 1 . . . 𝑞𝑛 ⟩ of an automaton A is a sequence of states 𝑞 0, . . . , 𝑞𝑛 interleaved with𝑙𝑖

letters 𝑙 1, . . . , 𝑙𝑛 such that 𝑞 0 = 𝑞𝐼 and 𝑞𝑖 −1 −→ 𝑞𝑖 for 𝑖 ∈ {1, . . . , 𝑛}. The path is accepting if the end
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

138:10

Amanda Stjerna and Philipp Rümmer

state is accepting, 𝑞𝑛 ∈ 𝐹 . The set of paths of A is denoted by Paths(A). Additionally, we use thenotation Paths(A, 𝑞) to mean all paths ending in state 𝑞. We write 𝑡 ∈ 𝑝 to express that transition 𝑡
occurs on path 𝑝. The states of a path 𝑝 = ⟨𝑞 0𝑙 1𝑞 1 . . . 𝑞𝑛 ⟩, denoted States(𝑝) = {𝑞 0, · · · , 𝑞𝑛 } are thestates visited along 𝑝. Note that 𝑞𝐼 ∈ States(𝑝) for every path since all paths start in the initial state.
The word of a path 𝑝 = ⟨𝑞 0𝑙 1𝑞 1 . . . 𝑞𝑛 ⟩ is the word 𝑤 (𝑝) = 𝑙 1 ◦ · · · ◦ 𝑙𝑛 ∈ Σ∗ formed by the labels on
the path. Finally, the set of words accepted by an automaton A, denoted by L (A) ⊆ Σ∗ , is the setof words of accepting paths.
The product of two automata A1 = 𝑄 1, 𝑞𝐼1, 𝐹 1, 𝛿 1 and A2 = 𝑄 2, 𝑞𝐼2, 𝐹 2, 𝛿 2 is the automaton
A1 × A2 = 𝑄 1 × 𝑄 2, ⟨𝑞𝐼1, 𝑞𝐼2 ⟩, 𝐹 1 × 𝐹 2, 𝛿with 𝛿 = {⟨⟨𝑞, 𝑞 ′′ ⟩, 𝑙, ⟨𝑞 ′, 𝑞 ′′′ ⟩⟩ | ⟨𝑞, 𝑙, 𝑞 ′ ⟩ ∈ 𝛿 1, ⟨𝑞 ′′, 𝑙, 𝑞 ′′′ ⟩ ∈ 𝛿 2 } .
The product automaton runs A1 and A2 in parallel on an input and only accepts the input if bothautomata would do so; we have L (A1 × A2 ) = L (A1 ) ∩ L (A2 ).
3.3 The Parikh Map and Its Image
Formally, the Parikh map over an alphabet Σ = {𝑎 1, . . . , 𝑎𝑘 } is deﬁned as in [Kozen 1997]:
𝜓 : Σ∗ → N𝑘
𝜓 (𝑠) = [#𝑎 1 (𝑠), #𝑎 2 (𝑠), . . . , #𝑎𝑘 (𝑠)]That is, 𝜓 (𝑠) is a vector of the number of occurrences of each character in the language for agiven string 𝑠. For example, for Σ = {𝑎, 𝑏}, we would have 𝜓 (𝑎𝑏𝑏) = [1, 2].
We deﬁne the image of this map, the Parikh image, of some language L ⊆ Σ∗ as:𝜓 (L) = {𝜓 (𝑥) | 𝑥 ∈ L}
Thus, we would have 𝜓 ({𝑎𝑏, 𝑎𝑏𝑏}) = {[1, 1] , [1, 2]}. We also sometimes use the standard notation#𝑙 (𝑤) to talk about an individual letter 𝑙 in a word 𝑤. For example, for the Parikh vector above, wewould have #𝑎(𝑎𝑏𝑏) = 1.
Parikh’s theorem states that any context-free language has a Parikh-equivalent regular language (c.f. [Esparza et al. 2011] for a construction of such automata from context-free grammars
and [Lavado et al. 2013] for bounds on its size). The Parikh image is therefore a semi-linear set andPresburger-deﬁnable. While Parikh’s theorem applies to arbitrary context-free languages, in thispaper we focus only on regular languages.
3.4

The Parikh Image of a Regular Language Expressed in Presburger Arithmetic

It is known that the Parikh image of any context-free language can be described by a linear-size
existential Presburger formula [Verma et al. 2005]. This representation can be straightforwardly
adapted for use with a product of regular languages. For an intuition, the approach consists ofﬁrst computing the product, then assigning each state and transition an existentially quantiﬁed
non-negative integer variable, and then describing all paths through the automaton through two
sets of constraints: ﬂow equations relating the inﬂow and outﬂow of each automaton state, andconstraints that enforce connectedness by ordering states by distance in a spanning tree rooted in
the initial state.
We refer to this model as the baseline approach, though we also apply optimisations as describedin Section 7.1. The calculus introduced in this paper, by contrast, lazily enforces the connectedness
constraint while also interleaving the computation of products of automata and propagating
information between the steps to reduce the amount of work that needs to be done.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

A Constraint Solving Approach to Parikh Images of Regular Languages

138:11

4 PROJECTIONS ON PARIKH IMAGES
The Parikh map 𝜓 represents a homomorphism from the (free) non-commutative monoid Σ∗ to the(free) commutative monoid N𝑘 . We are, however, often interested in projections of the Parikh map,
rather than the full image. We therefore consider arbitrary homomorphisms ℎ : Σ∗ → 𝑀, where𝑀 = (𝑋 ; ⊕; 0𝑀 ) is a commutative monoid. We give several examples of such projections on Parikh
images later in this section.
Observe that every homomorphism ℎ : Σ∗ → 𝑀 can be represented as the composition ℎ ′ ◦ 𝜓 ,for some homomorphism ℎ ′ : N𝑘 → 𝑀. One of the insights underlying our approach is that it ismore eﬃcient to directly compute a projection ℎ(L) on the Parikh image, than to ﬁrst compute thestandard image 𝜓 (L) followed by projection to some property of interest.
Example 4.1 (String Length). One such simplifying homomorphism can express string length,
the problem that originally motivated our study of the Parikh map. This mapping is relevant
when solving constraints that combine language membership with string length, for instance theconstraint given in the introduction:𝑥 ∈ L 1 ∧𝑦 ∈ L 2 ∧|𝑥 | > |𝑦|(3)

To solve this formula, let 𝑀 = N, and deﬁne the homomorphism 𝐿 by 𝐿(𝑎) = 1 for all characÍ
ters 𝑎 ∈ Σ. The length of a string 𝑠 = 𝑠 1 ◦ · · · ◦ 𝑠𝑛 is given by 𝐿(𝑠) = 𝐿(𝑠𝑖 ) = 1 + · · · + 1 = 𝑛, and tosolve (3) we can instead solve the equi-satisﬁable formula 𝛼 ∈ 𝐿(L 1 ) ∧ 𝛽 ∈ 𝐿(L 2 ) ∧ 𝛼 > 𝛽. This
paper proposes eﬃcient native procedures to reason about membership constraints like 𝛼 ∈ 𝐿(L 1 ),avoiding the computation of the complete image 𝐿(L 1 ). This encoding can be seen applied toautomaton 𝐵 in Example 2.1 (see Fig. 1b).
4.1

Integer Constraints on Strings

Parikh images are also applicable for deciding more general classes of string constraints [Chen et al.
2020]. Consider the substring constraint Constraint (iii) of Example 2.1: 𝑠 1 = substring(𝑠 2, 𝑖, 𝑛),that is 𝑠 1 is an 𝑛-length substring of 𝑠 2 starting at oﬀset 𝑖. That constraint belongs to an expressive
fragment of string logic that cannot be decided by most state-of-the-art string solvers.
In Section 2 we modelled Constraint (iii) (and the other constraints) using Parikh automata [Cadilhac et al. 2011; Klaedtke and Rueß 2002]. A Parikh automaton is a ﬁnite-state automaton extended
such that transitions are additionally labelled with oﬀset vectors deﬁning the increments of aﬁnite number of counters. This means that Parikh automata recognise words over an extendedalphabet Σ × 𝐷, where 𝐷 ⊆ N𝑑 is a ﬁnite set of increment vectors (notation as in [Cadilhac et al.
2011]) and Σ is the alphabet of the original automaton.
We use the symbols 𝜋 Σ, 𝜋𝐷 to denote projections to the ﬁrst and the second component of acomposite letter (𝑎, 𝑣¯), respectively, and extend those projections to words:
𝜋 Σ ((𝑎 1, 𝑣¯1 ) ◦ · · · ◦(𝑎𝑘 , 𝑣¯𝑘 )) = 𝑎 1 ◦ · · · ◦ 𝑎𝑘 ,𝜋𝐷 ((𝑎 1, 𝑣¯1 ) ◦ · · · ◦(𝑎𝑘 , 𝑣¯𝑘 )) = 𝑣¯1 + · · · + 𝑣¯𝑘 .

Deﬁnition 4.1. A Parikh automaton of dimension 𝑑 ≥ 0 is a pair ⟨A, 𝐶⟩, where 𝐶 ⊆ N𝑑 is a semilinear set (or, equivalently, a Presburger formula), and A is a ﬁnite automaton with the alphabet
Σ × 𝐷, where 𝐷 ⊆ N𝑑 . We say that ⟨A, 𝜑⟩ recognises a word 𝑤 ∈ Σ∗ if and only if the automaton
has a run accepting an extended word 𝑤 ′ ∈ (Σ × 𝐷) ∗ such that 𝜋 Σ (𝑤 ′ ) = 𝑤 and 𝜋𝐷 (𝑤 ′ ) ∈ 𝐶.
Applied to Constraint (iii), the decision procedure in [Chen et al. 2020] will construct a preimage of 𝑠 1 under the substring operation, and check whether this pre-image is consistent with theconstraint 𝑠 2 ∈ L (𝐵), corresponding to the full product seen in Example 2.1. Because substring
depends on the values of the integer variables 𝑖, 𝑛, a Parikh automaton, shown in Fig. 1a, models
the pre-image. The Parikh automaton has dimension 3, as it includes also the length register 𝑙𝐴 ,Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

138:12

Amanda Stjerna and Philipp Rümmer

besides variables 𝑖, 𝑛. Intuitively, this construction accumulates any preﬁx symbol, incrementing
𝑖 to mark the start of the substring; followed by the automaton representing the substring itself,
modiﬁed to add a counter to increment 𝑛 at each transition; followed by a state that accepts any
suﬃx after the matched substring.
Denoting the language described by Fig. 1a as L 𝑝𝑟𝑒 , we can then replace 𝑠 1 = substring(𝑠 2, 𝑖, 𝑛)and 𝑠 2 ∈ L (𝐵) (of Constraint (i)) with an equi-satisﬁable formula that no longer contains any
explicit substring operation:
𝑙𝐴 
 
(4)
𝑝 ∈ L 𝑝𝑟𝑒 ∧ 𝜋 Σ (𝑝) ∈ L (𝐵) ∧ 𝜋𝐷 (𝑝) =  𝑖  ∧ 0 ≤ 𝑖 ≤ 𝑖 + 𝑛 ≤ 𝑙𝐴𝑛  
To check the satisﬁability of Eq. (4), we need a decision procedure that can process intersections ofregular languages (in this case, of L 𝑝𝑟𝑒 and L (𝐵), synchronising on Σ), while imposing the side
condition 0 ≤ 𝑛 ≤ 𝑚 ≤ |𝑝 | on the increment sum. In [Chen et al. 2020], this decision procedureturned out to be main bottleneck of the string solver, which was one of the motivations to develop
the lazy algorithm proposed in this paper.

5 A CALCULUS FOR PROJECTIONS ON PARIKH IMAGES
We start by deﬁning our calculus, PC*, for one automaton, and only extend it to products ofautomata in Section 6. Assume an automaton A = ⟨𝑄, 𝑞𝐼 , 𝐹, 𝛿⟩ with 𝑘 transitions 𝛿 = {𝑡 1, · · · , 𝑡𝑘 }.
We use the notations introduced in Section 3.2. For convenience, we introduce the following
additional notions:𝑙Deﬁnition 5.1. The transition count, #(𝑡, 𝑝) is the number of times a transition 𝑡 = 𝑞 →− 𝑞′ ∈ 𝛿
appears on a path 𝑝. A transition selection function is a function 𝜎 : 𝛿 → N labelling everytransition 𝑡 ∈ 𝛿 with a non-negative number.
We introduce the two predicates that will be used by our calculus, with the following deﬁnitions:Deﬁnition 5.2. The Parikh predicate, Im A,ℎ (𝜎, 𝑚) holds for some automaton A = ⟨𝑄, 𝑞𝐼 , 𝐹, 𝛿⟩,some homomorphism ℎ : Σ∗ → 𝑀 to a commutative monoid 𝑀, some transition selection function
𝜎 : 𝛿 → N, and some monoid element 𝑚 ∈ 𝑀 if 𝑚 is an element of the Parikh image of L (A)modulo ℎ, or more formally, when there is an accepting path 𝑝 = ⟨𝑞 0𝑙 1𝑞 1 . . . 𝑞𝑛 ⟩ ∈ Paths(A) suchthat 𝜎 (𝑡) = #(𝑡, 𝑝) for all 𝑡 ∈ 𝛿, and 𝑚 = ℎ(𝑤 (𝑝)).
Deﬁnition 5.3. Conn(A, 𝜎) holds for some automaton A = ⟨𝑄, 𝑞𝐼 , 𝐹, 𝛿⟩ and transition selection
function 𝜎 : 𝛿 → N if for every 𝑡 = 𝑞 →− 𝑞 ′ ∈ 𝛿, if 𝜎 (𝑡) > 0 there is some 𝜎-selected accepting paththat visits 𝑡’s starting state 𝑞. More formally, if 𝜎 (𝑡) > 0 then there is some path 𝑝 ∈ Paths(A) with𝜎 (𝑡 ′ ) > 0 for every 𝑡 ′ ∈ 𝑝, and 𝑞 ∈ States(𝑝) such that 𝑝 ends in an accepting state 𝑞 ′ ∈ 𝐹 . The
predicate Conn(A, 𝜎) represents the condition that A is connected under the selection function 𝜎
for every transition, and is implied by Im A,ℎ (𝜎, 𝑚).
The rules of PC* for one automaton are given in Table 1. The rules operate on sets of formulasand can be interpreted as rules of a one-sided sequent calculus, in which all formulas are located in
the antecedent [Fitting 1996]. The rules relate premises 𝛤1, . . . , 𝛤𝑘 with some conclusion 𝛤 . When
constructing a proof, we start with some root 𝛤 , and then apply proof rules to the goals of theproof in bottom-up direction until all goals are closed, or no more rules are applicable.
A proof in which all proof goals are closed shows that the formulas in the root 𝛤 of the proof areinconsistent (have no solutions). An unclosable goal to which no rules are applicable gives rise
to a solution of the formulas in the root 𝛤 . Such a goal will only contain formulas in Presburger
arithmetic, allowing a solution to be computed using standard algorithms [Harrison 2009].
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

A Constraint Solving Approach to Parikh Images of Regular Languages

138:13

Table 1. Derivation rules for one automaton.

Name

Rule
Conn(A, 𝜎), Flow(A, 𝜎), 𝑚 =ÕSide conditions
𝜎 (𝑡) · ℎ(𝑡), 𝐸, 𝛤𝑡 ∈𝛿 A

ExpandIm A,ℎ (𝜎, 𝑚), 𝐸, 𝛤Conn(A, 𝜎), 𝐸, 𝛤, 𝜎 (𝑡) = 0 | Conn(A, 𝜎), 𝐸, 𝛤, 𝜎 (𝑡) > 0

Split

Conn(A, 𝜎), 𝐸, 𝛤Conn(A, 𝜎), {𝜎 (𝑡 ′ ) = 0 | 𝑡 ′ ∈ 𝐶} , 𝐸, 𝛤, 𝜎 (𝑡) = 0

Prop

Conn(A, 𝜎), {𝜎 (𝑡 ′ ) = 0 | 𝑡 ′ ∈ 𝐶} , 𝐸, 𝛤𝐸, 𝛤SubsumeNone

if 𝑡 ∈ 𝛿 A

if 𝑡 ∈ 𝛿 A andDom(𝐶, A, 𝑡)
Split and Prop
cannot be appliedConn(A, 𝜎), 𝐸, 𝛤

We use the convention of splitting the formulas in proof goals into linear (in-) equalities (𝐸) andother formulas (𝛤 ), and assume that predicates Im and Conn only occur positively. The transition
selection function 𝜎 is represented symbolically and can, in practice, be read as a function fromtransitions to N-valued terms (e.g. t or t+1). In our implementation Catra, described in Section 7,
𝜎 is a vector of fresh variables with the same size as 𝛿.
To ensure termination, rules can only be applied when they add new formulas on every createdbranch (the notion of regularity of a proof is required [Fitting 1996]). For example, this means that
Split can only be applied to proof goals that contain neither 𝜎 (𝑡) = 0 nor 𝜎 (𝑡) > 0, and can neverbe applied to split on the same term twice on the same branch.
The rule Expand expands an Im A,ℎ (𝜎, 𝑚) predicate into the more basic predicate Conn(A, 𝜎),as well as linear equations relating the transitions mentioned by 𝜎 with the monoid element 𝑚,and linear ﬂow equations described by Flow (below). Since Conn and Im are partially redundant
and the diﬀerence is covered by Flow, we can remove the instance of Im when applying Expand.
In this sense, we split the semantics of the Im predicate into its counting aspect (covered by Flow)and its connectedness aspect (covered by Conn).
𝑙

In Expand, we use the shorthand notation ℎ(𝑞 →− 𝑞 ′ ) = ℎ(𝑙), i.e., we allow the homomorphism ℎ
to be applied also to transitions 𝑡. The predicate Flow(A, 𝜎) represents the ﬂow equations tobe generated when expanding Im A,ℎ (𝜎, 𝑚). We assume that each application of the predicate
introduces fresh integer variables 𝑓𝑞 for every accepting state 𝑞 ∈ 𝐹 , and deﬁne:ÛÕÛFlow(A, 𝜎) =𝑓𝑞 ≥ 0 ∧𝑓𝑞 = 1 ∧In(𝑞, 𝜎) − Out(𝑞, 𝜎) = Sink(𝑞)
𝑞 ∈𝐹

𝑞 ∈𝐹

𝑞 ∈𝑄

Sink(𝑞) = 0 if 𝑞 ∉ 𝐹, 𝑓𝑞 otherwise.
ÕIn(𝑞, 𝜎) = StartFlow(𝑞) +𝜎 (𝑡)𝑡 ∈ (→− 𝑞)
StartFlow(𝑞) = 1 if 𝑞 = 𝑞𝐼 , otherwise 0.
ÕOut(𝑞, 𝜎) =𝜎 (𝑡)𝑡 ∈ (𝑞→−)Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

138:14

Amanda Stjerna and Philipp Rümmer

The rule Split allows us to branch the proof tree by trying to exclude a transition from a potential
solution before concluding that it must be included. Intuitively, this is what guarantees our ability
to make forward progress by eliminating paths through A.
The Prop rule allows us to propagate (dis-)connectedness across A. It states that we are only
allowed to use transitions attached to a reachable state, and is necessary to ensure connectedness
in the presence of cycles in A. The rule makes use of the notion of dominating sets of transitions,deﬁned as follows:
Deﬁnition 5.4. A set 𝐶 of transitions of an automaton A dominates a transition 𝑡, written
Dom(𝐶, A, 𝑡), if every accepting path 𝑝 of A with 𝑡 ∈ 𝑝 contains at least one transition from 𝐶.
Notably, Dom(∅, A, 𝑡) for every unreachable transition 𝑡, and Dom({𝑡 } , A, 𝑡) for every transition 𝑡.
The Dom relation can be eﬃciently implemented in a solver by using standard Ford-Fulkerson/
Edmonds-Karp min-cut between a state and the initial state after removing transitions where𝜎 (𝑡) = 0. By only performing this computation after such ﬁltering, a solver additionally avoids
breaking the rule of adding clauses that already appear in the formula.
Finally, the rule Subsume can be applied when the connectedness of an automaton has been
ensured by exhaustive application of the other rules. This suggests a proof strategy where you
Prop when you can, Split when you must, and Subsume when neither is possible anymore.
In addition to Table 1, we assume the existence of a rule Presburger-Close, corresponding to asound and complete solver for Presburger arithmetic formulas, and for constraints over 𝑀.
A decision procedure would start from one or multiple predicates Im A,ℎ (𝜎, 𝑚) to be satisﬁed,
possibly in combination with other constraints about 𝑚. It would then ﬁrst expand the predicatesusing the Expand rule, and subsequently apply the other rules to search for a solution.
As illustrated in Section 2, a decision procedure can also perform arithmetic rewriting of theoccurring terms and equations. Such reasoning is not necessary for correctness or completeness,but it shortens the examples considerably; we will therefore assume the existence of a rule Algebrathat allows us to perform standard algebraic reasoning on linear arithmetic constraints.
5.1

An Example

Here we will return to A ′ from Section 2 and perform the steps of Sections 2.2.2 and 2.2.3 withthe formal calculus we just established, but exclude Constraint (ii) and therefore the entire automaton B, since we introduce support for products of automata in Section 6. The example thenbecomes satisﬁable, as 𝑠 1 = dd, 𝑖 = 1, 𝑠 2 = adda, 𝑙𝐴 = 4 is a satisfying assignment to Constraint (i)and Constraint (iii) to Constraint (v).
𝑐/𝑖Starting with A ′ , ℎ extracts the increments of a transition, ℎ(𝑞 1 −−→ 𝑞 2 ) = 𝑣® for the increment
Σ/[𝑙𝐴+ ,𝑖 + ]vector 𝑣®, concretely ℎ(𝐼𝐴 −−−−−−−→ 𝐼𝐴 ) = [𝑙𝐴+, 𝑖 + ]. We use the same compact notation here as in
Section 2 to represent what is essentially a sparse vector of 1 and 0 coeﬃcients, i.e. [𝑙𝐴+, 𝑖 + ] = [1, 1, 0].
The reader is advised to review Fig. 1a from Section 2 while going through this example.
Initially, we let 𝜎 map to fresh variables to obtain, after some simpliﬁcations:𝑑/[𝑙𝐴+ ,𝑛 + ]𝜎 (𝐷 −−−−−−−−→ 𝐹𝐴 )𝑑/[𝑙𝐴+ ,𝑛 + ]𝜎 (𝐼𝐴 −−−−−−−−→ 𝐷)

= 𝑥1
= 𝑥4

Σ/[𝑙𝐴+ ]𝜎 (𝐹𝐴 −−−−−−→ 𝐹𝐴 )
Σ/[𝑙𝐴+ ,𝑖 + ]𝜎 (𝐼𝐴 −−−−−−−→ 𝐼𝐴 )Flow(A ′, 𝜎) == 𝑥2

𝑐/[𝑙𝐴+ ,𝑛 + ]𝜎 (𝐼𝐴 −−−−−−−−→ 𝐹𝐴 )

= 𝑥3

= 𝑥5

1+✚
𝑥5 = ✚
𝑥5 + 𝑥4 + 𝑥3 ∧𝑥4 = 𝑥1 ∧𝑥3 + 𝑥1 + ✚𝑥2 = ✚
𝑥2 + 1

Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

(5)

A Constraint Solving Approach to Parikh Images of Regular Languages

138:15..
.
𝑥 1 = 1 ∧ 𝑥 2 = 𝑙𝐴 − 3 ∧ 𝑥 3 = 0 ∧ 𝑥 4 = 1 ∧ 𝑥 5 = 1 ∧ 𝑛 = 2 ∧ 𝑖 = 1 ∧ 𝑙𝐴 > 3
Conn(𝐴′, 𝜎) ∧𝑥 1 = 1 ∧ 𝑥 2 = 𝑙𝐴 − 3 ∧ 𝑥 3 = 0 ∧ 𝑥 4 = 1 ∧ 𝑥 5 = 1 ∧ 𝑛 = 2 ∧ 𝑖 = 1 ∧ 𝑙𝐴 > 3
Conn(𝐴′, 𝜎) ∧𝑥 1 = 𝑛 − 1 ∧ 𝑥 2 = 𝑙𝐴 − 𝑛 − 𝑖 ∧ 𝑥 3 = 2 − 𝑛 ∧ 𝑥 4 = 𝑛 − 1 ∧ 𝑥 5 = 𝑖 ∧𝑛 = 2 ∧ 𝑖 = 1 ∧ 𝑙𝐴 > 3
Conn(𝐴′, 𝜎) ∧𝑥 1 = 𝑛 − 1 ∧ 𝑥 2 = 𝑙𝐴 − 𝑛 − 𝑖 ∧ 𝑥 3 = 2 − 𝑛 ∧ 𝑥 4 = 𝑛 − 1 ∧ 𝑥 5 = 𝑖 ∧𝑛 > 𝑖 ∧ 𝑙𝐴 − 𝑖 − 𝑛 > 0 ∧ 𝑖 > 0
Conn(𝐴′, 𝜎) ∧1 = 𝑥4 + 𝑥3 ∧ 𝑥4 = 𝑥1 ∧ 𝑥3 + 𝑥1 = 1 ∧𝑙𝐴 = 𝑥 1 + 𝑥 2 + 𝑥 3 + 𝑥 4 + 𝑥 5 ∧ 𝑖 = 𝑥 5 ∧ 𝑛 = 𝑥 1 + 𝑥 3 + 𝑥 4 ∧𝑛 > 𝑖 ∧ 𝑙𝐴 − 𝑖 − 𝑛 > 0 ∧ 𝑖 > 0
Conn(𝐴′, 𝜎) ∧ Flow(𝐴′, 𝜎) ∧𝑙𝐴 = 𝑥 1 + 𝑥 2 + 𝑥 3 + 𝑥 4 + 𝑥 5 ∧ 𝑖 = 𝑥 5 ∧ 𝑛 = 𝑥 1 + 𝑥 3 + 𝑥 4 ∧𝑛 > 𝑖 ∧ 𝑙𝐴 − 𝑖 − 𝑛 > 0 ∧ 𝑖 > 0ÍConn(𝐴′, 𝜎) ∧ Flow(𝐴′, 𝜎) ∧ [𝑙𝐴 , 𝑖, 𝑛] =ℎ(𝑡) · 𝜎 (𝑡) ∧SubsumeAlgebra: =-simp.

Algebra: >-reasoning

Algebra: =-simp.

(Expanding Flow)(Expanding sum)𝑡 ∈𝛿 A ′𝑛 > 𝑖 ∧ 𝑙𝐴 − 𝑖 − 𝑛 > 0 ∧ 𝑖 > 0

ExpandIm A ′ ,ℎ (𝜎, [𝑙𝐴 , 𝑖, 𝑛]) ∧ 𝑛 > 𝑖 ∧ 𝑙𝐴 − 𝑖 − 𝑛 > 0 ∧ 𝑖 > 0
Fig. 4. A proof tree for Constraint (i) and Constraint (iii) to Constraint (v) from Example 2.1, corresponding tohandling the Parikh automaton A ′ of Fig. 1a.

The proof tree is shown in Fig. 4. Like in Sections 2.2.1 and 2.2.2, by arithmetic reasoning the
calculus ends up with ﬁxed values for several of the transition variables 𝑥𝑘 , and eventually concludes
that the transition directly from state 𝐼𝐴 to 𝐹𝐴 (variable 𝑥 3 ) is incompatible with the constraint.
It is then possible to remove the Conn predicate using Subsume, since Prop is not able to infer
further constraints, and no non-trivial applications of Split remain to be done. After this, byfurther arithmetic reasoning we can derive a solution 𝑙𝐴 = 4, 𝑖 = 1, 𝑛 = 2, and conclude that the root
constraint is satisﬁable. To obtain values for the string variables 𝑠 1, 𝑠 2 corresponding to the solution,
one can construct an accepting path of the automaton with each transition 𝑡 taken 𝜎 (𝑡) times.
5.2

Correctness of PC*

Our correctness proof of PC* consists of two main parts: ﬁrst, we show that the constructionof a proof always terminates, and then that each of the proof rules in Table 1 is an equivalencetransformation, i.e., does not change the set of satisfying assignments of a formula. In combination,
those two results immediately imply that PC* gives rise to a decision procedure.
5.2.1

PC* Terminates.

Lemma 5.1. Suppose 𝛤 is a set of formulas in which the predicates Im and Conn only occur positively.
There is no inﬁnite sequence of proofs 𝑃0, 𝑃1, 𝑃2, . . . in which 𝑃 0 has 𝛤 as root, and each 𝑃𝑖+1 is derived
from 𝑃𝑖 by applying one of the rules in Table 1.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

138:16

Amanda Stjerna and Philipp Rümmer

Proof. The rule Expand can only be applied ﬁnitely often since each application removes one
Im predicate, and none of the rules introduce new instances of the predicate. The rule Subsume
can only be applied ﬁnitely often since it strictly decreases the combined number of Im and Connpredicates in sets of formulas, and none of the rules increases that number.
To show termination of Split and Prop, observe that the 𝜎 in a predicate Conn(A, 𝜎) is never
updated on a proof branch, which means that the set of terms 𝜎 (𝑡) for 𝑡 ∈ A on every branch is
ﬁnite. Each application of Split and Prop adds a new formula 𝜎 (𝑡) = 0 or 𝜎 (𝑡) > 0 to a proof goal,
which can only happen ﬁnitely often.
□
5.2.2

The Rules in Table 1 are Solution-Preserving.

Lemma 5.2. Consider an application of one of the rules in Table 1, with premises 𝛤1, . . . , 𝛤𝑘 andconclusion 𝛤 . An assignment 𝛽 satisﬁes the conclusion 𝛤 if and only if it satisﬁes one of the premises 𝛤𝑖 .
Proof. This property has to be shown by analysing the possible applications of each proof rule.
Expand unfolds the deﬁnition of the Im predicate. To show that the rule is solution-preserving,
we prove the equivalence of the upper and lower sets of formulas:• Assume that 𝛽 satisﬁes the conclusion, which means that there is some accepting path𝑝 = ⟨𝑞 0𝑙 1𝑞 1 . . . 𝑞𝑛 ⟩ ∈ Paths(A) with val𝛽 (𝜎 (𝑡)) = #(𝑡, 𝑝) and val𝛽 (𝑚) = ℎ(𝑤 (𝑝)). This
immediately implies that 𝛽 satisﬁes Conn(A, 𝜎), since a path is connected, and Flow(A, 𝜎)Ísince an accepting path satisﬁes the ﬂow equations. The equation 𝑚 = 𝑡 ∈𝛿 A 𝜎 (𝑡) ·ℎ(𝑡) holds
because of val𝛽 (𝜎 (𝑡)) = #(𝑡, 𝑝).
• Assume that 𝛽 satisﬁes the premise, which implies that val𝛽 (𝜎) describes a consistent, connected ﬂow of the automaton. By the same argument as in [Verma et al. 2005], this ﬂow
can be mapped to an accepting path 𝑝 of A such that each transition 𝑡 occurs on 𝑝 exactly
val𝛽 (𝜎 (𝑡)) times. Together with the equation val𝛽 (𝜎 (𝑡)) = #(𝑡, 𝑝), this implies that 𝛽 satisﬁes
Im A,ℎ (𝜎, 𝑚).
In Split, we make use of the fact that 𝜎 (𝑡) is N-valued by deﬁnition. For any 𝛽, clearly exactly
one of 𝜎 (𝑡) = 0 or 𝜎 (𝑡) > 0 will be satisﬁed, implying the property.
For Prop, suppose that Dom(𝐶, A, 𝑡), which means that every accepting path containing 𝑡
contains at least one of the transitions in 𝐶. For a 𝛽 satisfying Conn(A, 𝜎). This means that every
accepting path 𝑝 where 𝑡 ∈ 𝑝 has at least one transition 𝑡 ′ ∈ 𝐶 such that 𝜎 (𝑡 ′ ) = 0. This means that
also val𝛽 (𝜎 (𝑡)) = 0 has to hold since no unbroken path containing 𝑡 exists.
Finally, for Subsume, observe that if Split cannot be applied, then a goal must contain 𝜎 (𝑡) = 0
or 𝜎 (𝑡) > 0 for every 𝑡. In case the formulas in 𝐸 are inconsistent, an application of Subsume istrivially solution-preserving; therefore assume that 𝐸 is consistent, which means that it contains
exactly one of 𝜎 (𝑡) = 0 or 𝜎 (𝑡) > 0 for each 𝑡. Since Prop is not applicable, the transitions 𝑡with 𝜎 (𝑡) > 0 must form a connect sub-graph of the automaton; this means that Conn(A, 𝜎) is
redundant as it is implied by 𝐸.
□
6 PARIKH IMAGES FROM PRODUCTS OF AUTOMATA
We now generalise our calculus to natively work with intersections of regular languages, or
equivalently products of automata. For this extension, we change the main predicate Im to beindexed by a vector of automata ⟨A1, . . . , A𝑘 ⟩. For simplicity, we assume that the sets of states of
the 𝑘 automata (and therefore also the transition sets) are pairwise disjoint.
Deﬁnition 6.1. Suppose A1, . . . , A𝑘 are automata, ℎ : Σ∗ → 𝑀 is a homomorphism to a commuÐ
tative monoid 𝑀, 𝜎 : 𝑘𝑖=1 𝛿 A𝑖 → N is a transition selection function, and 𝑚 ∈ 𝑀. The predicate
Im ⟨ A1,...,A𝑘 ⟩,ℎ (𝜎, 𝑚) is true exactly when there are accepting paths 𝑝 1, . . . , 𝑝𝑘 of the respective
automata, such that for each 𝑖 ∈ {1, . . . , 𝑘 } and 𝑡 ∈ 𝛿 A𝑖 it holds that
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

A Constraint Solving Approach to Parikh Images of Regular Languages

138:17

Table 2. Additional derivation rules for products of arbitrarily many automata.

Name

ExpandM

RuleSide conditions𝑘Flow(A𝑖 , 𝜎), Conn(A𝑖 , 𝜎), 








Õ
,
𝑚=
𝜎 (𝑡) · ℎ(𝑡)






𝑡 ∈𝛿 A𝑖𝑖=1
Im ⟨ A1,...,A𝑘 ⟩,ℎ (𝜎, 𝑚), 𝐸, 𝛤Im ⟨ A1,...,A𝑘 ⟩,ℎ (𝜎, 𝑚), 𝐸, 𝛤None

Flow(A ′, 𝜎 ′ ),Conn(A , 𝜎 ′ ), Bind(A𝑖 , A 𝑗 , A ′, 𝜎 ′ ),Im ⟨ A1,A𝑖 −1,A𝑖+1,...,A 𝑗 −1,A 𝑗 +1,...,A𝑘 ,A ′ ⟩,ℎ (𝜎 ′, 𝑚), 𝐸, 𝛤′

MaterialiseIm ⟨ A1,...,A𝑖 ,...,A 𝑗 ,...,A𝑘 ⟩,ℎ (𝜎, 𝑚)𝐸, 𝛤

𝜎 ′ = Extend(A ′, 𝜎),1 ≤ 𝑖 < 𝑗 ≤ 𝑘,
A ′ = 𝜎 𝐸 (A𝑖 ) × 𝜎 𝐸 (A 𝑗 )• the multiplicity of 𝑡 on 𝑝𝑖 is consistent with 𝜎, that is, 𝜎 (𝑡) = #(𝑡, 𝑝𝑖 ),• the automata all accept the same word 𝑤 (𝑝𝑖 ) = 𝑤 (𝑝 1 ), and• the accepted word is mapped to 𝑚 = ℎ(𝑤 (𝑝𝑖 )) = ℎ(𝑤 (𝑝 1 )).
For the calculus (Table 2), we ﬁrst extend Expand to generate ﬂow equations and instancesof Conn for each automaton, resulting in a new rule ExpandM. Unlike Expand, ExpandM does
not remove the Im predicate, since it is needed to keep track of the currently considered partial
products.
The rule Materialise introduces the product of two individual automata A𝑖 , A 𝑗 ; this step
eliminates A𝑖 , A 𝑗 as index of the Im predicate, and instead adds the product of the automata
restricted to the transitions that can still be taken. The rule also introduces the ﬂow equations andthe Conn predicate.
In Materialise, we use the following notation for pruning away parts of an automaton basedon the transition selection function 𝜎, only keeping those transitions for which 𝜎 is positive:
𝜎 𝐸 (A) = ⟨𝑄, 𝑞𝐼 , 𝐹, {𝑡 ∈ 𝛿 | (𝜎 (𝑡) = 0) ∉ 𝐸}⟩
This ﬁltering operation can be optimised to also eliminate states from 𝑄 and 𝐹 that become
unreachable; this is kept implicit for sake of presentation at this point.
The rule Materialise has to connect the newly introduced product to the previous automata
A𝑖 , A 𝑗 . This is done by extending the selection function 𝜎 to 𝜎 ′ , mapping the transitions of the
product to fresh variables 𝑥𝑡 :(𝑥𝑡
Extend(A , 𝜎)(𝑡) =𝜎 (𝑡)′𝑡 ∈ 𝛿 A′otherwise

The multiplicity of transitions in the product then has to be related to the multiplicities in
the individual automata, modelled using the Bind predicate. The predicate expresses that themultiplicity of a transition 𝑡 ∈ 𝛿 A𝑖 in A𝑖 has to coincide with the sum of the multiplicities ofProc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

138:18

Amanda Stjerna and Philipp Rümmer

transitions in 𝜎 𝐸 (A𝑖 ) × 𝜎 𝐸 (A 𝑗 ) derived from 𝑡, and similarly for A 𝑗 :








Õ
 ′



𝑙
′ ′
′
𝜎 (𝑡 ) | 𝑡 = 𝑞 →− 𝑞 ∈ 𝛿 A𝑖 ∪𝜎 (𝑡) =




𝑙




𝑡 ′ =⟨𝑞,𝑞𝑅 ⟩→−𝑞 ′ ,𝑞𝑅′ ⟩ ∈𝛿 A ′
⟨


′ ′
Bind(A𝑖 , A 𝑗 , A , 𝜎 ) =








Õ


 ′

𝑙
𝜎 ′ (𝑡 ′ ) | 𝑡 = 𝑞 →− 𝑞′ ∈ 𝛿 A 𝑗
𝜎 (𝑡) =




𝑙




𝑡 ′ =⟨𝑞𝐿 ,𝑞⟩→− ⟨𝑞𝐿′ ,𝑞 ′ ⟩ ∈𝛿 A ′For precisely one automaton, neither rule applies, and we perform the calculus as before.
6.1 An Example
We return to our example in Section 2. We also reuse the deﬁnition of ℎ as the simple projection
to extract the counter increments, so in this case, ℎ(𝑡) = [𝑙𝐵+ ] for every transition 𝑡 since B only
counts length. The reader is advised to review Figs. 3a and 3b from Section 2 while going throughthis example. The transition variables of the ﬁgures match the ones used here.
We extend Eq. (5) from Section 5.1 with deﬁnitions for 𝐵 shown in Eq. (6):𝑎/𝑙𝐵+

𝜎 (𝐴 −−−−→ 𝐹𝐵 )𝑐/𝑙𝐵+𝜎 (𝐵 −−−−→ 𝐵)𝑏/𝑙𝐵+

𝜎 (𝐼𝐵 −−−−→ 𝐵)

= 𝑥6
= 𝑥9

𝑐/𝑙𝐵+

𝜎 (𝐴 −−−−→ 𝐴)
𝑐/𝑙𝐵+

𝜎 (𝐵 −−−−→ 𝐹𝐵 )= 𝑥7
= 𝑥 10𝑏/𝑙𝐵+

𝜎 (𝐵 −−−−→ 𝐼𝐵 )𝑎/𝑙𝐵+

𝜎 (𝐼𝐵 −−−−→ 𝐴)= 𝑥8= 𝑥 11= 𝑥 12

Flow(B, 𝜎) =1 + 𝑥 8 = 𝑥 11 + 𝑥 12 ∧𝑥 11 = 𝑥 6 ∧𝑥 12 = 𝑥 8 + 𝑥 10
𝑥 6 + 𝑥 10 = 1(6)The only possible rule at the start is ExpandM, which we use to add the corresponding constraints
on each automaton of the product as we would have had in the single-automaton version. After
that, we expand the various sums and apply light equality propagation.
We then continue by repeating the steps of Section 5.1, shown in Fig. 4 since the steps to propagate
Example 2.1 across the automaton A ′ still apply for the product. Note that this ﬁxes the values of
all transitions but one of A ′ , including the free counter variables 𝑖, 𝑛, whose new constant values
we propagate everywhere.
Once we have performed reasoning by equality to eliminate transition variables, we obtain theversion of B shown in Fig. 3b and represented by the clauses in the ﬁnal node in the tree. This
corresponds to the end of Section 2.2.2. Our only options now are to either split on which path wetake from 𝐼𝐵 by case-splitting on 𝑥 12 or to directly invoke Materialise. The latter would produce ashorter tree in this instance but might lead to a larger product being computed, so we pick Split.
This leads to an opportunity for propagation since 𝑥 12 = 0 cuts oﬀ 𝑥 9 from 𝐼𝐵 on the left branch.
Note that the same opportunity does not present itself on the right branch; the use of the upper
path to state 𝐴 does not preclude visiting state 𝐵.
In both cases the automata are now simpler, so we apply Materialise to obtain their product,
which for both branches is empty. An empty product will have no outgoing transitions from its
initial state, and so will lead to a ﬂow equation 1 = 0. We can then close the proof and know thatthe problem is unsatisﬁable. A full derivation tree for the example can be found in Fig. 5.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

A Constraint Solving Approach to Parikh Images of Regular Languages. . . ∧1 = 0∧ Im ∅,ℎ (𝜎, [𝑙𝐴 , 1, 2, 𝑙𝐴 ])𝑥 9 = 0 ∧ 𝑥 7 = 𝑙𝐴 − 2∧𝑥 2 = 𝑙𝐴 − 3 ∧ 𝑥 8 = 0∧𝑥 6 = 𝑥 11 = 1 ∧ 𝑥 10 = 0∧ Conn(𝐵, 𝜎)∧ Im ⟨ A ′ ,B ⟩,ℎ (𝜎, [𝑙𝐴 , 1, 2, 𝑙𝐴 ])138:19Materialise. . . ∧1 = 0∧ Im ∅,ℎ (𝜎, [𝑙𝐴 , 1, 2, 𝑙𝐴 ])Prop𝑥 12 = 0 ∧ 𝑥 7 = 𝑙𝐴 − 𝑥 9 − 2∧𝑥 2 = 𝑙𝐴 − 3 ∧ 𝑥 8 = 0∧𝑥 6 = 𝑥 11 = 1∧𝑥 10 = 0 ∧ Conn(B, 𝜎)∧ Im ⟨ A ′ ,B ⟩,ℎ (𝜎, [𝑙𝐴 , 1, 2, 𝑙𝐴 ])𝑥 12 > 0∧𝑥 7 = 𝑙𝐴 − 𝑥 9 − 2𝑥 11 − 2𝑥 12 ∧𝑥 2 = 𝑙𝐴 − 3∧
𝑥 8 = 𝑥 11 + 𝑥 12 − 1∧
𝑥 6 = 𝑥 11 ∧𝑥 10 = 1 − 𝑥 11 ∧Conn(B, 𝜎)∧Im ⟨ A ′ ,B ⟩,ℎ (𝜎, [𝑙𝐴 , 1, 2, 𝑙𝐴 ])𝑥 7 = 𝑙𝐴 − 𝑥 9 − 2𝑥 11 − 2𝑥 12∧𝑥 2 = 𝑙𝐴 − 3∧𝑥 8 = 𝑥 11 + 𝑥 12 − 1∧𝑥 6 = 𝑥 11
∧𝑥 10 = 1 − 𝑥 11
∧ Conn(B, 𝜎)∧ Im ⟨ A ′ ,B ⟩,ℎ (𝜎, [𝑙𝐴 , 1, 2, 𝑙𝐴 ])Split 𝑥 12 = 0

Í, Algebra
𝑙𝐴 = 𝑘=6 𝑥𝑘 ∧ 𝑥 2 = 𝑙𝐴 − 3 ∧ 1 + 𝑥 8 = 𝑥 11 + 𝑥 12 ∧ 𝑥 11 = 𝑥 6∧𝑥 12 = 𝑥 8 + 𝑥 10 ∧ Conn(B, 𝜎) ∧ Im ⟨ A ′ ,B ⟩,ℎ (𝜎, [𝑙𝐴 , 1, 2, 𝑙𝐴 ])Algebra: expand FlowÍ𝑙𝐴 = 𝑘=12
𝑥
∧
𝑥
=
𝑙
−
3
∧
Flow(B,
𝜎)
2
𝐴
𝑘
𝑘=6
∧ Conn(B, 𝜎) ∧ Im ⟨ A ′ ,B ⟩,ℎ (𝜎, [𝑙𝐴 , 1, 2, 𝑙𝐴 ])Repeat Fig. 4, 𝑙𝐴 = 𝑙𝐵 .
Í
Í𝑘=5
𝑙𝐵 = 𝑘=12
𝑘=6 𝑥𝑘 ∧ 𝑖 = 𝑥 5 ∧ 𝑙𝐴 = 𝑘=1 𝑥𝑘∧𝑛 = 𝑥 4 + 𝑥 1 ∧ Flow(B, 𝜎) ∧ Conn(A ′, 𝜎)∧ Conn(B, 𝜎) ∧ Im ⟨ A ′ ,B ⟩,ℎ (𝜎, [𝑙𝐴 , 𝑖, 𝑛, 𝑙𝐵 ])∧𝑙𝐴 = 𝑙𝐵 ∧ 𝑙𝐴 − 𝑖 − 𝑛 > 0 ∧ 0 < 𝑖 < 𝑛ExpandM
Im ⟨ A ′ ,B ⟩,ℎ (𝜎, [𝑙𝐴 , 𝑖, 𝑛, 𝑙𝐵 ]) ∧ 𝑙𝐴 = 𝑙𝐵 ∧ 𝑙𝐴 − 𝑖 − 𝑛 > 0 ∧ 0 < 𝑖 < 𝑛Í𝑘=12ExpandMaterialise

Fig. 5. A derivation for PC* on the Parikh image strings for the constraints of Example 2.1. Note the constantpropagation for 𝑛!

6.2 Correctness of PC* for Products of Automata
Since Table 2 only extends the existing rules of Table 1, we focus on the diﬀerences compared tothe calculus for a single automaton.
6.2.1

PC* for Products of Automata Terminates.

Lemma 6.1. Suppose 𝛤 is a set of formulas in which the product version of Im only occurs positively.
There is no inﬁnite sequence of proofs 𝑃0, 𝑃1, 𝑃2, . . . in which 𝑃 0 has 𝛤 as root, and each 𝑃𝑖+1 is derived
from 𝑃𝑖 by applying one of the rules in Table 2.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

138:20

Amanda Stjerna and Philipp Rümmer

Proof. The rule Materialise can similarly only be used ﬁnitely many times, as each application
reduces the number of automata in the product of Im by one automaton, until only one remains
and Lemma 5.1 for single-automaton instances apply.
ExpandM can only be applied precisely once per Im term since each application introduces anidentical set of formulas and we have a generic side condition that no rule may add only redundant
formulas.
□6.2.2 The Rules in Table 2 are Solution-preserving. Since our calculus now includes a rule introducing new variables, the Materialise rule, we have to slightly generalise the notion of solutionpreservation:
Lemma 6.2. Consider an application of one of the rules in Table 2, with premises 𝛤1, . . . , 𝛤𝑘 andconclusion 𝛤 . An assignment 𝛽 (over the symbols in 𝛤 ) satisﬁes the conclusion 𝛤 if and only if there isan extension 𝛽 ′𝑜 𝑓 𝛽 satisfying one of the premises 𝛤𝑖 .
Proof. We have to consider the two new rules in Table 2. The result is immediate for ExpandM,
since this rule does not remove the Im predicate from a proof goal, and the newly introduced
formulas are all implied by the Im predicate.
For Materialise, observe that the existence of an accepting path in A𝑖 × A 𝑗 is equivalent to
the existence of individual paths in A𝑖 , A 𝑗 accepting the same word. The path in the productwill satisfy the ﬂow equations and connectedness, and it will be related to the individual paths as
stipulated by the Bind predicate.
□
7 IMPLEMENTATION
We implement PC* for Parikh automata as described in Section 4.1. The artefact submitted alongwith this paper is a program that reads an instance ﬁle with one or more products of one or more
Parikh automaton with transition labels deﬁned as ranges of Unicode characters, along with a setof constraints on the ﬁnal values of their registers expressed as Presburger arithmetic in a C-like
syntax. We call this program Catra.
Catra is written in Scala, with the calculus described in this paper implemented as a theory
plug-in for the Princess automated theorem prover [Rümmer 2008], which also performs the
Presburger reasoning. For comparison, we also provide an implementation of the baseline methodfrom [Verma et al. 2005], a direct translation that uses the nuXmv symbolic model checker [Cavada
et al. 2014] to solve our constraints, and the approximation described in [Janků and Turoňová 2020]
on top of the standard baseline back-end. An example of an input ﬁle corresponding to our running
example introduced in Section 2 can be found in the root directory of the artefact [Stjerna andRümmer 2024].
Catra uses symbolic labels for automata. A symbolic label is deﬁned as a ﬁnite range of Unicode
code points. This allows representing regular expression patterns like (a-z) as a -> b [a, z] when
it would have otherwise required 27 non-symbolic transitions.
In satisfaction mode, supported by all backends, Catra tries to satisfy the constraints expressedby the input ﬁle, reporting Sat with register assignments or Unsat. Additionally, baseline and PC*
also support generating the Presburger formula describing the constraints of the input ﬁle, i.e.,
computing a closed-form representation of the complete Parikh image.
7.1 Implementing the Baseline
As a baseline, we use the same Presburger solver (Princess), input ﬁle parser, and automaton
implementation as Catra. We do this to better analyse the impact of the calculus rules themselves.
Adapting [Verma et al. 2005], we produce quantiﬁed Presburger formulae for each successive
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

A Constraint Solving Approach to Parikh Images of Regular Languages

138:21term and add them to Princess. We compute the product incrementally term by term, checking
satisﬁability at each step. We use a priority queue to select automata for each step and order themby their number of transitions. We use this heuristic to put oﬀ computing large (and therefore slow)
products until we have to, hoping to ﬁnd an empty intermittent product. This is roughly similar to
the approach taken in [Janků and Turoňová 2020].
Algorithm 1: How we implement the baseline approach
Data: A1, . . . , A𝑛 automata, other constraints 𝛤
Result: Sat or Unsat𝑝 ← newTheoremProver()assert(𝑝, 𝛤 )foreach A𝑖 do
assert(𝑝,𝜓 (A𝑖 ))if 𝑝 is Unsat then
break
end
end
𝑞 ← newPriorityQueue(A1, . . . , A𝑛 )while 𝑝 not Unsat and |𝑞| > 1 do
A, A ′ ← dequeue(q)assert(𝑝,𝜓 (A × A ′ ))enqueue(𝑞, A × A ′ )endreturn 𝑝’s SAT status
As an optimisation, our automata (including intermittent products) have dead states eliminatedduring construction. Any automaton we produce contains only states that are both reachable fromthe initial state and have a path to an accepting state. We never perform any other minimisationon the automata for either backend. More complex minimisation was left out since performing
minimisation on automata with counters is non-trivial.
7.2

Heuristics and Search Strategies

PC* as described in Sections 5 and 6 leaves some choices unspeciﬁed, including the priority ofrules and the order of their arguments. In this section, we address these and describe additional
implementation details and techniques used to enhance Catra.
7.2.1 Splitting, Materialisation, and Propagation. We order our rule applications as follows: ﬁrst,
propagate connectedness if possible, then perform materialisation if tractable as deﬁned below,
then ﬁnally resort to splitting as a last resort.
In addition to applying Split as described in Table 1 to randomly selected transitions, we prefersplitting to sever a strongly connected component from the initial state. We randomly select anautomaton where we can compute a cut between an SCC and the initial state, that is, where the SCC
does not contain the initial state and where the sum of the transition variables of the transitionsin the cut is not known to be positive. If there are multiple such strongly connected components,
we choose one randomly. We then proceed to split on the sum of the transition variables of the
cut as if it were a regular transition, e.g., its sum being zero or nonzero. In this way, we drive PC*
towards applying Prop.
The implementation of the connectedness constraint is opportunistic and straightforward. We
compute a set of dead states by performing forward and backward reachability computations on
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

138:22

Amanda Stjerna and Philipp Rümmer

an automaton, where we disregard any transition whose associated variable is known to be zero.
After that we add clauses ensuring any transition variable associated with a transition starting in adead state is zero.
Product materialisation is the ﬁnal piece of the puzzle. In the current implementation we put oﬀ
computing intermediate products until at most six transition variables of one of the automata are
not known to always be used (> 0) or always unused (≤ 0). The number was chosen experimentally.
The other automaton for the product is selected randomly.
7.2.2 Clause Learning. Catra enables clause learning by default when using our backend, as it
has been experimentally shown to increase the performance in aggregate (though not strictly).
We currently only implement minimal clause learning based on forward-reachability cuts. No
sophisticated clause learning for products has been implemented.
7.2.3 Random Restarts. Finally, we perform restarts scaled by the Luby series [Luby et al. 1993].
Experimental results have shown this to have a large improvement in performance, which isunsurprising given how many random choices we make during solving and how tail-heavy our
problem is.
8 EVALUATION
We evaluate the performance of Catra on 37 497 instances of Parikh automata intersection problems
generated by the Ostrich+ string constraint solver [Chen et al. 2020] when solving the PyEx
benchmarks, which are string constraints from symbolic execution that are known to be hard formany solvers [Reynolds et al. 2017]. After generating an initial 38 227, we remove 314 instancessolved in under ﬁve seconds by baseline as well as 416 instances that were duplicates of otherinstances in the set.
We also attempted to benchmark instances generated by Ostrich+ solving the Kaluza benchmarks [Saxena et al. 2010] (38 227 instances), but discarded them since they all turned out to betrivial for our tool Catra: every instance could be solved in under ﬁve seconds, with a mean
runtime of about 0.1s. The benchmarks are run on commit d54e33b of Catra.
The benchmarks for PC* and nuXmv are executed in parallel on a server running Ubuntu 22.04.3
LTS with an AMD Ryzen 9 5900X processor at 2.27 GHz and 12 cores, with 4 threads sharing thesame JVM. Baseline was executed one JVM instance per input as 6 jobs in with a 4 GB heap eachon an Intel i5-10600, 3.3 GHz CPU with 6 cores and 12 threads. Simultaneously, StarExec ran thesame experiment and produced almost identical results.
We compiled the code using Scala 2.13.12 and executed the experiments on OpenJDK Java
1.8 with a maximum heap of 100 GB. We used nuXmv version 2.0.0 invoked as a subprocess foreach instance. Instances were executed in batches of 10, each given a fresh JVM. Each JVM waswarmed up for 10 s on a random benchmark from the set before starting to execute. We believe thisrepresents a realistic use case where PC* is used to support, e.g., a string solver. Experiments were
executed in random order for all backends. Each instance got a time budget of 30 s.
All runtimes are measured in wall-clock time as observed by the JVM when executing the
instance, and exclude time spent parsing (usually far below 0.1 s).
8.1 Execution Time and Ability to Solve Instances
In Fig. 6a, we show how many of the 37 497 instances the respective back-end could solve. A
summary of their outcomes by instance type is also available in Table 3. Note that many instanceslack a ground truth as they are solved by only one backend. We see that PC* generally outperforms
nuXmv on determining unsatisﬁability, as does baseline, while being similar at satisﬁable instances.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

A Constraint Solving Approach to Parikh Images of Regular Languages

138:23
Boxplot grouped by backend
runtime30

Outcome by solver

30000

nr instances

25

SAT
UNSAT
TIMEOUTMEMORY_OUT
ERROR

35000

25000

20
15
10

20000

5

15000

0

10000

PC*

baseline[backend]

nuXmv

PC*

0

baseline

5000

backend(a) The division of statuses per backend.

nuXmv(b) The distribution of runtimes for solved instances
per backend, assuming they were solved within the
30 s timeout. The whiskers use the default placementin Pandas, 1,5 times the IQR (interquartile range).

1400
1200

nr solved

1000
800

backend600

PC*
PC*, no clause learning
PC*, no clause learning, no restarts
PC*, product threshold = 1
PC*, product threshold = 200
baseline
nuXmv

400
200
0
0

20

40

60

after

80

100

120

(c) The number of instances solved as the time budget increases, simulated from one 120 s-timeout run.
Fig. 6. Evaluation of PC* solving Parikh automata problems generated by Ostrich.

Both PC* and nuXmv outperforms baseline on satisﬁable instances. On satisﬁable instances, nuXmv
and PC* have similar performance.
Baseline performs worse on satisﬁable instances because it executes a heuristic meant to detect
unsatisﬁability early, similar to [Janků and Turoňová 2020]. The heuristic is enabled since theimprovement is signiﬁcant compared to the extra cost.
Finally, in Figs. 6b, 7a and 7b and we compare runtimes for solved instances between the backends.
We see that nuXmv has a more even spread of runtimes up to 20 s, while both PC* and baseline
tend towards solving their instances quickly or not at all, though PC* does have a long tail ofoutlier instances that ﬁnish as the timeout increaseses. Notably, Fig. 7a shows that any instancesolved by baseline in 30 s is also solved by PC* in under 5 s.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

138:24

Amanda Stjerna and Philipp Rümmer

30

PC* vs baseline runtime, where timeout = 30s

25

PC*, runtime (s)PC*, runtime (s)

25
20
15
10
5
0

PC* vs nuXmv runtime, where timeout = 30s

30

20
15
10
5

0

5

10

15

20

baseline, runtime (s)2530(a) Per-instance runtime between baseline and PC*

0

0

5

10

15

20

nuXmv, runtime (s)2530(b) Per-instance runtime between nuXmv and PC*

Fig. 7. Per-instance duels between backends.
Table 3. Number of successful results within a timeout of 30 s. Instances solved by no backend within thetimeout (about half of the set) are omitted from the table.

backendkind

PC* baseline

nuXmv

Sat
Unsat

6587
16022

7532
13903

8
6193

8.1.1 Scalability. To investigate scaling we additionally execute 2 000 randomly sampled (without
replacement) benchmarks with a 120-second timeout. We add runs of PC* with clause learningand restarts disabled, and with only clause learning disabled to show the impact of Section 7.2.3,
and Section 7.2.2 respectively. These experiments are executed on a smaller machine, a six-core
AMD Ryzen 5 2600 but the same Java version. Their max heap size is set to 20 GB since this system
has less RAM. The baseline experiments are executed separately as only two threads.
A cactus plot showing the number of instances solved within a given timeout can be seen in
Fig. 6c. We see that PC* outperforms nuXmv in general but that nuXmv might scale better onvery long runtimes. This is likely due to two factors. First, nuXmv is more mature than PC*, andits more general model checking methods might pay oﬀ on more diﬃcult instances compared toproblem-speciﬁc methods. Second, for longer-running calculations clause learning as describedin Section 7.2.2 might matter more. As clause learning in Catra is rudimentary and generalises
poorly across product computations, there is a performance hit.
8.2 Evaluation in Ostrich
To evaluate the eﬀectiveness of PC* in a string solver, Catra was experimentally integrated
as the Parikh automata product solver into the string solver Ostrich version 1.3. Ostrich isan independently developed solver that participated in the recent SMT-COMP 20231 , winning
the single-query track for quantiﬁer-free strings (QF_S), as well as dominating other solvers on
unsatisﬁable string benchmarks [SMT-COMP 2023].
1 https://smt-comp.github.io/2023/participants/ostrich

Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

A Constraint Solving Approach to Parikh Images of Regular Languages

138:25

Table 4. Number of solved benchmarks in the set of quantifier-free strings with linear integer arithmetic
constraints (QF_SLIA) at SMT-COMP 2023. The numbers are from the competition results, except for CA-Str,
which is executed by us on the same cluster as the competition with the same resources, and the two virtual
portfolio solvers Ostrich+CA and Competition which aggregate the best results from Ostrich/CA-Str andall the competition results for non-Ostrich solvers respectively.

solverkind

CA-Str Competitors Ostrich 1.3 Ostrich+CA
6411
5566

Sat
Unsat

14207
7574

9586
7356

Z3-Noodler

9913
7389

cvc5

z3alpha7344 14069
5367 7377

13599
7298

QF_SLIA track of SMT-COMP 2023: solved benchmarks over time
20000
17500

nr solved

15000
12500

solverCA-StrCompetitors
Ostrich 1.3
Ostrich+CA
Z3-Noodler
cvc5
z3alpha

10000
7500
5000
2500
0

0

200

400

600

after (s)

800

1000

1200

Fig. 8. The number of instances solved in the QF_SLIA track of SMT-COMP 2023 as the time budget increases.

At SMT-COMP, Ostrich competed using a portfolio of three diﬀerent back-ends:• BW-Str: a backward-propagation-based solver, not utilising Parikh automata [Chen et al.
2019].
• ADT-Str: a solver based on algebraic data-types.
• CE-Str: a re-implementation of the Ostrich+ algorithm [Chen et al. 2020], using Parikh
automata and the encoding from [Verma et al. 2005] (referred to in this paper as baseline).
For our experiments, we modify the CE-Str solver to apply Catra (with PC* as its chosen backend)
instead of the previous baseline method, resulting in a new back-end CA-Str. Combining the resultsfrom SMT-COMP for Ostrich 1.3 with our new results running CA-Str we construct a virtual
portfolio Ostrich+CA that simulates running CA-Str as a fourth back-end to Ostrich. We similarly
combine the results of all non-Ostrich solvers to obtain the virtual portfolio solver Competition.
We extend the results of SMT-COMP 2023 with our modiﬁed Ostrich on the single-query
string solving with linear integer arithmetic constraints track (QF_SLIA). We picked QF_SLIA
since Ostrich already performed well on the other two string solving tracks. In fact, every solver,
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

138:26

Amanda Stjerna and Philipp Rümmer

including Ostrich, handled every benchmark in QF_SNIA within the timeout. Additionally, Parikhintersection problems would mainly be generated by Ostrich when solving constraints involving
integers, meaning that CA-Str would be of little or no help on the QF_S track.
We obtain the results by executing Ostrich 1.3 with CA-Str using the same benchmarking
infrastructure (the StarExec cluster) and conﬁguration that ran SMT-COMP 2023, combining our
new results for CA-Str with the published results of SMT-COMP 2023. 2 Where available, we use
the revised, out-of competition version of the results for solvers with bugs discovered during thecompetition, including Ostrich and Z3-Noodler. 3 Note that Z3-Noodler abstained on 70 instances,and thus has a lower total number of results. We used the parallel results for all solvers.
As can be seen from Table 4 and Fig. 8, integrating Catra as a back-end leads to gains both on
satisﬁable and unsatisﬁable problems. On satisﬁable problems, the combination Ostrich+CA isstill outperformed by cvc5 and z3alpha. On unsatisﬁable benchmarks, Ostrich+CA now narrowly
beats the other solvers squeezing past cvc5, which is promising given that Ostrich 1.3 (without
CA-Str), cvc5, and z3alpha all show very strong performance on this class of benchmarks.
These results are not unexpected. It is known that automata-based string solvers (Ostrich,
Z3-Noodler) tend to perform better on unsatisﬁable than on satisﬁable benchmarks, compared tosolvers that do not utilize automata and directly work on regular expressions (cvc5, z3alpha). The
computation of automata representations of regular constraints can be expensive, and might beunnecessary for satisﬁable formulas. In addition, the algorithm in Ostrich has stronger theoreticalcompleteness guarantees than cvc5 and Z3-Str, and ensuring completeness often has an adverse
eﬀect on performance in practice [Barbosa et al. 2022; Chen et al. 2019; Zheng et al. 2013].
The results show that PC* can be used to enhance the performance of an automaton-based
string solver. Moreover, the cactus plot in Table 4 illustrates that CA-Str is immediately useful,boosting the results for the Ostrich portfolio even at the ﬁrst datapoint (though marginally). These
results should be considered preliminary, however, as we believe that a deeper integration of Catra
into string solvers can lead to signiﬁcant performance gains. In particular, the integration layer iscurrently too shallow to allow Ostrich to learn clauses generated by Catra and additionally incurs
overhead from serialising and deserialising the current Parikh automata problem into Catra’s
input format.
8.3 Threats to Validity
The most obvious threat to validity would be an unsound implementation. To address this we havevalidated all reported solutions made by PC* with nuXmv. A previous version contained a racewith random restarts during product materialisation causing non-deterministic unsoundness in 0,7of instances. Additionally, both we and the artefact evaluation committee independently discovered a soundness issue in CA-Str on one instance in QF_S where the 20230329-automatark-lu/
instance08425.smt2 instance was incorrectly reported as Unsat. The underlying issue was that
Catra generated a too broad blocking clause for a product without transitions. We implemented aﬁx and re-evaluated all benchmarks. Performance was not measurably aﬀected.
Since addressing those bugs we have observed no further soundness issues in neither Catra nor
in CA-Str. Benchmarking results for both runs are included in the artefact of this paper, and show
virtually identical performance characteristics. We have additionally executed all of the benchmarks
on machines with widely diﬀerent performance characteristics and have observed the trends to berobust.
2 StarExec Job ID 59410, “SMT-COMP 2023 single query ﬁnal”, available at https://www.starexec.org/starexec/secure/details/

job.jsp?id=59410.
3 StarExec Job ID 59668, “SMT-COMP 2023 single query ﬁnal ﬁxed” available at https://www.starexec.org/starexec/secure/details/job.jsp?id=59668.
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

A Constraint Solving Approach to Parikh Images of Regular Languages

138:27The second threat to validity is our implementation of automata operations. As PC* by designoﬄoads some of the product computation work onto Princess, the baseline could be unfairly
disadvantaged by a slow automata product implementation. We believe this is not an issue sincesimilar performance issues with the baseline approach have been reported for other string solvers,
as well as for a previous implementation in Ostrich. Additionally, proﬁling shows that baseline
spends most of its time in Princess, suggesting that the automaton implementation is not thebottleneck. Finally, the diﬀerence in performance between PC* and baseline was unaﬀected bysigniﬁcant optimisation of the automata library, additionally strengthening this thesis.
9 CONCLUSION
In this paper, we have introduced a calculus to compute commutating operations on intersectionsof regular languages that we call PC*. We have evaluated it on 37 497 Parikh automata intersection
problems generated by the Ostrich+ string solver [Chen et al. 2020] solving the PyEx benchmark
suite [Reynolds et al. 2017] using our Parikh automata solver Catra.
Within Catra, PC* shows astonishing performance in terms of solve-time compared to thebaseline approach laid out in [Verma et al. 2005] when implemented on the same underlying
automated theorem prover (Princess, [Rümmer 2008]). It is also competitive with the nuXmv
model checker [Cavada et al. 2014], outperforming it on unsatisﬁable instances and generally
outperforming it for timeouts under 30 seconds with its advantage increasing drastically for evenshorter timeouts. 30 seconds would generally be considered a long timeout for our intended use assupporting infrastructure to a string constraint solver.
Future investigations involve two tracks. The ﬁrst one is integration into existing string solvers(wich Ostrich being a particularly promising candidate due to its shared use of Princess), andfurther adaptation to that use case. Closer inspection of the instances where we currently time out
should be useful to further improve our heuristics.
The second track for future improvements is the extension into other problem domains, including
other logics, model checking problems, as well as to more powerful automata such as transducers.
In principle, we can already express stronger constraints than Parikh automata due to our use of
an automated theorem prover which allows rich constraints on counter variables.
10DATA-AVAILABILITY STATEMENT

A reproduction package featuring all relevant logs and all benchmarked instances is available [Stjerna
and Rümmer 2024]. Catra and Ostrich are both available as living software under a 3-clause BSD license on GitHub at https://github.com/amandasystems/catra and https://github.com/uuveriﬁers/
ostrich respectively. A version of Ostrich using CA-Str is available in the cea-catra branch. Codefor the paper itself is available at https://github.com/amandasystems/oopsla-artefact.
ACKNOWLEDGMENTS
We thank the reviewers for insightful comments. This work was supported by the Swedish ResearchCouncil (VR) under grants 2018-04727 and 2021-06327, the Swedish Foundation for Strategic
Research (SSF) under the project WebSec (Ref. RIT17-0011), and the Wallenberg project UPDATE.
REFERENCES
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Bui Phi Diep, Lukáš Holík, Ahmed Rezine, and Philipp Rümmer.
2017. Flatten and conquer: a framework for eﬃcient analysis of string constraints. In Proceedings of the 38th ACM
SIGPLAN Conference on Programming Language Design and Implementation (Barcelona, Spain) (PLDI 2017). Association
for Computing Machinery, New York, NY, USA, 602–617. https://doi.org/10.1145/3062341.3062384
Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

138:28

Amanda Stjerna and Philipp Rümmer

Parosh Aziz Abdulla, Mohamed Faouzi Atig, Yu-Fang Chen, Lukáš Holík, Ahmed Rezine, Philipp Rümmer, and Jari Stenman.
2015. Norn: An SMT Solver for String Constraints. In Computer Aided Veriﬁcation, Daniel Kroening and Corina S.
Păsăreanu (Eds.). Springer International Publishing, Cham, 462–469. https://doi.org/10.1007/978-3-319-21690-4_29
Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir
Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli,
and Yoni Zohar. 2022. cvc5: A Versatile and Industrial-Strength SMT Solver. In Tools and Algorithms for the Construction
and Analysis of Systems, Dana Fisman and Grigore Rosu (Eds.). Springer International Publishing, Cham, 415–442.
https://doi.org/10.1007/978-3-030-99524-9_24
Murphy Berzish, Vijay Ganesh, and Yunhui Zheng. 2017. Z3str3: A String Solver with Theory-aware Heuristics. In 2017 Formal
Methods in Computer Aided Design (FMCAD). IEEE, Vienna, Austria, 55–59. https://doi.org/10.23919/FMCAD.2017.8102241
Murphy Berzish, Mitja Kulczynski, Federico Mora, Florin Manea, Joel D. Day, Dirk Nowotka, and Vijay Ganesh. 2021. An
SMT Solver for Regular Expressions and Linear Arithmetic over String Length. In Computer Aided Veriﬁcation, Alexandra
Silva and K. Rustan M. Leino (Eds.). Springer International Publishing, Cham, 289–312. https://doi.org/10.1007/978-3030-81688-9_14
Tevﬁk Bultan, Fang Yu, Muath Alkhalaf, and Abdulbaki Aydin. 2017. String Analysis for Software Veriﬁcation and Security.
Springer, Cham. https://doi.org/10.1007/978-3-319-68670-7
Michaël Cadilhac, Alain Finkel, and Pierre McKenzie. 2011. On the expressiveness of Parikh automata and related models.
arXiv:1101.1547 [cs.FL]
Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover,
Marco Roveri, and Stefano Tonetta. 2014. The nuXmv Symbolic Model Checker. In Computer Aided Veriﬁcation, Armin
Biere and Roderick Bloem (Eds.). Springer International Publishing, Cham, 334–342. https://doi.org/10.1007/978-3-31908867-9_22
Taolue Chen, Matthew Hague, Jinlong He, Denghang Hu, Anthony Widjaja Lin, Philipp Rümmer, and Zhilin Wu. 2020.
A Decision Procedure for Path Feasibility of String Manipulating Programs with Integer Data Type. In AutomatedTechnology for Veriﬁcation and Analysis, Dang Van Hung and Oleg Sokolsky (Eds.). Springer International Publishing,
Cham, 325–342. https://doi.org/10.1007/978-3-030-59152-6_18
Taolue Chen, Matthew Hague, Anthony W. Lin, Philipp Rümmer, and Zhilin Wu. 2019. Decision procedures for pathfeasibility of string-manipulating programs with complex operations. Proc. ACM Program. Lang. 3, POPL, Article 49 (jan2019), 30 pages. https://doi.org/10.1145/3290362
Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Eﬃcient SMT Solver. In Tools and Algorithms for the Construction andAnalysis of Systems, C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 337–340.
https://doi.org/10.1007/978-3-540-78800-3_24
Javier Esparza, Pierre Ganty, Stefan Kiefer, and Michael Luttenberger. 2011. Parikh’s theorem: A simple and direct automaton
construction. Inform. Process. Lett. 111, 12 (2011), 614–619. https://doi.org/10.1016/j.ipl.2011.03.019
Diego Figueira and Leonid Libkin. 2015. Path Logics for Querying Graphs: Combining Expressiveness and Eﬃciency. In
2015 30th Annual ACM/IEEE Symposium on Logic in Computer Science. IEEE, Kyoto, Japan, 329–340. https://doi.org/10.
1109/LICS.2015.39
Melvin C. Fitting. 1996. First-Order Logic and Automated Theorem Proving (2nd ed.). Springer-Verlag, New York, NY, USA.
John Harrison. 2009. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, Shaftesbury Road,
Cambridge, UK.
Lukáš Holík, Petr Janků, Anthony W. Lin, Philipp Rümmer, and Tomáš Vojnar. 2017. String constraints with concatenationand transducers solved eﬃciently. Proc. ACM Program. Lang. 2, POPL, Article 4 (dec 2017), 32 pages. https://doi.org/10.
1145/3158092
Petr Janků and Lenka Turoňová. 2020. Solving String Constraints with Approximate Parikh Image. In Computer Aided
Systems Theory – EUROCAST 2019, Roberto Moreno-Díaz, Franz Pichler, and Alexis Quesada-Arencibia (Eds.). Springer
International Publishing, Cham, 491–498. https://doi.org/10.1007/978-3-030-45093-9_59
Juhani Karhumäki. 1980. Generalized Parikh mappings and homomorphisms. Information and Control 47, 3 (1980), 155–165.
https://doi.org/10.1016/S0019-9958(80)90493-3
Felix Klaedtke and Harald Rueß. 2002. Parikh Automata and Monadic Second-Order Logics with Linear Cardinality Constraints.
Technical Report 177. Albert-Ludwigs-Universität Freiburg. https://tr.informatik.uni-freiburg.de/reports/report177/
report00177.ps.gz
Dexter C. Kozen. 1997. Automata and computability. Springer, New York.
Giovanna J. Lavado, Giovanni Pighizzini, and Shinnosuke Seki. 2013. Converting nondeterministic automata and context-freegrammars into Parikh equivalent one-way and two-way deterministic automata. Information and Computation 228-229(2013), 1–15. https://doi.org/10.1016/j.ic.2013.06.003
Michael Luby, Alistair Sinclair, and David Zuckerman. 1993. Optimal speedup of Las Vegas algorithms. Inform. Process. Lett.
47, 4 (1993), 173–180. https://doi.org/10.1016/0020-0190(93)90029-9

Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.

A Constraint Solving Approach to Parikh Images of Regular Languages

138:29Kimbal Marriott and Peter Stuckey. 1998. Programming with Constraints: An Introduction. The MIT Press, Cambridge, MA,
USA. https://doi.org/10.7551/mitpress/5625.001.0001
Federico Mora, Murphy Berzish, Mitja Kulczynski, Dirk Nowotka, and Vijay Ganesh. 2021. Z3str4: A Multi-armed String
Solver. In Formal Methods, Marieke Huisman, Corina Păsăreanu, and Naijun Zhan (Eds.). Springer International Publishing,
Cham, 389–406. https://doi.org/10.1007/978-3-030-90870-6_21
Rohit J. Parikh. 1966. On Context-Free Languages. J. ACM 13, 4 (oct 1966), 570–581. https://doi.org/10.1145/321356.321364
Rodrigo Raya. 2023. Decision Procedures for Power Structures. Ph. D. Dissertation. EPFL, Lausanne. https://doi.org/10.5075/epﬂthesis-10546
Andrew Reynolds, Maverick Woo, Clark Barrett, David Brumley, Tianyi Liang, and Cesare Tinelli. 2017. Scaling Up DPLL(T)String Solvers Using Context-Dependent Simpliﬁcation. In Computer Aided Veriﬁcation, Rupak Majumdar and Viktor
Kunčak (Eds.). Springer International Publishing, Cham, 453–474. https://doi.org/10.1007/978-3-319-63390-9_24
Philipp Rümmer. 2008. A Constraint Sequent Calculus for First-Order Logic with Linear Integer Arithmetic. In Logic for
Programming, Artiﬁcial Intelligence, and Reasoning, Iliano Cervesato, Helmut Veith, and Andrei Voronkov (Eds.). Springer
Berlin Heidelberg, Berlin, Heidelberg, 274–289. https://doi.org/10.1007/978-3-540-89439-1_20
Prateek Saxena, Devdatta Akhawe, Steve Hanna, Feng Mao, Stephen McCamant, and Dawn Song. 2010. A Symbolic
Execution Framework for JavaScript. In 2010 IEEE Symposium on Security and Privacy. IEEE, Oakland, CA, USA, 513–528.
https://doi.org/10.1109/SP.2010.38
Helmut Seidl, Thomas Schwentick, Anca Muscholl, and Peter Habermehl. 2004. Counting in Trees for Free. In Automata,
Languages and Programming, Josep Díaz, Juhani Karhumäki, Arto Lepistö, and Donald Sannella (Eds.). Springer Berlin
Heidelberg, Berlin, Heidelberg, 1136–1149. https://doi.org/10.1007/978-3-540-27836-8_94
Rani Siromoney and V. Rajkumar Dare. 1985. A generalization of the Parikh vector for ﬁnite and inﬁnite words. In Foundationsof Software Technology and Theoretical Computer Science, S. N. Maheshwari (Ed.). Springer Berlin Heidelberg, Berlin,
Heidelberg, 290–302.
SMT-COMP. 2023. SMT-COMP 2023 Results. The SMT Steering Committee. https://smt-comp.github.io/2023/results.html
Daniel Stan and Anthony W. Lin. 2021. Regular Model Checking Approach to Knowledge Reasoning over Parameterized
Systems. In Proceedings of the 20th International Conference on Autonomous Agents and MultiAgent Systems (Virtual Event,
United Kingdom) (AAMAS ’21). International Foundation for Autonomous Agents and Multiagent Systems, Richland, SC,
1254–1262. https://doi.org/10.5555/3463952.3464097
Caleb Stanford, Margus Veanes, and Nikolaj Bjørner. 2021. Symbolic Boolean Derivatives for Eﬃciently Solving Extended
Regular Expression Constraints. In PLDI 21. Association for Computing Machinery, New York, NY, USA, 620–635.
https://doi.org/10.1145/3453483.3454066
Amanda Stjerna and Philipp Rümmer. 2024. Reproduction Package for ‘A Constraint Solving Approach to Parikh Images ofRegular Languages’. https://doi.org/10.5281/zenodo.10796555
Kumar Neeraj Verma, Helmut Seidl, and Thomas Schwentick. 2005. On the Complexity of Equational Horn Clauses. In
Automated Deduction – CADE-20, Robert Nieuwenhuis (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 337–352.
https://doi.org/10.1007/11532231_25
Yunhui Zheng, Xiangyu Zhang, and Vijay Ganesh. 2013. Z3-str: a z3-based string solver for web application analysis. In
Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering (Saint Petersburg, Russia) (ESEC/FSE
2013). Association for Computing Machinery, New York, NY, USA, 114–124. https://doi.org/10.1145/2491411.2491456

Received 21-OCT-2023; accepted 2024-02-24

Proc. ACM Program. Lang., Vol. 8, No. OOPSLA1, Article 138. Publication date: April 2024.