Term Rewriting

We use an adaption of the ARI format. Our format differs from the formt used at COCO as follows:

• We do not impose any variable conditions, so a rewrite rule is a pair of arbitrary terms.
• Identifiers (i.e., names of variables or function symbols) must be valid SMT-LIB symbols, whereas COCO uses a more liberal definition. Both simple and quoted symbols are allowed.
• Rules are annotated with optional costs, which are natural numbers. So rules are defined as follows:

rule ::= ( rule term term cost?)
cond ::= :cost number