LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes/rewriters - one_point_rule_rewriter.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 46 50 92.0 %
Date: 2020-01-19 00:33:35 Functions: 6 6 100.0 %
Legend: Lines: hit not hit

          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         226 :   Derived& derived()
      34             :   {
      35         226 :     return static_cast<Derived&>(*this);
      36             :   }
      37             : 
      38        1314 :   data::data_expression apply(const data::data_expression& x)
      39             :   {
      40             :     data::one_point_rule_rewriter r;
      41        1314 :     return r(x);
      42             :   }
      43             : 
      44         109 :   pbes_expression apply(const forall& x)
      45             :   {
      46         218 :     pbes_expression body = derived().apply(forall(x).body());
      47             : 
      48         218 :     std::map<data::variable, std::set<data::data_expression> > inequalities = find_inequalities(body);
      49         109 :     mCRL2log(log::debug) << "x = " << x << std::endl;
      50         109 :     mCRL2log(log::debug) << "\ninequalities(body) = " << data::print_inequalities(inequalities) << std::endl;
      51         109 :     if (!inequalities.empty())
      52             :     {
      53          30 :       auto p = data::detail::make_one_point_rule_substitution(inequalities, x.variables());
      54          23 :       data::mutable_map_substitution<>& sigma = p.first;
      55          23 :       const std::vector<data::variable>& remaining_variables = p.second;
      56          23 :       if (remaining_variables.size() != x.variables().size()) // one or more substitutions were found
      57             :       {
      58          16 :         mCRL2log(log::debug) << "Apply substitution sigma = " << sigma << " to x = " << body << std::endl;
      59          16 :         body = pbes_system::replace_variables_capture_avoiding(body, sigma);
      60          16 :         mCRL2log(log::debug) << "sigma(x) = " << body << std::endl;
      61          16 :         if (remaining_variables.empty())
      62             :         {
      63          16 :           mCRL2log(log::debug) << "Replaced " << x << "\nwith " << body << std::endl;
      64          16 :           return body;
      65             :         }
      66           0 :         data::variable_list v(remaining_variables.begin(), remaining_variables.end());
      67           0 :         mCRL2log(log::debug) << "Replaced " << x << "\nwith " << forall(v, body) << std::endl;
      68           0 :         return forall(v, body);
      69             :       }
      70             :     }
      71          93 :     return forall(x.variables(), body);
      72             :   }
      73             : 
      74         115 :   pbes_expression apply(const exists& x)
      75             :   {
      76         230 :     pbes_expression body = derived().apply(exists(x).body());
      77             : 
      78         230 :     std::map<data::variable, std::set<data::data_expression> > equalities = find_equalities(body);
      79         115 :     mCRL2log(log::debug) << "x = " << body << "\nequalities(x) = " << data::print_inequalities(equalities) << std::endl;
      80         115 :     if (!equalities.empty())
      81             :     {
      82          67 :       auto p = data::detail::make_one_point_rule_substitution(equalities, x.variables());
      83          60 :       data::mutable_map_substitution<>& sigma = p.first;
      84          60 :       const std::vector<data::variable>& remaining_variables = p.second;
      85          60 :       if (remaining_variables.size() != x.variables().size()) // one or more substitutions were found
      86             :       {
      87          53 :         mCRL2log(log::debug) << "Apply substitution sigma = " << sigma << " to x = " << body << std::endl;
      88          53 :         body = pbes_system::replace_variables_capture_avoiding(body, sigma);
      89          53 :         mCRL2log(log::debug) << "sigma(x) = " << body << std::endl;
      90          53 :         if (remaining_variables.empty())
      91             :         {
      92          52 :           mCRL2log(log::debug) << "Replaced " << x << "\nwith " << body << std::endl;
      93          52 :           return body;
      94             :         }
      95           2 :         data::variable_list v(remaining_variables.begin(), remaining_variables.end());
      96           1 :         mCRL2log(log::debug) << "Replaced " << x << "\nwith " << exists(v, body) << std::endl;
      97           1 :         return exists(v, body);
      98             :       }
      99             :     }
     100          62 :     return exists(x.variables(), body);
     101             :   }
     102             : 
     103             :   // TODO: This case was added to prevent a data not to be transformed into a PBES not.
     104             :   // It should not be necessary to do this, but otherwise a PFNF test case fails.
     105           2 :   pbes_expression apply(const not_& x)
     106             :   {
     107           4 :     pbes_expression operand = derived().apply(x.operand());
     108           2 :     if (data::is_data_expression(operand))
     109             :     {
     110           2 :       return data::not_(atermpp::down_cast<data::data_expression>(operand));
     111             :     }
     112             :     else
     113             :     {
     114           0 :       return not_(operand);
     115             :     }
     116             :   }
     117             : };
     118             : 
     119             : } // namespace detail
     120             : /// \endcond
     121             : 
     122             : /// \brief A rewriter that applies one point rule quantifier elimination to a PBES.
     123             : class one_point_rule_rewriter
     124             : {
     125             :   public:
     126             :     /// \brief The term type
     127             :     typedef pbes_expression term_type;
     128             : 
     129             :     /// \brief The variable type
     130             :     typedef data::variable variable_type;
     131             : 
     132             :     /// \brief Rewrites a pbes expression.
     133             :     /// \param x A term
     134             :     /// \return The rewrite result.
     135         573 :     pbes_expression operator()(const pbes_expression& x) const
     136             :     {
     137         573 :       return core::make_apply_builder<detail::one_point_rule_rewrite_builder>().apply(x);
     138             :     }
     139             : };
     140             : 
     141             : } // namespace pbes_system
     142             : 
     143             : } // namespace mcrl2
     144             : 
     145             : #endif // MCRL2_PBES_REWRITERS_ONE_POINT_RULE_REWRITER_H

Generated by: LCOV version 1.13