Crest

The tool crest performs a confluence/termination analysis on logical constrained rewrite systems (LCTRSs for short). It is written in Haskell and based on the Haskell term-rewriting library and a fork of the Haskell simple-smt library. As default SMT solver currently Z3 is used. Currently it supports checking if an LCTRS is (non-)confluent using the following methods:

(weak) orthogonality
strongly closedness
(almost) parallel closedness
(almost) development closedness
parallel closedness of parallel critical pairs
non-confluence via finding a non-trivial constrained equation in normal form originating from a CCP
redundant constrained rules

The implementation of those criteria follows the explained concepts in the accompanying publications below.

News

16 July 2025 crest version 1.0 released
05 May 2025 our tool paper on crest was presented at TACAS 2025
29 September 2023 moved (outdated) CADE information to different website
21 September 2023 links to related publications (including full version of CADE paper) online
22 May 2023 experiments with Newman's lemma (requested by a reviewer)
9 March 2023 crest version 0.1 released

Publications

Improving Confluence Analysis for LCTRSs
14th International Workshop on Confluence (IWC) 2025 (link)
Automated Analysis of Logically Constrained Rewrite Systems using crest
31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) 2025 (link)
Automated Analysis of Logically Constrained Rewrite Systems using crest
arXiv version of the TACAS 2025 paper on crest (link)
Confluence of Logically Constrained Rewrite Systems Revisited (Full Version)
full version of the IJCAR 2024 paper on arXiv
Confluence of Logically Constrained Rewrite Systems Revisited
12th International Joint Conference on Automated Reasoning (IJCAR) 2024 (link)
Reducing Confluence of LCTRSs to Confluence of TRSs
12th International Workshop on Confluence 2023 (link)
Confluence Criteria for Logically Constrained Rewrite Systems (Full Version)
full version of the CADE 2023 paper on arXiv
Confluence Criteria for Logically Constrained Rewrite Systems
29th International Conference on Automated Deduction 2023 (link)

Latest Binaries/Experiments/Source Code version 1.0.0.6

Below you find fully statically linked linux binaries of crest-cr (crest-sn) and crest-cr-benchmark (crest-sn-benchmark). For other operating system binaries use the contact information below. A dependency of all binaries is a Z3 binary in your path as well as other SMT solvers if they are activated via their respective flag. Furthermore our benchmarking tools need find. Note that "*-cr-*" denotes the confluence tools and "*-sn-*" the termination tools. For more information consult the usage information of the binaries or the README in the source code.

crest-cr Linux Usage
crest-cr-benchmark Linux Usage
crest-sn Linux Usage
crest-sn-benchmark Linux Usage
benchmark set examples.tar.gz
source code source-code.tar.gz

Compiling crest's source code also produces binaries for a (partial) translation from the ARI format into the input formats of Ctrl, Cora, AProVE (iTRSs only) and the crest prototype presented at CADE 2023.

Experiments

The current results on the ARI-COPS database using a timeout of 10 seconds and 8 threads: confluence (standard output) and termination (standard output). They were produced with:

./crest-cr-benchmark problems-ari-cops --html -j 8 -t 10
./crest-sn-benchmark problems-ari-cops --html -j 8 -t 10

The current results on a selected set of benchmarks shipped with the source code, using a timeout of 10 seconds and 8 threads: confluence (standard output) and termination (standard output). They were produced with:

./crest-cr-benchmark examples-cr --html -j 8 -t 10
./crest-sn-benchmark examples-sn --html -j 8 -t 10

Input Format (*.ari)

It accepts LCTRSs in the new ARI format described here. For an outdated description with a little bit more infromation see the publication at IWC 2023.