Implement a new rewrite engine based on rewriting theory

[mlaveaux]

This pull request forms the basis for a new rewrite engine with the goal to resolve issue #912. It is (for now) a pure innermost rewrite based on non-linear adaptive pattern matching automata. This pull request is mostly to start with compilation on different platforms and testing.

Matching

Matching is based on the work "Adaptive Non-linear Pattern Matching Automata.", with several variations that can be toggled for experimental comparison. The current implementation positions are indexed into a sub term table for faster consistency checking (avoiding linear walk through term) and delivering the matching substitution.

Progress

• [ ] Implement an iterative rewrite engine using a configuration stack that avoids the need of tracking normal forms and computing matching substitution. I think this can also avoid the construction of intermediate terms somewhat.
• [ ] Add pseudo code from papers into the documentation.
• [ ] Integrate strategy from the just-in-time rewrite engine.
• [ ] Higher order matching.
• [ ] It is not yet competitive with the existing rewriters.
• [x] Print rewrite steps performed, debug information and metrics.
• [x] Introduce the notion of positions to the toolset.
• [x] Added the mCRL2 benchmarks from the "Rewrite Engines Competition" benchmark set.
• [x] Implemented a naive matching algorithm that can optionally index on the head symbol.
• [x] Implemented the non-linear pattern matching automata for matching either performing consistency checks during matching or afterwards.
• [x] Implemented a straightforward innermost rewriter that can deal with enumeration, lambda terms.
• [x] Implemented rewrite cache of closed terms for experimentation, disabled by default.
• [x] Track normal forms of the right-hand side using a tag, or using an unordered set.