2016/09/12  Version 1.6: Competition version. 
2016/04/21  Version 1.5: Supported AC termination
(certifiable, via experimental option x ).

2016/02/07  Version 1.4: A bugfix for relative termination. 
2015/07/02  Version 1.3: Competition version. 
2015/02/22  Version 1.2: Supported relative termination. 
2014/06/17  Version 1.1 released. 
2014/02/12  Version 1.0 released. 
./NaTT [file] [option]... [processor]...
The TRS whose termination should be verified is read from either the specified file or the standard input. The format should follow the WST format.
To execute NaTT, an SMTLIB 2.0 compliant solver must be installed. The following options are provided for specifying such an SMT solver for backend of NaTT:
smt "command"
:
Uses the solver invoked by command for backend.
The solver should be configured to process SMTLIB 2.0 scripts given
through the standard input.
z3
:
Specifies Z3 version 4.0 or later
for backend.
This option, choosen by default,
is a shorthand for smt "z3 smt2 in"
.
cvc4
:
Specifies CVC4 for backend.
Equivalent to smt "cvc4 incremental producemodels"
NaTT is based on the dependency pair (DP) framework . The following DP processors are available:
EDG
UNCURRY
EDG
processor.
LOOP
WPO [option]
EDG
, and as
a rule removal processor otherwise.
For the latter case,
a care must be taken not to break monotonicity when choosing options.
Following options are available:
a:
algebrapol
,
max
, or
mpol
. (default: pol
)
w[:neg]/W
:neg
is specified
(cf. ).
(default: enabled, nonnegative)
c[:n]/C
b
or t
,
then coefficients are in {0,1} or {0,1,2}, resp. and encoded in linear formulas.
If n is a number or omitted, then coefficients are
natural numbers (below n) and encoded in nonlinear formulas.
For the latter case, the backend SMT solver must support QFNIA logic.
For rule removal processors, 1 is added to (topleft elements of) coefficients
to maintain monotonicity.
dim:n
a:max
or a:mpol
options.
s:{t/p/e}
p[:s]/P
f/F
Z
adm
KBO
,
which is a shorthand for WPO Z adm
.
KBO c[:n]
.
POLO
, which is a shorthand for WPO s:e P F
.
POLO dim n
,
where n is the dimension.
POLO a:mpol
.
LPO
, a shorthand for WPO a:max W
.
RPO
, a shorthand for WPO a:max W mset
.