[Termtools] supplementing the competition input format

[Peter Schneider-Kamp]

Johannes Waldmann wrote:
> Together with a common "control language",
> this will allow us to compare and combine parts of provers.

Right, a common "control language" should be the next goal.

> I don't know whether QRESTRICTION is "typical" (or "Aprove centric"),
> but I do think it is the right idea that Aprove outputs such
> QRESTRICTION statements. If a prover does not understand this,
> it just ignores them.

QRESTRICTION might be a bit "AProVE centric. In virtually all
cases this will be either empty (full termination) or it will
be a superset of the left-hand sides of the rules and thus
we can additionally set (STRATEGY INNERMOST) such that tools
that care about innermost get most of the advantage.

Kind regards,
Peter