[Termtools] naming, placing and contents of benchmarks (srs/cycles)

Johannes Waldmann johannes.waldmann at htwk-leipzig.de
Fri Sep 9 11:37:03 CEST 2016


Dear all,

Wenzel's SRS and Cycle benchmarks should be added to TPDB,
but I now think their file names
(like aaabaaaa-aaaaaaabaaab.srs.xml) are impractical,
and instead they should just be numbered.
(but original name  should be kept as attribute,
for later reference to results of this year's competition)

Cycle termination problems look like SRS problems,
but we might want to make a distinction.
We could make a separate directory
for cycle termination problems.

We could also (additionally) put some annotation
in the problems themselves.
I think this annotation should be a "theory",
because it is rewriting modulo conjugation (rotation).

Note this cannot be expressed in the benchmark (XTC) format
(where "theory" is attached to function symbol).
Also, there is no "theory" (per se) in the CPF input tag
(it has "acRewriteSystem").

For historical reference, the original (plain text) format
would be easier to extend for this,
since it had THEORY declaration at the top level,
https://www.lri.fr/~marche/tpdb/format.html

- J.


More information about the Termtools mailing list