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/rewriters/one_point_rule_rewriter.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_DATA_REWRITERS_ONE_POINT_RULE_REWRITER_H
      13             : #define MCRL2_DATA_REWRITERS_ONE_POINT_RULE_REWRITER_H
      14             : 
      15             : #include "mcrl2/data/equality_one_point_substitution.h"
      16             : #include "mcrl2/data/expression_traits.h"
      17             : #include "mcrl2/data/find_equalities.h"
      18             : #include "mcrl2/data/optimized_boolean_operators.h"
      19             : #include "mcrl2/data/replace.h"
      20             : #include "mcrl2/data/substitutions/mutable_map_substitution.h"
      21             : 
      22             : namespace mcrl2::data
      23             : {
      24             : 
      25             : namespace detail
      26             : {
      27             : 
      28             : template <typename Derived>
      29             : class one_point_rule_rewrite_builder: public data_expression_builder<Derived>
      30             : {
      31             :   public:
      32             :     typedef data_expression_builder<Derived> super;
      33             : 
      34             :     using super::apply;
      35             : 
      36           2 :     Derived& derived()
      37             :     {
      38           2 :       return static_cast<Derived&>(*this);
      39             :     }
      40             : 
      41             :     template <class T>
      42           1 :     void apply(T& result, const forall& x)
      43             :     {
      44           1 :       data_expression body; 
      45           1 :       derived().apply(body, x.body());
      46           1 :       std::vector<variable> variables;
      47             : 
      48           1 :       std::map<variable, std::set<data_expression> > inequalities = find_inequalities(body);
      49           1 :       if (!inequalities.empty())
      50             :       {
      51           1 :         auto [sigma, remaining_variables] = make_one_point_rule_substitution(inequalities, x.variables());
      52           1 :         if (remaining_variables.size() != x.variables().size()) // one or more substitutions were found
      53             :         {
      54           1 :           mCRL2log(log::debug) << "Apply substitution sigma = " << sigma << " to x = " << body << std::endl;
      55           1 :           body = data::replace_variables_capture_avoiding(body, sigma);
      56           1 :           mCRL2log(log::debug) << "sigma(x) = " << body << std::endl;
      57           1 :           if (remaining_variables.empty())
      58             :           {
      59           1 :             mCRL2log(log::debug) << "Replaced " << x << "\nwith " << body << std::endl;
      60           1 :             result = body;
      61           1 :             return;
      62             :           }
      63           0 :           data::variable_list v(remaining_variables.begin(), remaining_variables.end());
      64           0 :           mCRL2log(log::debug) << "Replaced " << x << "\nwith " << forall(v, body) << std::endl;
      65           0 :           make_forall(result, v, body);
      66           0 :           return;
      67           0 :         }
      68           1 :       }
      69           0 :       make_forall(result, x.variables(), body);
      70           3 :     }
      71             : 
      72             :     template <class T>
      73           1 :     void apply(T& result, const exists& x)
      74             :     {
      75           1 :       data_expression body;
      76           1 :       derived().apply(body, x.body());
      77           1 :       std::vector<variable> variables;
      78             : 
      79           1 :       std::map<variable, std::set<data_expression> > equalities = find_equalities(body);
      80           1 :       if (!equalities.empty())
      81             :       {
      82           1 :         auto [sigma, remaining_variables] = make_one_point_rule_substitution(equalities, x.variables());
      83           1 :         if (remaining_variables.size() != x.variables().size()) // one or more substitutions were found
      84             :         {
      85           1 :           mCRL2log(log::debug) << "Apply substitution sigma = " << sigma << " to x = " << body << std::endl;
      86           1 :           body = data::replace_variables_capture_avoiding(body, sigma);
      87           1 :           mCRL2log(log::debug) << "sigma(x) = " << body << std::endl;
      88           1 :           if (remaining_variables.empty())
      89             :           {
      90           1 :             mCRL2log(log::debug) << "Replaced " << x << "\nwith " << body << std::endl;
      91           1 :             result = body;
      92           1 :             return;
      93             :           }
      94           0 :           data::variable_list v(remaining_variables.begin(), remaining_variables.end());
      95           0 :           mCRL2log(log::debug) << "Replaced " << x << "\nwith " << exists(v, body) << std::endl;
      96           0 :           make_exists(result, v, body);
      97           0 :           return;
      98           0 :         }
      99           1 :       }
     100           0 :       make_exists(result, x.variables(), body);
     101           3 :     }
     102             : };
     103             : 
     104             : } // namespace detail
     105             : 
     106             : struct one_point_rule_rewriter
     107             : {
     108             :   using argument_type = data_expression;
     109             :   using result_type = data_expression;
     110             : 
     111        1383 :   data_expression operator()(const data_expression& x) const
     112             :   {
     113        1383 :     data_expression result;
     114        1383 :     core::make_apply_builder<detail::one_point_rule_rewrite_builder>().apply(result, x);
     115        1383 :     return result;
     116           0 :   }
     117             : };
     118             : 
     119             : template <typename T>
     120             : void one_point_rule_rewrite(T& x, typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = 0)
     121             : {
     122             :   core::make_update_apply_builder<data::data_expression_builder>(one_point_rule_rewriter()).update(x);
     123             : }
     124             : 
     125             : template <typename T>
     126             : T one_point_rule_rewrite(const T& x, typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = 0)
     127             : {
     128             :   T result;
     129             :   core::make_update_apply_builder<data::data_expression_builder>(one_point_rule_rewriter()).apply(result, x);
     130             :   return result;
     131             : }
     132             : 
     133             : } // namespace mcrl2::data
     134             : 
     135             : #endif // MCRL2_DATA_REWRITERS_ONE_POINT_RULE_REWRITER_H