Saigawa

News

About

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

Download

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

Latest Version

Old Version

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

Tool Authors

Contact