Implement a new rewrite engine based on rewriting theory#1717

Open

mlaveaux wants to merge 138 commits intomCRL2org:masterfrom mlaveaux:feature/rewriter

+3,112-112

Commits on Mar 15, 2024

Made the Rewriter class non copyable.
mlaveaux
committed
Removed commented code.
mlaveaux
committed
Added innermost as a new rewriter implementation.
mlaveaux
committed
Removed an obsolete comment block.
mlaveaux
committed
Added several functions implemented according to the pseudocode.
mlaveaux
committed
Added a constexpr constant to indicate that a variable is undefined.
mlaveaux
committed
Implemented a substitution function, abstraction case not yet finished.
mlaveaux
committed
The match function applies the substitution to the right-hand side.
mlaveaux
committed
Fixed an issue with the capture avoiding substitution, updated comments.
mlaveaux
committed
Only print one message per tried (succesful or failing) rule.
mlaveaux
committed
Optimized matching by only trying equations that start with the same head symbol.
mlaveaux
committed
Renamed defined to count to match the standard map interface.
mlaveaux
committed
Made match_lhs a free function (accepting any substitution template).
mlaveaux
committed
Keep track of sub-terms that are already in normal form.
mlaveaux
committed
Fixed a mistake induced by merging.
mlaveaux
committed
Use an unordered_map_large to store the matching substitution.
mlaveaux
committed
Moved the implementation of recording normal forms to helper functions.
mlaveaux
committed
Added comment to matching_sigma.
mlaveaux
committed
Added computing of conditions similar to the jitty rewriter.
mlaveaux
committed
Fixed the rewriting of individual function symbols.
mlaveaux
committed
Enable an option to toggle normal form tracking.
mlaveaux
committed
Fixed a mistake with the normal form tracking.
mlaveaux
committed
Moved static functions to a single utility header.
mlaveaux
committed
Smaller fixed, the substitution does not have to be applied again.
mlaveaux
committed
Added a possible implementation of the construction stacks.
mlaveaux
committed
Optimized construction_stacks by removing the temporary argument vector.
mlaveaux
committed
The matching substitution is used recursively and thus can not be saved.
mlaveaux
committed
No longer rewrite in the ConstructionStack.
mlaveaux
committed
Moved the choice for using the construction stack to a helper function.
mlaveaux
committed
Small documentation fixes and removed an extraneous semicolon.
mlaveaux
committed
Optimized ConstructionStack by reusing an existing argument stack.
mlaveaux
committed
Use get_nested_head to determine the head of a data_expression.
mlaveaux
committed
Fixed smaller documentation issues.
mlaveaux
committed
Use the stack_array to store arguments during rewriting and substitution.
mlaveaux
committed
Only try to perform a match when the application is not in normal form.
mlaveaux
committed
Check for the given term being in normal form in the match function.
mlaveaux
committed
Replaced the unordered_map by a mapping using the index of the head symbol.
mlaveaux
committed
Only insert normal forms when they are not already marked as such.
mlaveaux
committed
Made the m_local_sigma (was m_matching_sigma) and the argument stack mutable.
mlaveaux
committed
When terms are equivalent they must match by definition.
mlaveaux
committed
Added caching for results of rewriting function applications.
mlaveaux
committed
Use the fixed_size_cache with a size of 1000 elements.
mlaveaux
committed
Updated the comments and removed some unnecessary printing.
mlaveaux
committed
Increased default fixed_size_cache to 1024 elements, use emplace in indexed_set.
mlaveaux
committed
Moved caching to before the call to rewrite_application.
mlaveaux
committed
Fixed some warnings, improved documentation and changed caching behaviour.
mlaveaux
committed
Applied the fifo_policy for the rewrite cache and only cache results after substitution.
mlaveaux
committed
Added a compile time option to count the number of applications per rewrite rule.
mlaveaux
committed
Added a cache_metric object to track cache hits and misses.
mlaveaux
committed
Print cached rewrite steps and rewrite cache metrics.
mlaveaux
committed
Added rewriting lambda abstractions by renaming all bound variables.
mlaveaux
committed
Moved applying the substitution to a different header file.
mlaveaux
committed
Print alpha-conversion before rewriting the body.
mlaveaux
committed
Moved the implementation of the construction stack to its own header.
mlaveaux
committed
Moved (naive) matching to its own class and implementation.
mlaveaux
committed
The substitution must be mutable when applying due to renaming bound variables.
mlaveaux
committed
Renamed all variables in rewrite rules to avoid conflicts.
mlaveaux
committed
Print the single-step rewrite steps performed during rewriting.
mlaveaux
committed
Made the unprotected_aterm constructor explicit.
mlaveaux
committed
The substitution must be stored when rewriting conditions.
mlaveaux
committed
Added a virtual base class for matching algorithms.
mlaveaux
committed
Added an implementation of an pattern match automaton based matcher.
mlaveaux
committed
Fixed several compilation errors after rebasing.
mlaveaux
committed
Changed the interface of Matcher to have less impact on performance.
mlaveaux
committed
Added the automaton matcher as default.
mlaveaux
committed
Moved the stopwatch class to the mcrl2::utilities namespace.
mlaveaux
committed
Simplified the matching implementation.
mlaveaux
committed
Added naive handling of non-linear patterns.
mlaveaux
committed
Moved the linearisation of a TRS to a separate header.
mlaveaux
committed
Do not redefine equivalence_classes in the automaton_matcher header.
mlaveaux
committed
Moved is_consistent to the consistency header.
mlaveaux
committed
Moved the implementation of the underlying automaton to a separate class.
mlaveaux
committed
Changed the underlying automaton to an indexed version.
mlaveaux
committed
Rename TRS variables such that their position is the identifier (and thus unique).
mlaveaux
committed
Moved some implementations to headers and added the AdaptiveMatcher.
mlaveaux
committed
Use a vector for the argument stack that is preserved between calls.
mlaveaux
committed
Worked on the implementation of the APMA construction.
mlaveaux
committed
Worked on the construction of the EAPMA.
mlaveaux
committed
Removed the automaton_matcher as it is subsumed by the adaptive_matcher.
mlaveaux
committed
Simplified and fixed several parts of the EPMA evaluation.
mlaveaux
committed
Fixed some performance issues in the AdaptiveMatcher.
mlaveaux
committed
Enabled a choice for on-the-fly or naive consistency checking in NaiveMatcher.
mlaveaux
committed
Fixed several issues, implemented select and restrict.
mlaveaux
committed
Changed the interface of the matching algorithms to perform better.
mlaveaux
committed
Print additional debug and performance metrics, added options for optimizations.
mlaveaux
committed
Moved all substitution, on right hand sides exclusively to the final state.
mlaveaux
committed
Moved the substitution to the final state to avoid unnecessary substitutions.
mlaveaux
committed
Added an option for greedy matching (choose first available match).
mlaveaux
committed
Fixed some issues, replaced mutable_indexed_substitution by a map substitution.
mlaveaux
committed
Removed an unnecessary include.
mlaveaux
committed
Moved the definition and functions related to positions to a different header.
mlaveaux
committed
Implemented linearisation using positions, added a naive check based on variables.
mlaveaux
committed
Added variables of the condition to be substituted.
mlaveaux
committed
Added a consistency check based on the indices stored for matching.
mlaveaux
committed
Fixed various issues.
mlaveaux
committed
Changed the greedy algorithm slightly.
mlaveaux
committed
Check for consistency on-the-fly enabled first.
mlaveaux
committed
Changed the matching interface to return an iterator over all matches.
mlaveaux
committed
Simplified the cases for conditional rewriting.
mlaveaux
committed
The matching substitution must be preserved for the adaptive automata.
mlaveaux
committed
Fixed some issues with rewriting conditions, added more logging.
mlaveaux
committed
Fixed an issue with progressing when the current index is not consistent.
mlaveaux
committed
Added an optional on-the-fly check for non confluent rules.
mlaveaux
committed
Print additional information about the rewriter.
mlaveaux
committed
Brute force optimize for the smallest automaton.
mlaveaux
committed
Fixed compilation issues under MSVC.
mlaveaux
committed
Implemented enumeration of quantifiers and rewriting of where clauses.
mlaveaux
committed
Preparation for reusing indices in the automaton matcher.
mlaveaux
committed
Implemented tracking normal forms using tags.
mlaveaux
committed
Commented the confluence detection out.
mlaveaux
committed
Added a sequence_substitution to store the matching substitution.
mlaveaux
committed
Tracking normal forms using tags is now more efficient than set based.
mlaveaux
committed
Added the missing sequence_substitution header, removed unused code.
mlaveaux
committed
Fixed several MSVC warnings.
mlaveaux
committed
Optimized the sequence substitution by reusing a single allocated queue.
mlaveaux
committed
Improved the interface of the iterator returned by the matching algorithms.
mlaveaux
committed
Added the original equation to a linear_data_equation for printing.
mlaveaux
committed
Fixed an error in the sequence_substitution.
mlaveaux
committed
Introduced function symbols for consistency checking checkmark and cross.
mlaveaux
committed
Added consistency states.
mlaveaux
committed
Added the evaluation of a consistency state.
mlaveaux
committed
Added the consistency part of the construction.
mlaveaux
committed
Fixed a bug with the computation of workC.
mlaveaux
committed
Removed on-the-fly consistency checking from the iterator.
mlaveaux
committed
Added a printer for expressions in the rewriter.
mlaveaux
committed
Do not reset the rewrite rule statistics for every top-level rewrite.
mlaveaux
committed
Made jitty the default rewriter.
mlaveaux
committed
Fixed an issue with the percentage calculation in cache_metric.
mlaveaux
committed
Collect information about the number of rewrite calls.
mlaveaux
committed
Fixed some compiler warnings.
mlaveaux
committed
Minor changes.
mlaveaux
committed
Added the REC benchmarks to benchmark the rewriters.
mlaveaux
committed
Resolved more compilation errors.
mlaveaux
committed
Fixed more compilation errors.
mlaveaux
committed
Fixed compilation error.
mlaveaux
committed
Fixed the namespace of stopwatch.
mlaveaux
committed
Fixed the namespace in the tools.
mlaveaux
committed
These benchmarks were already moved upstream
mlaveaux
committed