For the TACAS 2025 submission click here.

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

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

News

• 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

• 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 0.8.7.1

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

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 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.

Contact

For questions or feedback please contact Jonas Schöpf or Aart Middeldorp.