Saigawa

News

Saigawa 1.4 released. This version participates in the 1st Confluence Competition (CoCo 2012)

About

Saigawa is a fully automatic confluence tool for first-order term rewrite systems. The latest version is based on the four confluence criteria:

confluence criterion of Hirokawa and Middeldorp (JAR 2011)
confluence criterion of Klein and Hirokawa (LPAR 2011)
Church-Rosser modulo by Jouannaud and Kirchner (SIAM Journal of Computing, 1986)
rule labeling of van Oostrom (RTA 2008)

Download

The source code and 64-bit Linux executable of Saigawa are freely available.

Latest Version

Saigawa 1.4: saigawa-1.4.tar.gz (x64 Linux executable)
(May 22, 2012; supported confluence criterion of [Jouannaud and Kirchner, SIAM Journal of Computing 1986])

Old Version

Saigawa 1.3: saigawa-1.3.tar.gz
(May 22, 2012; supported confluence criterion of [Klein and Hirokawa, LPAR 2012])
Saigawa 1.2: saigawa-1.2.tar.gz
(October 3, 2011; supported fully automatic mode)
Saigawa 1.1: saigawa-1.1.tar.gz
(July 19, 2011; fixed a bug of -dc and -dc2)
Saigawa 1.0: saigawa-1.0.tar.gz
(November 30, 2010)

Requirement

The tool requires termination tools and a QF-NIA SMT solver. In the default setting it uses:

Please set PATH to ttt2, muterm, and minismt. Note that Saigawa can show (non-)confluence even if some of the above tools have not been installed, while confluence proving power diminishes.

Usage

Usage of saigawa is

$ saigawa [option] <filename.trs>

Here the input file is specified in the WST competition format. The tool outputs YES if confluence is proved, NO if confluence is disproved, and MAYBE if the tool does not reach any conclusion.

Experimental Data

Experiments for the paper of Dominik Klein and Nao Hirokawa, ``Confluence of Non-Left-Linear TRSs via Relative Termination'', LPAR-18, 2012.
Experiments for the journal article of Nao Hirokawa and Aart Middeldorp, ``Decreasing Diagrams and Relative Termination'', Journal of Automated Reasoning.

Tool Authors

Contact

Nao Hirokawa