The format for first-order conditional rewrite systems is a simplification of the old TPDB format, according to the following grammar:
ctrs ::= (CONDITIONTYPE ctype) [(VAR idlist)] (RULES rulelist) [(COMMENT string)] ctype ::= SEMI-EQUATIONAL | JOIN | ORIENTED idlist ::= ε | id idlist rulelist ::= ε | rule rulelist rule ::= term -> term | term -> term | condlist condlist ::= cond | cond, condlist cond ::= term == term term ::= id | id() | id(termlist) termlist ::= term | term, termlistThe restrictions on
stringare the same as in the TRS format.
(CONDITIONTYPE ORIENTED) (VAR x) (RULES not(x) -> false | x == true not(x) -> true | x == false )
Thomas Sternagel provided a converter ctrs-converter.jar between the 'old' TRS format and the modified TRS format. It is a simple command line tool that either accepts the path to a trs file as its sole argument or (if no argument is provided) reads from standard input. The tool outputs the converted CTRS on standard output. It is able to convert in both directions (depending on the format of the input). If the input is in the 'old' format and the tool encounters mixed conditions it issues an error message.