Automated Analysis of Logically Constrained Rewrite Systems using crest

TL;DR

crest addresses the problem of automatically proving (non-)confluence and termination for logically constrained rewrite systems. It adopts advanced confluence techniques based on parallel critical pairs, automated non-confluence detection, and a suite of termination methods, plus transformations that merge or split constrained rules. The authors provide extensive experiments comparing crest with Ctrl, CRaris, Cora, and TRS tools on the ARI benchmarks, showing crest achieves high coverage and competitive termination results and uniquely supports non-confluence proofs. They also discuss practical aspects, implementation details, and future directions such as formalization, web interface, and broader theory support.

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.