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/pbes/rewriters/one_point_rule_rewriter.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_REWRITERS_ONE_POINT_RULE_REWRITER_H
      13             : #define MCRL2_PBES_REWRITERS_ONE_POINT_RULE_REWRITER_H
      14             : 
      15             : #include "mcrl2/data/consistency.h"
      16             : #include "mcrl2/data/rewriters/one_point_rule_rewriter.h"
      17             : #include "mcrl2/pbes/find_equalities.h"
      18             : #include "mcrl2/pbes/replace.h"
      19             : 
      20             : namespace mcrl2 {
      21             : 
      22             : namespace pbes_system {
      23             : 
      24             : /// \cond INTERNAL_DOCS
      25             : namespace detail {
      26             : 
      27             : template <typename Derived>
      28             : struct one_point_rule_rewrite_builder: public pbes_system::pbes_expression_builder<Derived>
      29             : {
      30             :   typedef pbes_system::pbes_expression_builder<Derived> super;
      31             :   using super::apply;
      32             : 
      33         247 :   Derived& derived()
      34             :   {
      35         247 :     return static_cast<Derived&>(*this);
      36             :   }
      37             : 
      38             :   template <class T>
      39        1378 :   void apply(T& result, const data::data_expression& x)
      40             :   {
      41             :     data::one_point_rule_rewriter r;
      42        1378 :     result = r(x);
      43        1378 :   }
      44             : 
      45             :   template <class T>
      46         119 :   void apply(T& result, const forall& x)
      47             :   {
      48         119 :     pbes_expression body;
      49         119 :     derived().apply(body, forall(x).body());
      50             : 
      51         119 :     std::map<data::variable, std::set<data::data_expression> > inequalities = find_inequalities(body);
      52         119 :     mCRL2log(log::debug) << "x = " << x << std::endl;
      53         119 :     mCRL2log(log::debug) << "\ninequalities(body) = " << data::print_inequalities(inequalities) << std::endl;
      54         119 :     if (!inequalities.empty())
      55             :     {
      56          25 :       auto p = data::make_one_point_rule_substitution(inequalities, x.variables());
      57          25 :       data::mutable_map_substitution<>& sigma = p.first;
      58          25 :       const std::vector<data::variable>& remaining_variables = p.second;
      59          25 :       if (remaining_variables.size() != x.variables().size()) // one or more substitutions were found
      60             :       {
      61          18 :         mCRL2log(log::debug) << "Apply substitution sigma = " << sigma << " to x = " << body << std::endl;
      62          18 :         body = pbes_system::replace_variables_capture_avoiding(body, sigma);
      63          18 :         mCRL2log(log::debug) << "sigma(x) = " << body << std::endl;
      64          18 :         if (remaining_variables.empty())
      65             :         {
      66          18 :           mCRL2log(log::debug) << "Replaced " << x << "\nwith " << body << std::endl;
      67          18 :           result = body;
      68          18 :           return;
      69             :         }
      70           0 :         data::variable_list v(remaining_variables.begin(), remaining_variables.end());
      71           0 :         mCRL2log(log::debug) << "Replaced " << x << "\nwith " << forall(v, body) << std::endl;
      72           0 :         make_forall(result, v, body);
      73           0 :         return;
      74           0 :       }
      75          25 :     }
      76         101 :     make_forall(result, x.variables(), body);
      77         137 :   }
      78             : 
      79             :   template <class T>
      80         126 :   void apply(T& result, const exists& x)
      81             :   {
      82         126 :     pbes_expression body;
      83         126 :     derived().apply(body, exists(x).body());
      84             : 
      85         126 :     std::map<data::variable, std::set<data::data_expression> > equalities = find_equalities(body);
      86         126 :     mCRL2log(log::debug) << "x = " << body << "\nequalities(x) = " << data::print_inequalities(equalities) << std::endl;
      87         126 :     if (!equalities.empty())
      88             :     {
      89          62 :       auto p = data::make_one_point_rule_substitution(equalities, x.variables());
      90          62 :       data::mutable_map_substitution<>& sigma = p.first;
      91          62 :       const std::vector<data::variable>& remaining_variables = p.second;
      92          62 :       if (remaining_variables.size() != x.variables().size()) // one or more substitutions were found
      93             :       {
      94          55 :         mCRL2log(log::debug) << "Apply substitution sigma = " << sigma << " to x = " << body << std::endl;
      95          55 :         body = pbes_system::replace_variables_capture_avoiding(body, sigma);
      96          55 :         mCRL2log(log::debug) << "sigma(x) = " << body << std::endl;
      97          55 :         if (remaining_variables.empty())
      98             :         {
      99          53 :           mCRL2log(log::debug) << "Replaced " << x << "\nwith " << body << std::endl;
     100          53 :           result = body;
     101          53 :           return;
     102             :         }
     103           2 :         data::variable_list v(remaining_variables.begin(), remaining_variables.end());
     104           2 :         mCRL2log(log::debug) << "Replaced " << x << "\nwith " << exists(v, body) << std::endl;
     105           2 :         make_exists(result, v, body);
     106           2 :         return;
     107           2 :       }
     108          62 :     }
     109          71 :     make_exists(result, x.variables(), body);
     110         181 :   }
     111             : 
     112             :   // TODO: This case was added to prevent a data not to be transformed into a PBES not.
     113             :   // It should not be necessary to do this, but otherwise a PFNF test case fails.
     114             :   template <class T>
     115           2 :   void apply(T& result, const not_& x)
     116             :   {
     117           2 :     pbes_expression operand; 
     118           2 :     derived().apply(operand, x.operand());
     119           2 :     if (data::is_data_expression(operand))
     120             :     {
     121           2 :       result = data::not_(atermpp::down_cast<data::data_expression>(operand));
     122             :     }
     123             :     else
     124             :     {
     125           0 :       result = not_(operand);
     126             :     }
     127           2 :   }
     128             : };
     129             : 
     130             : } // namespace detail
     131             : /// \endcond
     132             : 
     133             : /// \brief A rewriter that applies one point rule quantifier elimination to a PBES.
     134             : class one_point_rule_rewriter
     135             : {
     136             :   public:
     137             :     /// \brief The term type
     138             :     typedef pbes_expression term_type;
     139             : 
     140             :     /// \brief The variable type
     141             :     typedef data::variable variable_type;
     142             : 
     143             :     /// \brief Rewrites a pbes expression.
     144             :     /// \param x A term
     145             :     /// \return The rewrite result.
     146         710 :     pbes_expression operator()(const pbes_expression& x) const
     147             :     {
     148         710 :       pbes_expression result;
     149         710 :       core::make_apply_builder<detail::one_point_rule_rewrite_builder>().apply(result, x);
     150         710 :       return result;
     151           0 :     }
     152             : };
     153             : 
     154             : } // namespace pbes_system
     155             : 
     156             : } // namespace mcrl2
     157             : 
     158             : #endif // MCRL2_PBES_REWRITERS_ONE_POINT_RULE_REWRITER_H