Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Implement a new rewrite engine based on rewriting theory #1717

Open
wants to merge 138 commits into
base: master
Choose a base branch
from
Open

Implement a new rewrite engine based on rewriting theory #1717

wants to merge 138 commits into from

Conversation

mlaveaux
Copy link
Member

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.
  • Print rewrite steps performed, debug information and metrics.
  • Introduce the notion of positions to the toolset.
  • Added the mCRL2 benchmarks from the "Rewrite Engines Competition" benchmark set.
  • Implemented a naive matching algorithm that can optionally index on the head symbol.
  • Implemented the non-linear pattern matching automata for matching either performing consistency checks during matching or afterwards.
  • Implemented a straightforward innermost rewriter that can deal with enumeration, lambda terms.
  • Implemented rewrite cache of closed terms for experimentation, disabled by default.
  • Track normal forms of the right-hand side using a tag, or using an unordered set.

@mlaveaux mlaveaux added the feature New functionality label Jul 18, 2023
@mlaveaux mlaveaux self-assigned this Jul 18, 2023
@mlaveaux mlaveaux force-pushed the feature/rewriter branch 2 times, most recently from b19d9bc to 037a140 Compare March 12, 2024 16:49
@mlaveaux
Made the Rewriter class non copyable.
b6e1aa6
@mlaveaux
Removed commented code.
40179f0
@mlaveaux
Added innermost as a new rewriter implementation.
a76df75
@mlaveaux
Removed an obsolete comment block.
269c6e6
@mlaveaux
Added several functions implemented according to the pseudocode.
a38be7b 
 * Added a very naive matching function.
@mlaveaux
Added a constexpr constant to indicate that a variable is undefined.
c787008
@mlaveaux
Implemented a substitution function, abstraction case not yet finished.
88499dc
@mlaveaux
The match function applies the substitution to the right-hand side.
4e7754e 
 * Improved matching by ignoring impossible cases.
@mlaveaux
Fixed an issue with the capture avoiding substitution, updated comments.
1469a28
@mlaveaux
Only print one message per tried (succesful or failing) rule.
5e66d8e
@mlaveaux
Optimized matching by only trying equations that start with the same …
361fece 
…head symbol.
@mlaveaux
Renamed defined to count to match the standard map interface.
dece028
@mlaveaux
Made match_lhs a free function (accepting any substitution template).
8c68d0a
@mlaveaux
Keep track of sub-terms that are already in normal form.
6ce5550
@mlaveaux
Fixed a mistake induced by merging.
87cab79
@mlaveaux
Use an unordered_map_large to store the matching substitution.
0c23440
@mlaveaux
Moved the implementation of recording normal forms to helper functions.
fe3f214
@mlaveaux
Added comment to matching_sigma.
4d6dabc
@mlaveaux
Added computing of conditions similar to the jitty rewriter.
a8e6405
@mlaveaux
Fixed the rewriting of individual function symbols.
a866054
@mlaveaux
Enable an option to toggle normal form tracking.
abe76e2 
 * Clear the set of normal forms after the rewriting for more consistent
   benchmarking.
@mlaveaux
Fixed a mistake with the normal form tracking.
fac96a0
@mlaveaux
Moved static functions to a single utility header.
dbfc5b4
@mlaveaux
Smaller fixed, the substitution does not have to be applied again.
8dd11d1
@mlaveaux
Added a possible implementation of the construction stacks.
655e6b7
mlaveaux and others added 29 commits March 15, 2024 11:59
@mlaveaux
Commented the confluence detection out.
3703655
@mlaveaux
Added a sequence_substitution to store the matching substitution.
bf04658 
 * Although this still causes allocations it is far more efficient than
   map based substitutions, because the number of bound variables is low.
@mlaveaux
Tracking normal forms using tags is now more efficient than set based.
0f24528
@mlaveaux
Added the missing sequence_substitution header, removed unused code.
3a5e707
@mlaveaux
Fixed several MSVC warnings.
da496da
@mlaveaux
Optimized the sequence substitution by reusing a single allocated queue.
53003e3 
 * The assumption is that all assignments take place before the next
   sequence substitution is created, and that its destruction takes place
   in reverse order of creation.
@mlaveaux
Improved the interface of the iterator returned by the matching algor…
bdfac65 
…ithms.
@mlaveaux
Added the original equation to a linear_data_equation for printing.
1645942
@mlaveaux
Fixed an error in the sequence_substitution.
bee4e81
@mlaveaux
Introduced function symbols for consistency checking checkmark and cr…
97bd6be 
…oss.
@mlaveaux
Added consistency states.
370cbce
@mlaveaux
Added the evaluation of a consistency state.
93b9185
@mlaveaux
Added the consistency part of the construction.
50eebe8
@mlaveaux
Fixed a bug with the computation of workC.
0b84214
@mlaveaux
Removed on-the-fly consistency checking from the iterator.
6bd7e03
@mlaveaux
Added a printer for expressions in the rewriter.
3c1f406
@mlaveaux
Do not reset the rewrite rule statistics for every top-level rewrite.
c7f589e
@mlaveaux
Made jitty the default rewriter.
fad7a9c
@mlaveaux
Fixed an issue with the percentage calculation in cache_metric.
e577094
@mlaveaux
Collect information about the number of rewrite calls.
a2c7560
@mlaveaux
Fixed some compiler warnings.
22c3d46
@mlaveaux
Minor changes.
88d085a
@mlaveaux
Added the REC benchmarks to benchmark the rewriters.
962b8a4
@mlaveaux
Resolved more compilation errors.
bb05945
@mlaveaux
Fixed more compilation errors.
ab49534
@mlaveaux
Fixed compilation error.
8a6e328
@mlaveaux
Fixed the namespace of stopwatch.
9ac173f
@mlaveaux
Fixed the namespace in the tools.
2b94aa6
@mlaveaux
These benchmarks were already moved upstream
29a6dfd
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees

@mlaveaux mlaveaux

Labels
feature New functionality
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
1 participant
@mlaveaux