Implement a new rewrite engine based on rewriting theory

libraries/atermpp/benchmark/benchmark_shared.h

@@ -17,7 +17,7 @@ using namespace atermpp;
 template<typename F>
 void benchmark_threads(std::size_t number_of_threads, F f)
 {
-  stopwatch timer;
+  mcrl2::utilities::stopwatch timer;
 
   // Initialize a number of threads.
   std::vector<std::thread> threads(number_of_threads - 1);
@@ -40,45 +40,6 @@ void benchmark_threads(std::size_t number_of_threads, F f)
   std::cerr << "time: " << timer.seconds() << std::endl;
 }
 
-/// \brief Create a nested function application f_depth. Where f_0 = c and f_i = f(f_i-1,...,f_i-1).
-template<bool with_converter = false>
-aterm_appl create_nested_function(const std::string& function_name,  const std::string& leaf_name, std::size_t number_of_arguments, std::size_t depth)
-{
-  // Create a suitable function application.
-  function_symbol f(function_name, number_of_arguments);
-  function_symbol c(leaf_name, 0);
-
-  aterm_appl c_term(c);
-
-  // Initialize a wide function application.
-  std::vector<aterm> arguments(f.arity());
-  for (std::size_t i = 0; i < arguments.size(); ++i)
-  {
-    arguments[i] = c_term;
-  }
-  aterm_appl f_term(f, arguments.begin(), arguments.end());
-
-  for (std::size_t j = 0; j < depth; ++j)
-  {
-    // Create a very wide nested function application
-    for (std::size_t k = 0; k < arguments.size(); ++k)
-    {
-      arguments[k] = f_term;
-    }
-
-    if (with_converter)
-    {      
-      make_term_appl(f_term, f, arguments.begin(), arguments.end(), detail::do_not_convert_term<aterm>());
-    }
-    else
-    {
-      make_term_appl(f_term, f, arguments.begin(), arguments.end());
-    }
-  }
-
-  return f_term;
-}
-
 /// \brief Create a nested function application f_depth. Where f_0 = c and f_i = f(f_i-1,...,f_i-1).
 ///        However, this function uses the fixed arity constructor of length N which should be faster.
 template<std::size_t N>

libraries/atermpp/include/mcrl2/atermpp/aterm.h

@@ -48,7 +48,7 @@ class unprotected_aterm
 
   /// \brief Constructor.
   /// \param term The term from which the new term is constructed.
-  unprotected_aterm(const detail::_aterm* term) noexcept
+  explicit unprotected_aterm(const detail::_aterm* term) noexcept
    : m_term(term)
   {}
 

libraries/atermpp/include/mcrl2/atermpp/detail/aterm_hash.h

@@ -163,10 +163,13 @@ std::size_t aterm_hasher<N>::operator()(const _aterm& term) const noexcept
   const std::size_t arity = (N == DynamicNumberOfArguments) ? f.arity() : N;
 
   // This is a function application with arguments, hash each argument and combine the result.
-  const _aterm_appl<>& term_appl = static_cast<const _aterm_appl<>&>(term);
-  for (std::size_t i = 0; i < arity; ++i)
+  if constexpr (N > 0)
   {
-    hnr = combine(hnr, term_appl.arg(i));
+    const _aterm_appl<>& term_appl = static_cast<const _aterm_appl<>&>(term);
+    for (std::size_t i = 0; i < arity; ++i)
+    {
+      hnr = combine(hnr, term_appl.arg(i));
+    }
   }
 
   return hnr;

libraries/atermpp/include/mcrl2/atermpp/detail/aterm_pool_storage_implementation.h

@@ -412,7 +412,7 @@ typename ATERM_POOL_STORAGE::iterator ATERM_POOL_STORAGE::destroy(iterator it)
   const Element& term = *it;
 
   // Trigger the deletion hook before the term is actually destroyed.
-  call_deletion_hook(&term);
+  call_deletion_hook(unprotected_aterm(&term));
 
   // Remove them from the hash table, will also destroy terms with fixed arity.
   return m_term_set.erase(it);

libraries/data/CMakeLists.txt

@@ -9,9 +9,12 @@ mcrl2_add_library(mcrl2_data
     source/data_specification.cpp
     source/typecheck.cpp
     source/detail/prover/smt_lib_solver.cpp
+    source/detail/rewrite/innermost.cpp
     source/detail/rewrite/jitty.cpp
     source/detail/rewrite/rewrite.cpp
     source/detail/rewrite/strategy.cpp
+    source/detail/match/naive_matcher.cpp
+    source/detail/match/adaptive_matcher.cpp
     ${COMPILING_REWRITER_SRC}
   EXCLUDE_HEADERTEST
     mcrl2/data/detail/rewrite/jittycpreamble.h

libraries/data/include/mcrl2/data/data_equation.h

@@ -163,5 +163,20 @@ std::set<data::function_symbol> find_function_symbols(const data::data_equation&
 
 } // namespace mcrl2
 
+namespace std
+{
+
+template<>
+struct hash<mcrl2::data::data_equation>
+{
+    std::size_t operator()(const mcrl2::data::data_equation& v) const
+    {
+      const hash<atermpp::aterm> hasher;
+      return hasher(v);
+    }
+};
+
+} // namespace std
+
 #endif // MCRL2_DATA_DATA_EQUATION_H
 

libraries/data/include/mcrl2/data/detail/match/adaptive_matcher.h

@@ -0,0 +1,154 @@
+// Author(s): Maurice Laveaux
+// Copyright: see the accompanying file COPYING or copy at
+// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
+//
+// Distributed under the Boost Software License, Version 1.0.
+// (See accompanying file LICENSE_1_0.txt or copy at
+// http://www.boost.org/LICENSE_1_0.txt)
+//
+
+#ifndef MCRL2_DATA_DETAIL_ADAPTIVE_MATCHER_H
+#define MCRL2_DATA_DETAIL_ADAPTIVE_MATCHER_H
+
+#include "mcrl2/data/data_expression.h"
+#include "mcrl2/data/data_equation.h"
+#include "mcrl2/data/detail/match/matcher.h"
+#include "mcrl2/data/detail/match/automaton.h"
+#include "mcrl2/data/detail/match/position.h"
+#include "mcrl2/data/detail/match/automaton_consistency.h"
+#include "mcrl2/utilities/indexed_set.h"
+
+#include <vector>
+
+namespace mcrl2::data::detail
+{
+
+/// \brief Represents the unnamed variable omega.
+class not_equal : public function_symbol
+{
+public:
+  not_equal()
+    : function_symbol(core::identifier_string("@@not_equal"), data::sort_expression())
+  {}
+};
+
+/// \returns True iff the given data expression is of type omega.
+inline bool is_not_equal(const data_expression& expression)
+{
+  return expression == not_equal();
+}
+
+/// \brief An adaptive non-linear pattern matching automata
+template<typename Substitution>
+class AdaptiveMatcher final
+{
+public:
+  /// \brief Initialize the automaton matcher with a number of equations.
+  AdaptiveMatcher(const data_equation_vector& equations);
+  virtual ~AdaptiveMatcher() {}
+
+  /// \brief A (simplistic) iterator over the matching results.
+  class const_iterator
+  {
+  public:
+    const_iterator(Substitution& sigma)
+      : m_matching_sigma(sigma)
+    {}
+
+    /// \brief Construct an iterator over the match_set, computing the consistent patterns from the subterm indexing
+    const_iterator(std::vector<indexed_linear_data_equation>* match_set,
+      Substitution& sigma)
+      : m_match_set(match_set),
+        m_matching_sigma(sigma)
+    {}
+
+    void operator++()
+    {
+      // Find the next consistent match.
+      ++m_current_index;
+    }
+
+    const extended_data_equation& operator*()
+    {
+      return (*m_match_set)[m_current_index];
+    }
+
+    bool operator!=(std::nullptr_t) const
+    {
+      return (m_match_set != nullptr && m_current_index < m_match_set->size());
+    }
+
+  private:
+    std::vector<indexed_linear_data_equation>* m_match_set = nullptr;
+    Substitution& m_matching_sigma;
+
+    std::vector<bool> m_consistent;
+    std::size_t m_current_index = 0;
+  };
+
+  // Matcher interface.
+
+  /// \details We assume that the given substitution is the identity.
+  const_iterator match(const data_expression& term, Substitution& matching_sigma);
+
+private:
+
+  /// \brief Each state in the pattern match automaton is labelled with a set of variables.
+  struct apma_state
+  {
+    bool is_consistency_state() const { return compare.first != compare.second; }
+
+    bool is_matching_state() const { return position != std::numeric_limits<std::size_t>::max(); }
+
+    // Matching states:
+    std::size_t position = std::numeric_limits<std::size_t>::max(); ///< L, the index of the position to be inspected.
+    std::vector<std::size_t> argument_positions; ///< These are the positions where arguments must be stored in the subterm table.
+
+    // Consistency states:
+    std::pair<std::size_t, std::size_t> compare = std::make_pair(0,0); ///< L, the pair of positions that must be compared.
+
+    // Final states:
+    std::vector<indexed_linear_data_equation> match_set; ///< L, the equations that matched.
+    std::vector<std::pair<data::variable, std::size_t>> assignments; ///< P, the variables that must be assigned and their subterm position.
+  };
+
+  // The underlying automaton.
+  using Automaton = IndexedAutomaton<apma_state>;
+
+  /// \returns A subautomaton for the given state and prefix.
+  Automaton construct_apma(data_expression pref,
+    const std::vector<indexed_linear_data_equation>& L,
+    const std::set<std::pair<std::size_t, std::size_t> >& E,
+    const std::set<std::pair<std::size_t, std::size_t> >& N
+    );
+
+  /// \returns A subset of the given positions, filtering out unecessary positions.
+  std::set<position> restrict(const std::set<position>& positions, const std::vector<indexed_linear_data_equation>& L);
+
+  /// \returns A single position selected from a set of positions.
+  position select(const std::set<position>& positions, const std::vector<indexed_linear_data_equation>& L);
+
+  /// \returns A unique and consistent index for the given position.
+  std::size_t position_index(const position& positions);
+
+  // Information about the underlying automata.
+
+  Automaton m_automaton;
+
+  mcrl2::utilities::indexed_set<position> m_positions;
+
+  std::size_t m_dontcare_index = 0; ///< The index of the dontcare data_expression.
+  std::size_t m_equal_index = 0;
+  std::size_t m_not_equal_index = 0;
+
+  // Store (temporary) information about the match that can be invalidated.
+
+  std::vector<atermpp::unprotected_aterm> m_subterms; ///< A mapping from indices to subterms.
+};
+
+} // namespace mcrl2::data::detail
+
+// Explicit instantiations.
+
+
+#endif // MCRL2_DATA_DETAIL_ADAPTIVE_MATCHER_H