Line data    Source code

       1             : // Author(s): Jan Friso Groote
       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 strategy_rule.h
      10             : 
      11             : #ifndef MCRL2_DATA_DETAIL_REWRITE_STRATEGY_RULE_H
      12             : #define MCRL2_DATA_DETAIL_REWRITE_STRATEGY_RULE_H
      13             : 
      14             : #include "mcrl2/data/data_equation.h"
      15             : 
      16             : namespace mcrl2
      17             : {
      18             : namespace data
      19             : {
      20             : namespace detail
      21             : {
      22             : 
      23             : /// \brief Is either a rewrite rule to be matched or an index that should be rewritten.
      24             : class strategy_rule 
      25             : {
      26             :   protected:
      27             :     // Only one of the fields rewrite_rule, rewrite_index or cpp_function will be used
      28             :     // at any given time. As this hardly requires a lot of memory, we do not optimise
      29             :     // this using for instance a union type. 
      30             :     enum { data_equation_type, rewrite_index_type, cpp_function_type } m_strategy_element_type;
      31             :     data_equation m_rewrite_rule;
      32             :     size_t m_rewrite_index;
      33             :     std::function<data_expression(const data_expression&)> m_cpp_function;
      34             : 
      35             :   public:
      36      358894 :     strategy_rule(const std::size_t n)
      37      358894 :       : m_strategy_element_type(rewrite_index_type),
      38      358894 :         m_rewrite_index(n)
      39      358894 :     {}
      40             : 
      41        3373 :     strategy_rule(const std::function<data_expression(const data_expression&)> f)
      42        3373 :       :  m_strategy_element_type(cpp_function_type),
      43        3373 :          m_cpp_function(f)
      44        3373 :     {}
      45             : 
      46      582881 :     strategy_rule(const data_equation& eq)
      47      582881 :       : m_strategy_element_type(data_equation_type),
      48      582881 :         m_rewrite_rule(eq)
      49      582881 :     {}
      50             : 
      51     5293407 :     bool is_rewrite_index() const
      52             :     {
      53     5293407 :       return m_strategy_element_type==rewrite_index_type;
      54             :     }
      55             : 
      56     2886856 :     bool is_cpp_code() const
      57             :     {
      58             : 
      59     2886856 :       return m_strategy_element_type==cpp_function_type;
      60             :     }
      61             : 
      62     2886216 :     bool is_equation() const
      63             :     {
      64     2886216 :       return m_strategy_element_type==data_equation_type;
      65             :     }
      66             : 
      67     2886216 :     const data_equation& equation() const
      68             :     {
      69     2886216 :       assert(is_equation());
      70     2886216 :       assert(is_data_equation(m_rewrite_rule));
      71     2886216 :       return m_rewrite_rule;
      72             :     }
      73             : 
      74     1203316 :     std::size_t rewrite_index() const
      75             :     {
      76     1203316 :       assert(is_rewrite_index());
      77     1203316 :       return m_rewrite_index;
      78             :     }
      79             : 
      80         320 :     const std::function<data_expression(const data_expression&)> rewrite_cpp_code() const
      81             :     {
      82         320 :       assert(is_cpp_code());
      83         320 :       return m_cpp_function;
      84             :     }
      85             : };
      86             : 
      87             : /// A strategy is a list of rules and the number of variables that occur in it.
      88             : class strategy
      89             : {
      90             :   protected:
      91             :     std::size_t m_number_of_variables;
      92             :     std::vector<strategy_rule> m_rules;
      93             : 
      94             :   public:
      95             :     /// \brief Default constructor. 
      96      273423 :     strategy(size_t n, const std::vector<strategy_rule>& r)
      97      273423 :      : m_number_of_variables(n),
      98      273423 :        m_rules(r)
      99      273423 :     {}
     100             :    
     101             :     /// \brief Default constructor. 
     102      763637 :     strategy()
     103      763637 :      : m_number_of_variables(0)
     104      763637 :     {}
     105             :   
     106             :     /// \brief Provides the maximal number of variables used in the rewrite rules making up this strategy. 
     107      716050 :     std::size_t number_of_variables() const 
     108             :     { 
     109      716050 :       return m_number_of_variables; 
     110             :     }
     111             : 
     112             :     /// \brief Yield the rules of the strategy. 
     113     1848190 :     const std::vector<strategy_rule>& rules() const 
     114             :     { 
     115     1848190 :       return m_rules; 
     116             :     }
     117             : 
     118             : };
     119             : 
     120             : /// \brief Creates a strategy for given set of rewrite rules with head symbol f.
     121             : strategy create_strategy(data_equation_list rules);
     122             : 
     123             : } // namespace detail
     124             : } // namespace data
     125             : } // namespace mcrl2
     126             : 
     127             : #endif // MCRL2_DATA_DETAIL_REWRITE_STRATEGY_RULE_H
     128             :