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

Generated by: LCOV version 1.12