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, JACM 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 tottt2, 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.