Das Kapitel stellt das Crest-Tool vor, eine hochmoderne Software zur automatisierten Analyse logisch beschränkter Term-Rewrite-Systeme (LCTRS). Es beginnt mit der Erklärung der Bedeutung von LCTRS in der Programmanalyse und ihrer Erweiterung traditioneller Term-Rewrite-Systeme mit logischen Beschränkungen, die von SMT-Lösern gehandhabt werden. Anschließend geht der Text auf die wichtigsten Merkmale von Crest ein, einschließlich seiner Unterstützung für fortgeschrittene Konfluenztechniken, automatisierte Nichtkonfluenz- und Terminierungsanalysen und Unterstützung für Bitvektoren fester Größe. Die Architektur und Automatisierungsdetails des Tools werden diskutiert, wobei die Verwendung von Haskell und die Integration mit SMT-Solvern wie Z3 hervorgehoben werden. In diesem Kapitel werden auch neue Transformationstechniken zur Stärkung von Zusammenflusskonflikten vorgestellt, die Macht beweisen, wie etwa die Aufteilung kritischer Paare und die Verschmelzung beschränkter Umschreibregeln. Umfangreiche experimentelle Auswertungen zeigen die Stärke und Effizienz des Kamms und vergleichen ihn mit anderen Werkzeugen wie Strg, CRaris und Cora. Das Kapitel schließt mit Vorschlägen für zukünftige Erweiterungen, einschließlich der Anpassung leistungsstarker Methoden vom einfachen Umschreiben von Begriffen an die eingeschränkte Umgebung und der Entwicklung einer benutzerfreundlichen Weboberfläche. Die Open-Source-Verfügbarkeit von Crest und seine detaillierte Dokumentation machen es zu einer wertvollen Ressource für Forscher und Praktiker im Bereich des Umschreibens von Begriffen und der Programmanalyse.
KI-Generiert
Diese Zusammenfassung des Fachinhalts wurde mit Hilfe von KI generiert.
Abstract
We present crest, a tool for automatically proving (non-) confluence and termination of logically constrained rewrite systems. We compare crest to other tools for logically constrained rewriting. Extensive experiments demonstrate the promise of crest.
Hinweise
This research is funded by the Austrian Science Fund (FWF) project I5943.
1 Introduction
Term rewriting is a simple Turing-complete model of computation. Properties like confluence and termination are of key interest and numerous powerful tools have been developed for their analysis. Logically constrained term rewrite systems (LCTRSs for short) constitute a natural extension of term rewrite systems (TRSs) in which rules are equipped with logical constraints that are handled by SMT solvers, thereby avoiding the cumbersome encoding of operations on e.g. integers and bit vectors in term rewriting. LCTRSs, introduced by Kop and Nishida in 2013 [25], are useful for program analysis [8, 13, 23, 40]. They also developed Ctrl [26, 27], a tool for LCTRSs specializing in termination analysis and equivalence testing. Later, techniques for completion [39] and non-termination [33] analysis were added.
In this paper we describe crest, the Constrained REwriting Software Tool. The tool crest was first announced in [34] with support for a small number of confluence techniques. The new version described here includes numerous extensions:
more advanced confluence techniques (introduced in [35]),
automated non-confluence and termination analysis,
support for fixed-sized bit vectors,
transformation techniques based on splitting critical pairs and merging constrained rewrite rules, to further boost the confluence proving power.
The remainder of the paper is organized as follows. In the next section we recall important definitions pertaining to LCTRSs. Section 3 summarizes the main confluence and termination techniques implemented in crest. Automation details are presented in Section 4. The new transformation techniques are described in Section 5. In Section 6 we present our experiments, before concluding in Section 7 with suggestions for future extensions. We conclude this introductory section with mentioning other tools for LCTRSs.
Related Tools. We already mentioned Ctrl1 which until 2023 was the only tool capable of analyzing confluence and termination of LCTRSs. It supports termination analysis [24], completion techniques [39], rewriting induction for equivalence testing of LCTRSs [13], and basic confluence analysis [27]. Unfortunately, it is neither actively maintained nor very well documented, which is one reason why the development of crest was started. Moreover, a branch2 of the automated resource analysis tool TcT [4] performs complexity analysis on LCTRSs based on [40]. RMT by Ciobâcă et al. [7, 8] is a newer tool for program analysis based on a variation of LCTRSs.
In the 2024 edition of the Confluence Competition3 the tool CRaris,4 developed by Nishida and Kojima, made its appearance. The tool implements weak orthogonality [25] and the Knuth–Bendix criterion for terminating LCTRSs [34]. For termination, it implements the dependency pair framework [24] and the singleton self-looping removal processor [29] for LCTRSs with bit vectors.
Anzeige
Also in 2024 Guo et al. [14, 15] announced Cora, a new open-source tool for termination analysis of logically constrained simply-typed term rewrite systems, which serve as a high-order generalization of LCTRSs. It employs static dependency pairs [28] with several base methods, including a variant of the higher-order recursive path order [18].
2 Logically Constrained Term Rewriting
Familiarity with the basic notions of term rewriting [5] is assumed. We assume a many-sorted signature \(\mathcal {F}= \mathcal {F}_{\textsf{te}}\cup \mathcal {F}_{\textsf{th}}\) consisting of term and theory symbols together with a countably infinite set of variables \(\mathcal {V}\). For every sort \(\iota \) in \(\mathcal {F}_{\textsf{th}}\) we have a non-empty set \(\mathcal {V}\textsf{al}_\iota \subseteq \mathcal {F}_{\textsf{th}}\) of value symbols, such that all \(c \in \mathcal {V}\textsf{al}_\iota \) are constants of sort \(\iota \). We demand \(\mathcal {F}_{\textsf{te}}\cap \mathcal {F}_{\textsf{th}}\subseteq \mathcal {V}\textsf{al}\) where \(\mathcal {V}\textsf{al}= \bigcup _\iota \mathcal {V}\textsf{al}_\iota \). The set of terms constructed from function symbols in \(\mathcal {F}\) and variables in \(\mathcal {V}\) is by \(\mathcal {T}(\mathcal {F},\mathcal {V})\). A term in \(\mathcal {T}(\mathcal {F}_{\textsf{th}},\mathcal {V})\) is called a logical term. Ground logical terms are mapped to values by an interpretation \(\mathcal {J}\): \([\![{f({t_1},\dots ,{t_{n}})}]\!] = f_\mathcal {J}([\![{t_1}]\!],\dots ,[\![{t_n}]\!])\). Logical terms of sort \(\textsf{bool}\) are called constraints. A constraint \(\varphi \) is valid if \([\![{\varphi \gamma }]\!] = \top \) for all substitutions \(\gamma \) such that \(\gamma (x) \in \mathcal {V}\textsf{al}\) for all \(x \in \mathcal {V}\textsf{ar}(\varphi )\). Positions are sequences of positive integers to indicate subterms. The root of a term is denoted by the empty string \(\epsilon \). For a term s, its subterm at position p is given by \(s|_p\). The set of positions in \(s \in \mathcal {T}(\mathcal {F},\mathcal {V})\) is denoted by \(\mathcal {P}\textsf{os}(s)\) whereas \(\mathcal {P}\textsf{os}_\mathcal {F}(s)\) is restricted to positions with function symbols in s. We write \(\mathcal {V}\textsf{ar}(s)\) for the set of variables in s. A constrained rewrite rule is a triple \(\rho :\ell \rightarrow r~[\varphi ]\) where \(\ell , r \in \mathcal {T}(\mathcal {F},\mathcal {V})\) are terms of the same sort such that \(\textsf{root}(\ell ) \in \mathcal {F}_{\textsf{te}}\setminus \mathcal {F}_{\textsf{th}}\) and \(\varphi \) is a constraint. We denote the set \(\mathcal {V}\textsf{ar}(\varphi ) \cup (\mathcal {V}\textsf{ar}(r) \setminus \mathcal {V}\textsf{ar}(\ell ))\) of logical variables in \(\rho \) by \(\mathcal {L}\mathcal {V}\textsf{ar}(\rho )\). We write \(\mathcal {E}\mathcal {V}\textsf{ar}(\rho )\) for the set \(\mathcal {V}\textsf{ar}(r) \setminus (\mathcal {V}\textsf{ar}(\ell ) \cup \mathcal {V}\textsf{ar}(\varphi ))\) of extra variables. A set of constrained rewrite rules is called an LCTRS. A substitution \(\sigma \)respects a rule \(\rho :\ell \rightarrow r~[\varphi ]\), denoted by \(\sigma \vDash \rho \), if \(\mathcal {D}\textsf{om}(\sigma ) \subseteq \mathcal {V}\textsf{ar}(\rho )\), \(\sigma (x) \in \mathcal {V}\textsf{al}\) for all \(x \in \mathcal {L}\mathcal {V}\textsf{ar}(\rho )\), and \(\varphi \sigma \) is valid. Moreover, a constraint \(\varphi \) is respected by \(\sigma \), denoted by \(\sigma \vDash \varphi \), if \(\sigma (x) \in \mathcal {V}\textsf{al}\) for all \(x \in \mathcal {V}\textsf{ar}(\varphi )\) and \(\varphi \sigma \) is valid. We call \(f({x_1},\dots ,{x_{n}}) \rightarrow y~[y = f({x_1},\dots ,{x_{n}})]\) with a fresh variable y and \(f \in \mathcal {F}_{\textsf{th}}\setminus \mathcal {V}\textsf{al}\) a calculation rule. The set of all calculation rules induced by the signature \(\mathcal {F}_{\textsf{th}}\) of an LCTRS \(\mathcal {R}\) is denoted by \(\mathcal {R}_\textsf{ca}\) and we abbreviate \(\mathcal {R}\cup \mathcal {R}_\textsf{ca}\) to \(\mathcal {R}_\textsf{rc}\). A rewrite step \(s \rightarrow _{\mathcal {R}}t\) satisfies \(s|_p = \ell \sigma \) and \(t = s[r\sigma ]_p\) for some position p, constrained rewrite rule \(\rho :\ell \rightarrow r~[\varphi ]\) in \(\mathcal {R}_\textsf{rc}\), and substitution \(\sigma \) such that \(\sigma \vDash \rho \).
A constrained term is a pair \(s~[\varphi ]\) consisting of a term s and a constraint \(\varphi \). Two constrained terms \(s~[\varphi ]\) and \(t~[\psi ]\) are equivalent, denoted by \(s~[\varphi ] \sim t~[\psi ]\), if for every substitution \(\gamma \vDash \varphi \) with \(\mathcal {D}\textsf{om}(\gamma ) = \mathcal {V}\textsf{ar}(\varphi )\) there is some substitution \(\delta \vDash \psi \) with \(\mathcal {D}\textsf{om}(\delta ) = \mathcal {V}\textsf{ar}(\psi )\) such that \(s\gamma = t\delta \), and vice versa. Let \(s~[\varphi ]\) be a constrained term. If \(s|_p = \ell \sigma \) for some constrained rewrite rule \(\rho :\ell \rightarrow r~[\psi ] \in \mathcal {R}_\textsf{rc}\), position p, and substitution \(\sigma \) such that \(\sigma (x) \in \mathcal {V}\textsf{al}\cup \mathcal {V}\textsf{ar}(\varphi )\) for all \(x \in \mathcal {L}\mathcal {V}\textsf{ar}(\rho )\), \(\varphi \) is satisfiable and \(\varphi \Rightarrow \psi \sigma \) is valid then \(s~[\varphi ] \rightarrow _{\mathcal {R}}s[r\sigma ]_p~[\varphi ]\). The rewrite relation
on constrained terms is defined as \(\sim \cdot \rightarrow _{\mathcal {R}}\cdot \sim \) and
indicates that the rewrite step in
takes place at position p in s. Similarly, we write
if the position in the rewrite step is below position p. We illustrate some of these concepts by means of a simple example which models the computation of the maximum of two integers.
Example 1
Consider the LCTRS \(\mathcal {R}\) over the theory Ints with the rules
Here x and y are logical variables in both rules. There are no extra variables. The symbol \(\textsf{max}\) is the only term symbol. The theory symbols depend on the definition of Ints. As the goal is automation this usually consists of non-linear integer arithmetic as specified in the respective SMT-LIB theory.5
By applying the calculation rule \(x_1 + x_2 \rightarrow y~[y = x_1 + x_2]\) with substitution \(\{x_1 \mapsto \textsf{3}, x_2 \mapsto \textsf{2}, y \mapsto \textsf{5}\}\) followed by rule \(\alpha \) we obtain
One-step rewriting, i.e., rewriting a term using a single rule, was introduced above. The sufficient criteria for confluence, highlighted in the next section, heavily rely on the notation of parallel (
) and multi-step (
) rewriting following [35, Definition 3] and [34, Definition 8]. The former is capable of applying several rules at parallel positions in a step while the latter additionally allows recursive steps within the used matching substitutions of rules. A rewrite sequence consists of consecutive rewrite steps, independent of which kind. The reflexive and transitive closure of \(\rightarrow \) is denoted by \(\rightarrow ^{*}\). Moreover, for arbitrary terms s and t we write \(s \leftrightarrow t\) if \(s \mathrel {({\leftarrow } \cup {\rightarrow })} t\) and \(s \downarrow t\) if there exists a term u such that \(s \rightarrow ^{*} u \mathrel {^{*}{\leftarrow }} t\).
3 Confluence and Termination
Termination and confluence are well-known properties in static program analysis. Both properties are in general undecidable. With respect to (logically constrained) term rewriting, a program is terminating whenever it does not admit an infinite rewrite sequence. Confluence states that \(s \downarrow t\) whenever \(t \mathrel {^{*}{\leftarrow }} s \rightarrow ^{*} u\), for all terms s, t and u. Naively checking the properties is obviously not feasible. In (logically constrained) term rewriting there exist sufficient criteria that guarantee that these properties are satisfied for a given program. In the following we highlight key components of confluence and termination analysis for logically constrained rewrite systems.
The confluence methods implemented in crest are based on (parallel) critical pairs. These are defined as follows. Given a constrained rewrite rule \(\rho \), we write \(\mathcal{E}\mathcal{C}_\rho \) for \(\bigwedge \{x = x \mid x \in \mathcal {E}\mathcal {V}\textsf{ar}(\rho )\}\). An overlap of an LCTRS \(\mathcal {R}\) is a triple \(\langle \rho _1, p, \rho _2 \rangle \) with rules \(\rho _1:\ell _1 \rightarrow r_1~[\varphi _1]\) and \(\rho _2:\ell _2 \rightarrow r_2~[\varphi _2]\), satisfying the following conditions: (1) \(\rho _1\) and \(\rho _2\) are variable-disjoint variants of rewrite rules in \(\mathcal {R}_\textsf{rc}\), (2) \(p \in \mathcal {P}\textsf{os}_\mathcal {F}(\ell _2)\), (3) \(\ell _1\) and \(\ell _2|_p\) unify with mgu \(\sigma \) such that \(\sigma (x) \in \mathcal {V}\textsf{al}\cup \mathcal {V}\) for all \(x \in \mathcal {L}\mathcal {V}\textsf{ar}(\rho _1) \cup \mathcal {L}\mathcal {V}\textsf{ar}(\rho _2)\), (4) \(\varphi _1\sigma \wedge \varphi _2\sigma \) is satisfiable, and (5) if \(p = \epsilon \) then \(\rho _1\) and \(\rho _2\) are not variants, or \(\mathcal {V}\textsf{ar}(r_1) \nsubseteq \mathcal {V}\textsf{ar}(\ell _1)\). In this case we call \(\ell _2\sigma [r_1\sigma ]_p \approx r_2\sigma ~ [\varphi _1\sigma \wedge \varphi _2\sigma \wedge \psi \sigma ]\) a constrained critical pair (CCP) obtained from the overlap \(\langle \rho _1, p, \rho _2 \rangle \). Here \(\psi = \mathcal{E}\mathcal{C}_{\rho _1} \wedge \mathcal{E}\mathcal{C}_{\rho _2}\). The peak
with \(\varPhi = (\varphi _1 \wedge \varphi _2 \wedge \psi )\sigma \), from which the constrained critical pair originates, is called a constrained critical peak. The set of all constrained critical pairs of \(\mathcal {R}\) is denoted by \(\textsf{CCP}(\mathcal {R})\). A constrained equation \(s \approx t~[\varphi ]\) is trivial if \(s\sigma = t\sigma \) for every substitution \(\sigma \) with \(\sigma \vDash \varphi \). The trivial equations from \(\mathcal{E}\mathcal{C}_{\rho }\) are used in order to prevent loosing the information which (extra) variables are logical variables in the underlying rules of a CCP.
Example 2
Let us extend the LCTRS \(\mathcal {R}\) from Example 1 with an additional rule modeling the commutativity of \(\textsf{max}\):
There are six constrained critical pairs, including the following two:
$$\begin{aligned} x &\approx y~[x \geqslant y \wedge y \geqslant x] & x &\approx \max (y,x)~[x \geqslant y] \end{aligned}$$
The left one is trivial, the one on the right becomes trivial after one rewrite step: \(x \approx \max (y,x)~[x \geqslant y] \rightarrow x \approx x~[x \geqslant y]\). The remaining four pairs can be rewritten similarly.
Restricting the way in which constrained critical peaks are rewritten into trivial ones, yields different sufficient conditions for confluence of (left-)linear LCTRSs. We state the conditions below but refer to [25, 34, 35] for precise definitions:
joinable critical pairs for terminating LCTRSs ([34, Corollary 4]).
(C3)
strong closedness for linear LCTRSs ([34, Theorem 2]),
(C4)
(almost) parallel closedness for left-linear LCTRSs ([34, Theorem 4]),
(C5)
(almost) development closedness for left-linear LCTRSs ([35, Corollary 1]).
The final confluence criterion implemented in crest is based on parallel critical pairs. Let \(\mathcal {R}\) be an LCTRS, \(\rho :\ell \rightarrow r~[\varphi ]\) a rule in \(\mathcal {R}_\textsf{rc}\), and \(P \subseteq \mathcal {P}\textsf{os}_\mathcal {F}(\ell )\) a non-empty set of parallel positions. For every \(p \in P\) let \(\rho _p:\ell _p \rightarrow r_p~[\varphi _p]\) be a variant of a rule in \(\mathcal {R}_\textsf{rc}\). Let \(\psi = \mathcal{E}\mathcal{C}_{\rho } \wedge \bigwedge _{p \in P} \mathcal{E}\mathcal{C}_{\rho _p}\) and \(\varPhi = \varphi \sigma \wedge \psi \sigma \wedge \bigwedge _{p \in P} \varphi _p\sigma \). The peak
forms a constrained parallel critical pair\(\ell \sigma [r_p\sigma ]_{p \in P} \approx r\sigma ~[\varPhi ]\) if the following conditions are satisfied:
1.
\(\mathcal {V}\textsf{ar}(\rho _1) \cap \mathcal {V}\textsf{ar}(\rho _2) = \varnothing \) for different rules \(\rho _1\) and \(\rho _2\) in \(\{\rho \} \cup \{\rho _p \mid p \in P\}\),
2.
\(\sigma \) is an mgu of \(\{\ell _p = \ell |_p \mid p \in P\}\) such that \(\sigma (x) \in \mathcal {V}\textsf{al}\cup \mathcal {V}\) for all \(x \in \mathcal {L}\mathcal {V}\textsf{ar}(\rho ) \cup \bigcup _{p \in P} \mathcal {L}\mathcal {V}\textsf{ar}(\rho _p)\),
3.
\(\varphi \sigma \wedge \bigwedge _{p \in P} \varphi _p\sigma \) is satisfiable, and
4.
if \(P = \{\epsilon \}\) then \(\rho _\epsilon \) is not a variant of \(\rho \) or \(\mathcal {V}\textsf{ar}(r) \nsubseteq \mathcal {V}\textsf{ar}(\ell )\).
A constrained peak forming a constrained parallel critical pair is called a constrained parallel critical peak. The set of all constrained parallel critical pairs of \(\mathcal {R}\) is denoted by \(\textsf{CPCP}(\mathcal {R})\). The following sufficient condition for confluence is reported in ([35, Corollary 2]):
(C6)
parallel closedness of parallel critical pairs for left-linear LCTRSs.
Conditions (C5) and (C6) do not subsume each other. Both generalize conditions (C1) – (C4). All these confluence criteria try to find a specific closing rewrite sequence starting from a constrained (parallel) critical pair—which is seen as a constrained equation—to a trivial constrained equation. For example, parallel closedness in (C4) involves showing that each constrained critical pair \(s \approx t~[\varphi ]\) can be rewritten into a trivial constrained equation using a single parallel step
. Note that only the left part (s) is rewritten here and \(s' \approx t~[\varphi ]\) is a trivial constrained equation. For (finite) terminating TRSs, confluence is decided by rewriting critical pairs to normal form [20]. For terminating LCTRSs confluence—even for a decidable theory—is undecidable [35], but rewriting constrained critical pairs to normal forms is still of value. This is used in (C2) above. We need however to adapt the notion of normal form for constrained terms.
Example 3
The LCTRS \(\mathcal {R}\) over the theory \(\textsf{Ints}\) with rewrite rules
admits one (modulo symmetry) constrained critical pair:
None of the rules above are applicable, so this non-trivial constrained critical pair is in normal form with respect to \(\rightarrow _{\mathcal {R}}\), but it would be wrong to conclude that \(\mathcal {R}\) is not confluent; all substitutions \(\sigma \) that satisfy the constraint \(x \geqslant \textsf{1} \wedge x \leqslant \textsf{2}\) allow us to rewrite \((\textsf{g}(x) \approx \textsf{h}(x))\sigma \) to the trivial equations \(\textsf{a} \approx \textsf{a}\) or \(\textsf{b} \approx \textsf{b}\).
Definition 1
Given an LCTRS \(\mathcal {R}\), a constrained term \(s~[\varphi ]\) is in normal form if and only if for all substitutions \(\sigma \) with \(\sigma \vDash \varphi \) we have \(s\sigma \rightarrow _{\mathcal {R}}t\) for no term t.
Note that the constrained critical pair in Example 3 is not in normal form according to this definition. We present a simple sufficient condition for non-confluence. The easy proof can be found in the appendix of [37].
Lemma 1
An LCTRS is non-confluent if there exists a constrained critical pair that rewrites to a non-trivial constrained equation in normal form.
We will resume the analysis of Example 3 in Section 5. Termination plays an important role in the analysis of LCTRSs. crest implements the following methods reported in the papers by Kop and Nishida [24, 25]:
Method (T1) computes the strongly connected components in the dependency graph, and transforms the input LCTRS into so-called DP problems, which can be analyzed independently. It lies at the heart of the dependency pair framework [19] implemented in most termination tools for TRSs. Methods (T2) and (T4) are LCTRS variants of well-known methods for TRSs [3, 9]. Two further methods implemented in Ctrl are ported to crest:
(T5)
subterm criterion
(T6)
special value criterion
While (T5) is a well-known termination method for DP problems originating from TRSs [17], (T3) and (T6) are specific to LCTRSs. Method (T5) operates on the syntactic structure of dependency pairs and ignores the constraints. In method (T3) dependency pair symbols are also projected to a direct argument but then a strict decrease with respect to the constraint is required. For example, the rule \(\textsf{f}(x) \rightarrow \textsf{f}(x - 1)~[x > 0]\) cannot be handled by (T5), but as \(x > 0\) implies the strict decrease \(x \succ x - 1\) for a suitable well-founded relation \(\succ \), (T3) applies. Method (T6) is an extension of (T3) in which linear combinations of arguments are considered. Methods (T3) and (T6) are adapted to the higher-order LCTRS setting in [14, Sections 4.2 & 4.3].
4 Automation
Our tool crest is written in Haskell and the current version consists of roughly 12000 lines of code. Core modules like SMT solving use a fork of the simple-smt package6 and the rewriting modules are inspired by the term-rewriting package.7 In the following we provide some details of the key components.
Input Format.crest operates on LCTRSs in the new ARI format8 [1] adopted by the Confluence Competition (CoCo) and also partly by the Termination Competition.9 Problems in the ARI database are given a unique number which we will use throughout this paper to address specific LCTRSs. An example problem is given in Fig. 1. The ARI database format requires sort annotations for variables appearing as an argument of a polymorphic predicate. If this sort can be inferred at a different position then this can be ignored for crest. For example, consider the rule \(\textsf{f}(x = y,x) \rightarrow z~[z = x + \textsf{1}]\) with \(\textsf{f}:\textsf{Bool} \rightarrow \textsf{Int} \rightarrow \textsf{Int}\), \({+}:\textsf{Int} \rightarrow \textsf{Int} \rightarrow \textsf{Int}\) and \({=}:A \rightarrow A \rightarrow \textsf{Bool}\) with a polymorphic sort A. In the ARI database all variables need concrete sort annotation. For crest no sort annotation is necessary as all the sorts of variables can be inferred from the sort of \(\textsf{f}\).
Fig. 1.
ARI file 1528 (without sort annotations and meta information).
Theory symbols are those that are defined in a specific SMT-LIB theory, however, for fixed-sized bit vectors crest additionally supports function symbols defined in the SMT-LIB logic QF_BV.10 In addition to LCTRSs also plain TRSs and many-sorted TRSs are supported.
Pre-Processing. After parsing its input and assigning already known sorts to function symbols and variables we apply a basic type inference algorithm. Some function symbols in the core theory, which provides basic boolean functions, like “\(=\)” have a polymorphic sort. Therefore we need to infer unknown sorts in order to obtain a fully sorted LCTRS. This is required as sort information must be present for the declaration of variables in the SMT solver. During the parsing phase crest parses the respective theory from an internal representation of the SMT-LIB specification. Currently the theory of integers, reals, fixed-sized bit vectors and a combination of integers and reals are supported. Subsequently crest preprocesses the LCTRS by moving values in the left-hand sides of the rewrite rules into the constraints (by applying the transformation described in [34, Definition 13]). Afterwards it merges as many rules as possible following Definition 3 in Section 5.
Rewriting. One of the key components is the rewriting module which provides functionality to perform rewriting on constrained terms. This module computes rewrite sequences of arbitrary length, using single steps, parallel rewrite steps [35, Definition 7] and multisteps [35, Definition 5]. Calculation steps are modeled in an obvious way; whenever we have a term \(s[f({s_1},\dots ,{s_{n}})]~[\varphi ]\) with \({s_1},\dots ,{s_{n}} \in \mathcal {V}\textsf{al}\cup \mathcal {V}\textsf{ar}(\varphi )\) and \(f \in \mathcal {F}_{\textsf{th}}\), then we produce \(s[x]~[\varphi \wedge x = f({s_1},\dots ,{s_{n}})]\) for a fresh variable x. In some cases single rule steps need more care because of the lack of equivalence steps in rewrite sequences. For rules with variables that do not occur in the left-hand side, the matching substitution of the left-hand side does not provide an instantiation. However, those variables are logical and need to be instantiated with values. This is achieved by adding the constraint of the rule and its extra variables to the resulting constrained term after it has been confirmed that for those variables an instantiation exists. We illustrate this in the following example.
Example 4
Consider the constrained rule \(\rho :\textsf{f}(x) \rightarrow y~[x \geqslant 0 \wedge x > y]\), the constrained term \(\textsf{f}(z)~[z = \textsf{2}]\) and the matching substitution \(\{x \mapsto z\}\) between the left-hand side of \(\rho \) and \(\textsf{f}(z)\). The variable y is not part of the matching substitution and thus crest rewrites \(\textsf{f}(z)~[z = \textsf{2}]\) to \(y~[z = \textsf{2} \wedge z \geqslant 0 \wedge z > y]\). Using the constrained rule \(\rho ':\textsf{f}(x) \rightarrow y~[x \geqslant 0]\) from the same constrained term would give \(y~[z = \textsf{2} \wedge z \geqslant 0 \wedge y = y]\).
SMT. SMT solving is a key component in the analysis of LCTRSs and SMT solvers are heavily used during the analysis. In order for SMT solving to not form a bottleneck some care is needed. Again, each different analysis method is equipped with its own SMT solver instance started at the beginning of the analysis. Afterwards such an instance runs until the method has finished. In between, it waits for SMT queries, hence we avoid several restarts of this instance. Constraints are modeled as regular terms of sort boolean and can be checked for satisfiability and validity. Each of those checks runs in its own context (using push and pop commands) in order to avoid any interference with previous queries. Currently crest utilizes Z3 [30] as the default SMT solver, as it turned out to be the most reliable during development. Nevertheless, crest provides the (experimental) possibility to use Yices [10] and CVC5 [6].
Confluence. The computation of constrained critical pairs follows the definition and constrained parallel critical pairs are computed in a bottom up fashion by collecting all possible combinations of parallel steps. Then the various methods to conclude confluence are applied on those pairs. If a method fails on a constrained critical pair then, using Definition 2, the constrained critical pair is split. The logical constraint used in splitting is taken from a matching rule. The various methods run concurrently in order to prevent starvation of methods because of pending SMT solver queries. The first method which succeeds returns the result and all others, including their SMT solver instances, are terminated. We adopt heuristics to bound the number of rewrite steps in the closing sequences. The method that posed the biggest challenge to automation is the 2-parallel closedness [35, Definition 11] needed for (C6) as we cannot simply use an arbitrary parallel step starting from the right-hand side but need to synthesize a parallel step over a set of parallel positions that adheres to the variable condition present in the definition.
Termination. The choices in the parameters of the subterm criterion (T5) and the recursive path order (T2) are modeled in the SMT encoding. Similarly, for the value criterion (T3) first all possible projections are computed. Then an SMT encoding based on the given rules and theory is constructed and a model of the encoding (if it exists) delivers suitable projections that establish termination. An explicit boolean flag in the SMT encoding determines if a strict or weak decrease is achieved. The special variant with projections to suitable linear combinations (T6) encodes this by attaching unknown constants to the projected arguments and summing them up. Those unknowns are then determined by the SMT solver. The (special) value criterion is currently restricted to the theory of integers as suitable well-founded orderings are required. For the integer theory we use \(n \succ m\) if \(n > m \wedge n \geqslant 0\) holds.
Method (T4) receives a DP problem as input and tries to transform it into a smaller one by orienting strictly as many dependency pairs as possible. It is parameterized by a list of termination methods which are applied on the DP problem. The first one which succeeds determines the remaining problem to be solved. Before trying to solve the latter, (T1) is used to decompose it into smaller problems.
Features. Via the command-line arguments several features of crest can be accessed. This includes control over the number of threads in the concurrent setup, the overall timeout of the analysis, or if proof output and debug output should be printed. Furthermore, (parallel) critical pairs or the dependency graph approximation of a given LCTRS problem can be computed. The interface also offers a way to transform an LCTRS into a fully sorted LCTRS in the ARI format. In order to alter the default strategy for the analysis, crest offers a very basic strategy language to specify which methods should be used. Detailed information is provided in the usage information of the supplemented artifact.
5 Improving the Analysis via Transformations
In this section we present new transformations which are especially useful for confluence analysis. These transformations operate on either rules or constrained critical pairs and split or unify those based on their constraints.
Splitting Constrained Critical Pairs
If a constrained critical pair has more than one instance, which is almost always the case, and they cannot all be rewritten by a single rule, then we are not able to perform any rewrite step. To overcome this problem we propose a simple method to split constrained critical pairs.
Definition 2
Given an LCTRS \(\mathcal {R}\), a constrained critical pair \(\rho :s \approx t~[\varphi ] \in \textsf{CCP}(\mathcal {R})\) and a constraint \(\psi \in \mathcal {T}(\mathcal {F}_{\textsf{th}},\mathcal {V}\textsf{ar}(\varphi ))\), the set \(\textsf{CCP}(\mathcal {R})_\rho ^\psi \) is defined as \((\textsf{CCP}(\mathcal {R}) \setminus \{\rho \}) \cup \{s \approx t~[\varphi \wedge \psi ], s \approx t~[\varphi \wedge \lnot \psi ]\}\).
The following key lemma states that after splitting critical pairs, all confluence methods are still available. The proof is given in the appendix of [37].
Lemma 2
If \(t \mathrel {_{\mathcal {R}}{\leftarrow }} s \rightarrow _{\mathcal {R}} u\) then \(t \downarrow _{\mathcal {R}} u\) or \(t \leftrightarrow _{\textsf{CCP}_\rho ^\psi (\mathcal {R})} u\).
We illustrate the lemma on the LCTRS in Example 3.
Example 5
Consider the CCP \(\textsf{g}(x) \approx \textsf{h}(x)~[\varphi ]\) with \(\varphi :x \geqslant \textsf{1} \wedge x \leqslant \textsf{2}\) from Example 3. It is neither in normal form nor trivial. Since the subterm \(\textsf{g}(x)\) matches the left-hand side of the rule \(\textsf{g}(x) \rightarrow \textsf{a}~[x = \textsf{1}]\) (which is how crest renders the rule \(\textsf{g}(\textsf{1}) \rightarrow \textsf{a}\)), and the combined constraint \(\varphi \wedge x = \textsf{1}\) is satisfiable, the CCP is split into
$$\begin{aligned}\begin{gathered} \textsf{g}(x) \approx \textsf{h}(x)~[\varphi \wedge x = \textsf{1}] \qquad \text {and}\qquad \textsf{g}(x) \approx \textsf{h}(x)~[\varphi \wedge x \ne \textsf{1}] \end{gathered}\end{aligned}$$
The left one rewrites to the trivial constrained equation \(\textsf{a} \approx \textsf{a}~[\varphi \wedge x = \textsf{1}]\) using the rules \(\textsf{g}(x) \rightarrow \textsf{a}~[x = \textsf{1}]\) and \(\textsf{h}(x) \rightarrow \textsf{a}~[x \leqslant \textsf{1}]\). The right one is rewritten to \(\textsf{b} \approx \textsf{b}~[\varphi \wedge x \ne \textsf{1}]\) using the rules \(\textsf{g}(x) \rightarrow \textsf{b}~[x \leqslant \textsf{2}]\) and \(\textsf{h}(x) \rightarrow \textsf{b}~[x > \textsf{1}]\). Hence the LCTRS \(\mathcal {R}\) is locally confluent by Lemma 2. Using RPO with the precedence \(\textsf{f} > \textsf{g} > \textsf{h} > \textsf{a} > \textsf{b} > \textsf{c}\), termination of \(\mathcal {R}\) is easily shown and hence \(\mathcal {R}\) is confluent.
The following example shows that constrained critical pairs may be split infinitely often before local confluence can be verified.
Example 6
Consider the LCTRS \(\mathcal {R}\) over the theory \(\textsf{Ints}\) consisting of the rules
This LCTRS has a constrained critical pair \(\textsf{f}(n) \approx \textsf{g}(m)~[n \geqslant \textsf{0} \wedge m \geqslant \textsf{0} \wedge n = n \wedge m = m]\) originating from \(\textsf{a}\). To show confluence of \(\mathcal {R}\) we would need to split the pair in order to make rules applicable for joining a specific instance. However, there are infinitely many instances with pairwise different joining sequences.
The next example shows that splitting also helps to prove non-confluence.
Example 7
Consider the LCTRS \(\mathcal {R}\) in Example 3. By changing the constraint of the rule \(\textsf{f}(x) \rightarrow \textsf{g}(x)~[x \geqslant \textsf{1}]\) to \([x \geqslant \textsf{0}]\) we obtain a non-confluent LCTRS. This is shown by splitting the constrained critical pair \(\textsf{g}(x) \approx \textsf{h}(x)~[x \geqslant \textsf{0} \wedge x \leqslant \textsf{2}]\), and subsequently showing that \(\textsf{g}(x) \approx \textsf{h}(x)~[x < \textsf{1} \wedge x \geqslant \textsf{0} \wedge x \leqslant \textsf{2}]\) rewrites to the non-trivial normal form \(\textsf{c} \approx \textsf{a}~[x < \textsf{1} \wedge x \geqslant \textsf{0} \wedge x \leqslant \textsf{2}]\).
Merging Constrained Rewrite Rules
Next we discuss the merging of constrained rewrite rules. The idea here is that rewrite steps may become possible after merging similar rules.
Definition 3
Let \(\rho _i:\ell _i \rightarrow r_i~[\varphi _i]\) for \(i = 1, 2\) be variable-disjoint rewrite rules in an LCTRS \(\mathcal {R}\). Suppose there exists a renaming \(\sigma \) such that \(\ell _1 = \ell _2\sigma \), \(r_1 = r_2\sigma \) and \(\mathcal {V}\textsf{ar}(\varphi _1) = \mathcal {V}\textsf{ar}(\varphi _2\sigma )\). The LCTRS \(\mathcal {R}_{\rho _1}^{\rho _2}\) is defined as
The relations \(\rightarrow _{\mathcal {R}}\) and \(\rightarrow _{\mathcal {R}_{\rho _1}^{\rho _2}}\) coincide.
Example 8
The LCTRS \(\mathcal {R}\) over the theory \(\textsf{Ints}\) consisting of the rewrite rules
admits the constrained critical pair \(\textsf{2} \approx \textsf{g}(x)~[\textsf{1} \leqslant x \wedge x \leqslant \textsf{3} \wedge \textsf{2} \leqslant x \wedge x \leqslant \textsf{4}]\). After rewriting the subterm \(\textsf{g}(x)\) to \(\textsf{h}(x)\), no further step is possible because the rewrite rules for \(\textsf{h}\) are not applicable. However, if we merge the two rules for \(\textsf{h}\) into
$$\begin{aligned} \textsf{h}(x) \rightarrow y~[(x = \textsf{2} \wedge y = x) \vee (x = \textsf{3} \wedge y = \textsf{2})] \end{aligned}$$
we can proceed as \(\textsf{1} \leqslant x \wedge x \leqslant \textsf{3} \wedge \textsf{2} \leqslant x \wedge x \leqslant \textsf{4}\) implies \(((x = \textsf{2} \wedge y = x) \vee (x = \textsf{3} \wedge y = \textsf{2}))\sigma \) for \(\sigma (y) = \textsf{2}\). This is exactly how crest operates.
6 Experimental Evaluation
In this section we show the progress of crest since the start of its development in early 2023. Initial experiments of an early prototype of crest were reported in [34]. In the following tables the prototype of [34] is denoted by prototype. Since then more criteria for (non-)confluence and termination were added, and parts of the tool infrastructure were completely revised. Detailed results are available from the website of crest and the artifact of the experiments at the Zenodo repository [36].
All experiments were performed using the benchexec11 benchmarking framework which is also used in the StarExec cluster. The benchmark hardware consists of several Intel Xeon E5-2650 v4 CPUs having a base clock speed of 2.20GHz, amounting in total to 64 cores and 128 GB of RAM. As benchmarks we use the problems in the new ARI database12 in addition to the examples from this paper.
Tool Setup. Each tool receives an ARI benchmark as input and should return either "YES" (property was proved), "NO" (property was disproved) or "MAYBE" (don’t know) as the first line of its output. In the tables we represent those with ✓, ✗ and ?, respectively. The fourth category depicted by † denotes that the translation from the ARI format to the input format of the respective tool failed. In order to have a realistic setup, a tool has 4 cores including 8 GB of RAM available for each run. Each tool has 60 seconds to solve a problem before it is killed. Since we have no information about how many threads the other tools use, in the experiments we use CPU time over wall-clock time in order to have a fair comparison.
Our tool crest is split into different binaries depending on the analysis. The most important ones are crest-cr for confluence and crest-sn for termination. We use those two including an additional flag to allow at most 8 threads for the concurrent setup. The default strategy for confluence uses all methods concurrently and where specific methods are tested we restrict to those using our strategy flag. For the default termination setup we use reduction pairs including dependency graph analysis, recursive path order, (special) value criterion and subterm criterion.
Cora, Ctrl and the prototype of [34] do not accept the ARI format as input. We have developed transformation tools which (try to) transform an ARI benchmark into their respective input. This might not always be possible, hence the transformation tool might fail, which is the reason why we do not distinguish tool (parse) errors from "MAYBE".
Table 1.
Confluence analysis of examples.
Dummy
Examples. In Table 1 we compare the LCTRS confluence tools on the examples in this paper. crest only fails on Example 6, which is a confluent LCTRS, but for which no automatable method is known.
Confluence Competition. The last (2024) Confluence Competition13 hosted the first LCTRS category, with crest and CRaris as participants. The former achieved 67 confluence and 26 non-confluence proofs on a total of 100 selected problems from the ARI database. CRaris, which does not (yet) implement techniques for non-confluence achieved 54 confluence proofs. Currently, crest is the only tool utilizing a criterion for non-confluence of LCTRSs.
Fig. 2.
ARI file 1529 (without sort annotations and meta information).
Confluence. All confluence criteria implemented in crest, except (C2), require left-linearity. For (C3) right-linearity is also required. Left- and right-linearity is checked only on the non-logical variables. Table 2 presents a summary of the confluence methods implemented in crest. The full set of benchmarks consists of the 107 problems in the ARI database. crest can prove in a full run with all methods enabled 72 confluent and 26 non-confluent. Of the remaining 9 problems, 2 result in "MAYBE" and 7 in a timeout. Interesting to observe is that (almost) development closedness is way faster than (almost) parallel closedness, which may be due to the fact that less multi-steps than parallel steps are needed to turn a constrained critical pair into a trivial one. The number 72 is explained by the fact that (C5) and (C6) are incomparable: (C5) succeeds on the problem in Fig. 1 but fails on the one in Fig. 2, while the opposite holds for (C6).
Table 2.
Confluence analysis using methods in crest on 107 LCTRSs.
Dummy
Table 3.
Confluence analysis of LCTRS tools on 107 LCTRSs.
Dummy
In Table 3 we compare all confluence tools on the same 107 LCTRS problems. Ctrl supports only weak orthogonality and CRaris in addition the Knuth–Bendix criterion. Overall crest is able to solve 92 % of the LCTRS problems in the current ARI database and this percentage is reached even if the timeout is restricted to 10 seconds. The prototype of [34] supports the methods (C1), (C3), (C4) and proves 67 (63 %) confluent within 122 seconds.
Termination. In Table 4 we compare the different termination methods in crest. The "dependency graph" method corresponds to (T1) with a check for the absence of SCCs, "recursive path order" corresponds to (T2), "subterm criterion" to (T5), "(special) value criterion" to (T3) ((T6)) and "reduction pairs" to (T4). The methods annotated with (T1) work on DP problems and are applied after an initial dependency graph analysis. The method "reduction pairs no SVC" uses (T2), (T3) and (T5) and "default" includes additionally (T6). The latter constitutes the current default setup in crest.
Table 4.
Termination analysis using methods in crest on 107 LCTRSs.
Dummy
We continue the evaluation by comparing crest to other termination tools for LCTRSs. For this comparison we use the higher-order tool Cora and Ctrl. The experiments in Table 5 show that the tools are comparable in strength on the LCTRS benchmarks in the ARI database, which is not that surprising as the implemented methods are similar. All tools together prove 73 % of the LCTRSs in the ARI database terminating. All those tools fail on the bit vector problem in Fig. 3 whereas CRaris is able to prove termination (Naoki Nishida, personal communication). A fork of the official version of Ctrl14 implements the technique of [33] for non-termination of LCTRSs. Initial experiments reveal that it succeeds to prove non-termination of 8 problems in Table 5.
Table 5.
Termination analysis of LCTRS tools on 107 LCTRSs.
Dummy
Fig. 3.
ARI file 1605 (without sort annotations and meta information).
Term Rewrite Systems. In the final experiment we compare crest with the state-of-the-art in automated confluence proving for TRSs. After parsing an input TRS, crest attaches a single sort to all function symbols and variables, and adds an empty constraint to all rules. At this point the TRS can be analyzed as an LCTRS. We compare crest to the latest winner of the TRS category in the Confluence Competition, CSI [32], on the 566 TRS benchmarks in the ARI database. The results can be seen in Table 6. Keeping in mind that there is some overhead in the analysis of crest on TRSs as all its methods are geared towards the constrained setting, the 31 % mark is not a bad result. Here it is important to note that CSI has been actively developed over a ten-year period and utilizes many more confluence methods—there is several decades of research on confluence analysis of TRSs while LCTRS confluence analysis is still in its infancy.
Table 6.
Confluence analysis of crest and CSI on 566 TRSs.
Dummy
7 Conclusion and Future Work
In this paper we presented crest, an open-source tool for automatically proving (non-)confluence and termination of LCTRSs. Detailed experiments were provided to show the power of crest.
In order to further strengthen the (non-)confluence analysis in crest we plan to adapt powerful methods like order-sorted decomposition [12] and redundant rules [31, 38] for plain term rewriting to the constrained setting. Labeling techniques [41] are also on the agenda. The same holds for termination analysis. Natural candidates are matrix interpretations [11] as well as the higher-order methods in [14]. Especially termination problems on real values, like the one in Fig. 4, should be supported in future. Also non-termination analysis of LCTRSs [33] is of interest. Completion, which is supported in Ctrl [39], is another topic for a future release of crest. In a recent paper [2] the semantics of LCTRSs is investigated. In that context, concepts like checking consistency of constrained theories are relevant, which are worthy to investigate from an automation viewpoint.
Since constrained rewriting is highly complex [35, Section 3], a formalization of the implemented techniques in a proof assistant like Isabelle/HOL is important. The recent advances in the formalization and subsequent certification of advanced confluence techniques [16, 21, 22] for plain rewriting in connection with the transformation in [35, Section 4] make this a realistic goal.
Finally, to improve the user experience we aim at a convenient web interface and a richer command-line strategy.
Code and Availability Statement. The source code and data that support the contributions of this work are freely available in the Zenodo repository “crest - Constrained REwriting Software Tool: Artifact for TACAS 2025” at https://doi.org/10.5281/zenodo.13969852 [36]. The authors confirm that the data supporting the findings of this study are available within the paper and the artifact.
We thank Fabian Mitterwallner for valuable discussions on automation. We are grateful to the authors of the tools used in the experiments for their help in obtaining executables and useful insights about their usage. The insightful comments and suggestions provided by the reviewers greatly improved the presentation of the paper.
Disclosure of Interests
The authors have no competing interests to declare that are relevant to the content of this article.
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
on constrained terms is defined as \(\sim \cdot \rightarrow _{\mathcal {R}}\cdot \sim \) and
indicates that the rewrite step in
takes place at position p in s. Similarly, we write
if the position in the rewrite step is below position p. We illustrate some of these concepts by means of a simple example which models the computation of the maximum of two integers.
) and multi-step (
) rewriting following [35, Definition 3] and [34, Definition 8]. The former is capable of applying several rules at parallel positions in a step while the latter additionally allows recursive steps within the used matching substitutions of rules. A rewrite sequence consists of consecutive rewrite steps, independent of which kind. The reflexive and transitive closure of \(\rightarrow \) is denoted by \(\rightarrow ^{*}\). Moreover, for arbitrary terms s and t we write \(s \leftrightarrow t\) if \(s \mathrel {({\leftarrow } \cup {\rightarrow })} t\) and \(s \downarrow t\) if there exists a term u such that \(s \rightarrow ^{*} u \mathrel {^{*}{\leftarrow }} t\).
forms a constrained parallel critical pair \(\ell \sigma [r_p\sigma ]_{p \in P} \approx r\sigma ~[\varPhi ]\) if the following conditions are satisfied:
. Note that only the left part (s) is rewritten here and \(s' \approx t~[\varphi ]\) is a trivial constrained equation. For (finite) terminating TRSs, confluence is decided by rewriting critical pairs to normal form [20]. For terminating LCTRSs confluence—even for a decidable theory—is undecidable [35], but rewriting constrained critical pairs to normal forms is still of value. This is used in (C2) above. We need however to adapt the notion of normal form for constrained terms.
