The tool crest performs a confluence analysis on logical constrained rewrite
systems (LCTRSs for short). It is written in Haskell and bases on the
Haskell term-rewriting library.
Currently it supports checking if an LCTRS is orthogonal, weakly orthogonal,
strongly closed or (almost) parallel closed.
The implementation of those criteria follows the explained concepts in the accompanying
CADE-29 paper.
Below you find the linux binaries of crest used for the CADE-29 paper (for other operating system binaries contact an author).
A prerequisite of the tool is a Z3 binary in your
path as well as other SMT solvers if they are activated via their respective flag.
Below you find the experiments and how to reproduce them on your own with the provided binaries above.
Note that elapsed times may differ due to the SMT solver and concurrency in crest.
Futhermore, also results near the timeout could be different.
Results on full set:
The results were obtained with a timeout of 5 seconds on 125 problems and all methods activated.
Download and extract the benchmark set above and run
crest-benchmark --html examples-paper/
to obtain the file crest-benchmark.html with the results.
Selected interesting examples (Table 1):
These experiments show the answers to Table 1 in the paper and were run with a timeout of 10 seconds.
Due to re-running the experiments they may differ.
Download and extract the benchmark set above and run
crest-benchmark --html -t 10 --seq examples-paper/
to obtain the file crest-benchmark.html with the results.
Relative comparison between methods (Table 2):
These experiments were run with a timeout of 5 seconds and only one method activated on all 125 problems in the benchmark set.
Below each link the command to obtain the file crest-benchmark.html with the results is given.
At the moment our tool crest lacks termination analysis (this is work in progress), we are not able to apply Newman's lemm
for confluence analysis. A reviewer of the CADE-29 paper suggested to use Ctrl as a black box for termination analysis and then
use crest to show local confluence. A big thank you to Cynthia Kop for providing us a binary and helpful information how
to compile Ctrl!
Newman's Lemma (results for local confluence on terminating examples)
crest-benchmark --html -m 6 examples-paper-sn/ -t 60
Input Format (*.lctrs)
The input file for crest needs to adhere to the grammar in the figure below, which starts at the production rule input.
The input mainly consists of three different parts, formatspec specifying the format of the input and the respective logic,
symbol which specifies function symbols and rule which specifies a rule of the LCTRS.
The first part formatspec specifies that we only allow LCTRSs and the respective logic which is restricted to
logics which crest can handle at the moment.
Note that although :logic is optional in this S-expression we demand for our tool that a logic is specified
whenever theory symbols are used.
If not then intended theory symbols are treated as standard term symbols.
In order to define the signature of an LCTRS, all function symbols are defined as symbol with their respective fid,
the arity which is an arbitrary natural number and a sort declaration sortdecl.
The non-terminal fid specifies the name of a function symbol and is not allowed to contain white-space,
characters in "(),:;[]{}?≈" and keywords like fun, rule, :logic, etc.
Every symbol which is not defined in fun or given by the SMT-LIB logic in formatspec is treated as a variable.
Names of variables are given by vid which follows the same policy as fid.
A sortdecl is a sequence of sorts (like Bool or Int for sorts defined by the theory QF_LIA)
separated by white-space and enclosed by parentheses.
A sort specified by sort is allowed to be a character sequence not containing white-space or a character in "(),.:;[]~*<>?".
Rules are defined by rule with two term's that are standard terms consisting of function symbols and variables in S-expression syntax.
Furthermore, a constraint is specified as smtexp which is a term consisting of
variables and function symbols from the theory, i.e. a valid S-expression in the chosen SMT-LIB logic.
A vardecl is a sequence of variable sort pairs separated by white-space and enclosed in parentheses.
This is useful whenever type inference fails to infer types for variables.
As we need to check satisfiability of constraints and thus specify a unique sort for each variable appearing
in the constraint used by the SMT-solver, the LCTRS must be fully sorted.
Input Grammar for crest:
For an example look at the LCTRS max from the paper:
(format LCTRS :logic QF_LIA)
(fun max 2 :sort (Int Int Int))
(rule (max x y) x :guard (>= x y) :vars ((x Int)))
(rule (max x y) y :guard (>= y x))
(rule (max x y) (max y x) :vars ((x Int) (y Int)))