Constrained REwriting Software Tool
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)
Sources
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 source-code.tar.gz |
Experiments
The current confluence results (standard output) on the full set of benchmarks with a timeout of 10 seconds using 8 threads for concurrency:
./crest-cr-benchmark examples --html -j 8 -t 10
The current termination results (standard output) on the full set of benchmarks with a timeout of 10 seconds using 8 threads for concurrency:
./crest-sn-benchmark examples --html -j 8 -t 10
Input Formats (*.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.
Contact
For questions or feedback please contact Jonas Schöpf or