Line data    Source code

       1             : // Author(s): Wieger Wesselink
       2             : // Copyright: see the accompanying file COPYING or copy at
       3             : // https://github.com/mCRL2org/mCRL2/blob/master/COPYING
       4             : //
       5             : // Distributed under the Boost Software License, Version 1.0.
       6             : // (See accompanying file LICENSE_1_0.txt or copy at
       7             : // http://www.boost.org/LICENSE_1_0.txt)
       8             : //
       9             : /// \file mcrl2/data/rewriter.h
      10             : /// \brief The class rewriter.
      11             : 
      12             : #ifndef MCRL2_DATA_REWRITER_H
      13             : #define MCRL2_DATA_REWRITER_H
      14             : 
      15             : #include "mcrl2/atermpp/detail/aterm_configuration.h"
      16             : #include "mcrl2/data/detail/rewrite.h"
      17             : #include "mcrl2/data/expression_traits.h"
      18             : 
      19             : namespace mcrl2
      20             : {
      21             : 
      22             : namespace data
      23             : {
      24             : 
      25             : /// \brief Rewriter class for the mCRL2 Library. It only works for terms of type data_expression
      26             : /// and data_expression_with_variables.
      27             : template < typename Term >
      28             : class basic_rewriter
      29             : {
      30             :   public:
      31             :     /// \brief The type for the substitution that is used internally.
      32             :     typedef data::mutable_indexed_substitution<> substitution_type;
      33             : 
      34             :   protected:
      35             :     /// \brief The wrapped Rewriter.
      36             :     std::shared_ptr<detail::Rewriter> m_rewriter;
      37             : 
      38             :   public:
      39             : 
      40             :     /// \brief The type for expressions manipulated by the rewriter.
      41             :     typedef Term term_type;
      42             : 
      43             :     /// \brief The rewrite strategies of the rewriter.
      44             :     typedef rewrite_strategy strategy;
      45             : 
      46             :   protected:
      47             : 
      48             :     /// \brief Constructor.
      49             :     /// \param[in] r A rewriter
      50           0 :     explicit basic_rewriter(const std::shared_ptr<detail::Rewriter>& r) :
      51           0 :       m_rewriter(r)
      52           0 :     {}
      53             : 
      54             :     /// \brief Copy Constructor
      55        6651 :     basic_rewriter(const basic_rewriter& other)=default;
      56             : 
      57             :     /// \brief Assignment operator
      58          25 :     basic_rewriter& operator=(const basic_rewriter& other)=default;
      59             : 
      60             :     /// \brief Constructor.
      61             :     /// \param[in] d A data specification
      62             :     /// \param[in] s A rewriter strategy.
      63        1751 :     explicit basic_rewriter(const data_specification& d, const strategy s = jitty) :
      64        1751 :       m_rewriter(detail::createRewriter(d, used_data_equation_selector(d), static_cast< rewrite_strategy >(s)))
      65        1751 :     { }
      66             : 
      67             :     /// \brief Constructor.
      68          50 :     basic_rewriter(const data_specification& d, const used_data_equation_selector& equation_selector, const strategy s = jitty) :
      69          50 :       m_rewriter(detail::createRewriter(d, equation_selector, static_cast< rewrite_strategy >(s)))
      70          50 :     {}
      71             : 
      72             : };
      73             : 
      74             : /// \brief Rewriter that operates on data expressions.
      75             : //
      76             : /// \attention As long as normalisation of sorts remains necessary, the data
      77             : /// specification object used for construction *must* exist during the
      78             : /// lifetime of the rewriter object.
      79             : 
      80             : class rewriter: public basic_rewriter<data_expression>
      81             : {
      82             :   protected:
      83             :     // cache the empty substitution, since it is expensive to construct
      84       88648 :     static substitution_type& empty_substitution()
      85             :     {
      86             : #ifdef MCRL2_ENABLE_MULTITHREADING 
      87             :       static_assert(mcrl2::utilities::detail::GlobalThreadSafe);
      88       88648 :       thread_local substitution_type result;
      89             : #else
      90             :       static_assert(!mcrl2::utilities::detail::GlobalThreadSafe);
      91             :       static substitution_type result;
      92             : #endif
      93       88648 :       assert(result.empty());    // This static substitution should always become empty again after use.
      94       88648 :       return result;
      95             :     }
      96             : 
      97             :     /// \brief Default specification used if no specification is specified at construction
      98          12 :     static const data_specification& default_specification()
      99             :     {
     100          12 :       static data_specification specification;
     101          12 :       return specification;
     102             :     }
     103             : 
     104             :     /// \brief Constructor for internal use.
     105             :     /// \param[in] r A rewriter
     106           0 :     explicit rewriter(const std::shared_ptr<detail::Rewriter>& r) :
     107           0 :       basic_rewriter(r)
     108           0 :     {}
     109             : 
     110             : #ifdef MCRL2_COUNT_DATA_REWRITE_CALLS
     111             :     mutable std::size_t rewrite_calls = 0;
     112             : #endif
     113             : 
     114             :   public:
     115             :     typedef basic_rewriter<data_expression>::substitution_type substitution_type;
     116             : 
     117             :     /// \brief Constructor.
     118             :     /// \param[in] r a rewriter.
     119        6651 :     rewriter(const rewriter& r) = default;
     120             : 
     121             :     /// \brief Constructor.
     122             :     /// \param[in] d A data specification
     123             :     /// \param[in] s A rewriter strategy.
     124        1751 :     explicit rewriter(const data_specification& d = rewriter::default_specification(), const strategy s = jitty) :
     125        1751 :       basic_rewriter<data_expression>(d, s)
     126        1751 :     { }
     127             : 
     128             :     /// \brief Constructor.
     129             :     /// \param[in] d A data specification
     130             :     /// \param[in] selector A component that selects the equations that are converted to rewrite rules
     131             :     /// \param[in] s A rewriter strategy.
     132             :     template < typename EquationSelector >
     133          50 :     rewriter(const data_specification& d, const EquationSelector& selector, const strategy s = jitty) :
     134          50 :       basic_rewriter<data_expression>(d, selector, s)
     135             :     {
     136          50 :     }
     137             : 
     138             :     /// \brief Create a clone of the rewriter in which the underlying rewriter is copied, and not passed as a shared pointer. 
     139             :     /// \details This is useful when the rewriter is used in different parallel processes. One rewriter can only be used sequentially. 
     140             :     /// \return A rewriter, with a copy of the underlying jitty, jittyc or jittyp rewriting engine. 
     141           0 :     rewriter clone()
     142             :     {
     143           0 :       return rewriter(m_rewriter->clone());
     144             :     }
     145             : 
     146             :     /// \brief Initialises this rewriter with thread dependent information. 
     147             :     /// \details This function sets a pointer to the m_busy_flag and m_forbidden_flag of this.
     148             :     ///          process, such that rewriter can access these faster than via the general thread.
     149             :     ///          local mechanism. It is expected that this is not needed when compilers become.
     150             :     ///          faster, and should be removed in due time. 
     151         347 :     void thread_initialise()
     152             :     {
     153         347 :       m_rewriter->thread_initialise();
     154         347 :     }
     155             : 
     156             :     /// \brief Rewrites a data expression.
     157             :     /// \param[in] d A data expression.
     158             :     /// \return The normal form of d.
     159       88648 :     data_expression operator()(const data_expression& d) const
     160             :     {
     161       88648 :       return (*this)(d, empty_substitution());
     162             :     }
     163             : 
     164             :     /// \brief Rewrites the data expression d, and on the fly applies a substitution function.
     165             :     /// to data variables.
     166             :     /// \param[in] d A data expression.
     167             :     /// \param[in] sigma A substitution function.
     168             :     /// \return The normal form of the term.
     169             :     template <typename SubstitutionFunction>
     170       16526 :     data_expression operator()(const data_expression& d, const SubstitutionFunction& sigma) const
     171             :     {
     172       16526 :       substitution_type sigma_with_iterator;
     173       16526 :       std::set<variable> free_variables = data::find_free_variables(d);
     174       31288 :       for(const variable& free_variable: free_variables)
     175             :       {
     176       14762 :         sigma_with_iterator[free_variable] = sigma(free_variable);
     177             :       }
     178       33052 :       return (*this)(d, sigma_with_iterator);
     179       16526 :     }
     180             : 
     181             :     /// \brief Rewrites the data expression d, and on the fly applies a substitution function.
     182             :     /// to data variables.
     183             :     /// \param[out] result The normal form of the term is placed in result.
     184             :     /// \param[in] d A data expression.
     185             :     /// \param[in] sigma A substitution function.
     186             :     template <typename SubstitutionFunction>
     187          16 :     void operator()(data_expression& result, const data_expression& d, const SubstitutionFunction& sigma) const
     188             :     {
     189          16 :       substitution_type sigma_with_iterator;
     190          16 :       std::set<variable> free_variables = data::find_free_variables(d);
     191          29 :       for(const variable& free_variable: free_variables)
     192             :       {
     193          13 :         sigma_with_iterator[free_variable] = sigma(free_variable);
     194             :       }
     195          16 :       (*this)(result, d, sigma_with_iterator);
     196          16 :     }
     197             : 
     198             :     /// \brief Rewrites the data expression d, and on the fly applies a substitution function
     199             :     /// to data variables.
     200             :     /// \param[in] d A data expression.
     201             :     /// \param[in] sigma A substitution function.
     202             :     /// \return The normal form of the term.
     203             :     //  Added bij JFG, to avoid the use of find_free_variables in the function operator() with
     204             :     //  an arbitrary SubstitionFunction, as this is prohibitively costly.
     205      109026 :     data_expression operator()(const data_expression& d, substitution_type& sigma) const
     206             :     {
     207      109026 :       data_expression result;
     208      109026 :       (*this)(result, d, sigma);
     209      109026 :       return result;
     210           0 :     }
     211             : 
     212             :     /// \brief Rewrites the data expression d, and on the fly applies a substitution function
     213             :     /// to data variables.
     214             :     /// \param[out] result The normal form of the term is put in resul is put in result
     215             :     /// \param[in] d A data expression.
     216             :     /// \param[in] sigma A substitutionA. function
     217             :     //  Added bij JFG, to avoid the use of find_free_variables in the function operator() with
     218             :     //  an arbitrary SubstitionFunction, as this is prohibitively costly.
     219      269912 :     void operator()(data_expression& result, const data_expression& d, substitution_type& sigma) const
     220             :     {
     221             : #ifdef MCRL2_COUNT_DATA_REWRITE_CALLS
     222             :       rewrite_calls++;
     223             : #endif
     224             : #ifdef MCRL2_PRINT_REWRITE_STEPS
     225             :       mCRL2log(log::debug) << "REWRITE " << d << "\n";
     226             : #endif
     227      269912 :       m_rewriter->rewrite(result,d,sigma);
     228             : #ifdef MCRL2_PRINT_REWRITE_STEPS
     229             :       mCRL2log(log::debug) << " ------------> " << result << std::endl;
     230             : #endif
     231      269912 :     }
     232             : 
     233        8452 :     ~rewriter()
     234             :     {
     235             : #ifdef MCRL2_COUNT_DATA_REWRITE_CALLS
     236             :       std::cout << "number of data rewrite calls: " << rewrite_calls << std::endl;
     237             : #endif
     238        8452 :     }
     239             : };
     240             : 
     241             : } // namespace data
     242             : 
     243             : } // namespace mcrl2
     244             : 
     245             : #endif // MCRL2_DATA_REWRITER_H