LCOV - code coverage report
Current view: top level - pbes/include/mcrl2/pbes/rewriters - quantifiers_inside_rewriter.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 0 110 0.0 %
Date: 2020-01-19 00:33:35 Functions: 0 31 0.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/quantifiers_inside_rewriter.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_PBES_REWRITERS_QUANTIFIERS_INSIDE_REWRITER_H
      13             : #define MCRL2_PBES_REWRITERS_QUANTIFIERS_INSIDE_REWRITER_H
      14             : 
      15             : #include "mcrl2/pbes/builder.h"
      16             : #include "mcrl2/pbes/join.h"
      17             : 
      18             : namespace mcrl2 {
      19             : 
      20             : namespace pbes_system {
      21             : 
      22             : namespace detail {
      23             : 
      24             : pbes_expression quantifiers_inside(const pbes_expression& x);
      25             : pbes_expression quantifiers_inside_forall(const std::set<data::variable>& variables, const pbes_expression& x);
      26             : pbes_expression quantifiers_inside_exists(const std::set<data::variable>& variables, const pbes_expression& x);
      27             : 
      28             : inline
      29           0 : std::set<data::variable> make_variable_set(const data::variable_list& x)
      30             : {
      31           0 :   return std::set<data::variable>(x.begin(), x.end());
      32             : }
      33             : 
      34             : struct quantifiers_inside_builder: public pbes_expression_builder<quantifiers_inside_builder>
      35             : {
      36             :   typedef pbes_expression_builder<quantifiers_inside_builder> super;
      37             :   using super::apply;
      38             : 
      39           0 :   pbes_expression apply(const forall& x)
      40             :   {
      41           0 :     auto const& phi = x.body();
      42           0 :     auto W = make_variable_set(x.variables());
      43           0 :     return quantifiers_inside_forall(W, apply(phi));
      44             :   }
      45             : 
      46           0 :   pbes_expression apply(const exists& x)
      47             :   {
      48           0 :     auto const& phi = x.body();
      49           0 :     auto W = make_variable_set(x.variables());
      50           0 :     return quantifiers_inside_exists(W, apply(phi));
      51             :   }
      52             : };
      53             : 
      54             : struct quantifiers_inside_forall_builder: public pbes_expression_builder<quantifiers_inside_forall_builder>
      55             : {
      56             :   typedef pbes_expression_builder<quantifiers_inside_forall_builder> super;
      57             :   using super::apply;
      58             : 
      59             :   const std::set<data::variable>& V;
      60             : 
      61           0 :   quantifiers_inside_forall_builder(const std::set<data::variable>& V_)
      62           0 :     : V(V_)
      63           0 :   {}
      64             : 
      65           0 :   pbes_expression apply(const not_& x)
      66             :   {
      67           0 :     auto const& phi = x.operand();
      68           0 :     return not_(quantifiers_inside_exists(V, phi));
      69             :   }
      70             : 
      71           0 :   pbes_expression apply(const or_& x)
      72             :   {
      73             :     using utilities::detail::set_difference;
      74             :     using utilities::detail::set_intersection;
      75             :     typedef core::term_traits<pbes_system::pbes_expression> tr;
      76             : 
      77           0 :     std::vector<pbes_expression> X;
      78           0 :     utilities::detail::split(x, std::back_inserter(X), tr::is_or, tr::left, tr::right);
      79           0 :     std::vector<std::set<data::variable>> FV;
      80           0 :     for (const pbes_expression& x_i: X)
      81             :     {
      82           0 :       FV.push_back(set_intersection(find_free_variables(x_i), V));
      83             :     }
      84             :     auto i = std::min_element(FV.begin(), FV.end(),
      85           0 :             [&](const std::set<data::variable>& x, const std::set<data::variable>& y)
      86             :             {
      87           0 :               return x.size() < y.size();
      88           0 :             }
      89           0 :            );
      90             : 
      91           0 :     const std::set<data::variable>& W = *i;
      92           0 :     std::vector<pbes_expression> X1;
      93           0 :     std::vector<pbes_expression> X2;
      94           0 :     for (std::size_t j = 0; j < X.size(); j++)
      95             :     {
      96           0 :       if (std::includes(W.begin(), W.end(), FV[j].begin(), FV[j].end()))
      97             :       {
      98           0 :         X2.push_back(X[j]);
      99             :       }
     100             :       else
     101             :       {
     102           0 :         X1.push_back(X[j]);
     103             :       }
     104             :     }
     105           0 :     return make_forall(data::variable_list(W.begin(), W.end()),
     106           0 :                        data::optimized_or(quantifiers_inside_forall(set_difference(V, W), join_or(X1.begin(), X1.end())),
     107           0 :                            join_or(X2.begin(), X2.end()))
     108           0 :                       );
     109             :   }
     110             : 
     111           0 :   pbes_expression apply(const imp& x)
     112             :   {
     113             :     using utilities::detail::set_difference;
     114             :     using utilities::detail::set_intersection;
     115           0 :     auto const& phi = x.left();
     116           0 :     auto const& psi = x.right();
     117           0 :     auto W = set_intersection(set_intersection(V, find_free_variables(phi)), find_free_variables(psi));
     118           0 :     return make_forall(data::variable_list(W.begin(), W.end()),
     119           0 :                        data::optimized_imp(quantifiers_inside_exists(set_difference(V, W), phi),
     120           0 :                            quantifiers_inside_forall(set_difference(V, W), psi)
     121             :                           )
     122           0 :                       );
     123             :   }
     124             : 
     125           0 :   pbes_expression apply(const forall& x)
     126             :   {
     127             :     using utilities::detail::set_union;
     128           0 :     std::set<data::variable> W = make_variable_set(x.variables());
     129           0 :     return quantifiers_inside_forall(set_union(V, W), x.body());
     130             :   }
     131             : 
     132             :   // default case
     133             :   template <typename T>
     134           0 :   pbes_expression apply_default(const T& x)
     135             :   {
     136             :     using utilities::detail::set_intersection;
     137           0 :     auto W = set_intersection(V, find_free_variables(x));
     138           0 :     return make_forall(data::variable_list(W.begin(), W.end()), x);
     139             :   }
     140             : 
     141           0 :   pbes_expression apply(const exists& x)
     142             :   {
     143           0 :     return apply_default(x);
     144             :   }
     145             : 
     146           0 :   pbes_expression apply(const data::data_expression& x)
     147             :   {
     148           0 :     return apply_default(x);
     149             :   }
     150             : 
     151           0 :   pbes_expression apply(const propositional_variable_instantiation& x)
     152             :   {
     153           0 :     return apply_default(x);
     154             :   }
     155             : };
     156             : 
     157             : struct quantifiers_inside_exists_builder: public pbes_expression_builder<quantifiers_inside_exists_builder>
     158             : {
     159             :   typedef pbes_expression_builder<quantifiers_inside_exists_builder> super;
     160             :   using super::apply;
     161             : 
     162             :   const std::set<data::variable>& V;
     163             : 
     164           0 :   quantifiers_inside_exists_builder(const std::set<data::variable>& V_)
     165           0 :     : V(V_)
     166           0 :   {}
     167             : 
     168           0 :   pbes_expression apply(const not_& x)
     169             :   {
     170           0 :     auto const& phi = x.operand();
     171           0 :     return not_(quantifiers_inside_forall(V, phi));
     172             :   }
     173             : 
     174           0 :   pbes_expression apply(const and_& x)
     175             :   {
     176             :     using utilities::detail::set_difference;
     177             :     using utilities::detail::set_intersection;
     178             :     typedef core::term_traits<pbes_system::pbes_expression> tr;
     179             : 
     180           0 :     std::vector<pbes_expression> X;
     181           0 :     utilities::detail::split(x, std::back_inserter(X), tr::is_and, tr::left, tr::right);
     182           0 :     std::vector<std::set<data::variable>> FV;
     183           0 :     for (const pbes_expression& x_i: X)
     184             :     {
     185           0 :       FV.push_back(set_intersection(find_free_variables(x_i), V));
     186             :     }
     187             :     auto i = std::min_element(FV.begin(), FV.end(),
     188           0 :                               [&](const std::set<data::variable>& x, const std::set<data::variable>& y)
     189             :                               {
     190           0 :                                   return x.size() < y.size();
     191           0 :                               }
     192           0 :     );
     193             : 
     194           0 :     const std::set<data::variable>& W = *i;
     195           0 :     std::vector<pbes_expression> X1;
     196           0 :     std::vector<pbes_expression> X2;
     197           0 :     for (std::size_t j = 0; j < X.size(); j++)
     198             :     {
     199           0 :       if (std::includes(W.begin(), W.end(), FV[j].begin(), FV[j].end()))
     200             :       {
     201           0 :         X2.push_back(X[j]);
     202             :       }
     203             :       else
     204             :       {
     205           0 :         X1.push_back(X[j]);
     206             :       }
     207             :     }
     208           0 :     return make_exists(data::variable_list(W.begin(), W.end()),
     209           0 :                        data::optimized_and(quantifiers_inside_exists(set_difference(V, W), join_and(X1.begin(), X1.end())),
     210           0 :                             join_and(X2.begin(), X2.end()))
     211           0 :     );
     212             :   }
     213             : 
     214           0 :   pbes_expression apply(const imp& x)
     215             :   {
     216           0 :     auto const& phi = x.left();
     217           0 :     auto const& psi = x.right();
     218           0 :     return data::optimized_imp(quantifiers_inside_forall(V, phi), quantifiers_inside_exists(V, psi));
     219             :   }
     220             : 
     221           0 :   pbes_expression apply(const exists& x)
     222             :   {
     223             :     using utilities::detail::set_union;
     224           0 :     std::set<data::variable> W = make_variable_set(x.variables());
     225           0 :     return quantifiers_inside_exists(set_union(V, W), x.body());
     226             :   }
     227             : 
     228             :   // default case
     229             :   template <typename T>
     230           0 :   pbes_expression apply_default(const T& x)
     231             :   {
     232             :     using utilities::detail::set_intersection;
     233           0 :     auto W = set_intersection(V, find_free_variables(x));
     234           0 :     return make_exists(data::variable_list(W.begin(), W.end()), x);
     235             :   }
     236             : 
     237           0 :   pbes_expression apply(const forall& x)
     238             :   {
     239           0 :     return apply_default(x);
     240             :   }
     241             : 
     242           0 :   pbes_expression apply(const data::data_expression& x)
     243             :   {
     244           0 :     return apply_default(x);
     245             :   }
     246             : 
     247           0 :   pbes_expression apply(const propositional_variable_instantiation& x)
     248             :   {
     249           0 :     return apply_default(x);
     250             :   }
     251             : };
     252             : 
     253             : inline
     254           0 : pbes_expression quantifiers_inside(const pbes_expression& x)
     255             : {
     256             :   quantifiers_inside_builder f;
     257           0 :   return f.apply(x);
     258             : }
     259             : 
     260             : inline
     261           0 : pbes_expression quantifiers_inside_forall(const std::set<data::variable>& variables, const pbes_expression& x)
     262             : {
     263           0 :   quantifiers_inside_forall_builder f(variables);
     264           0 :   return f.apply(x);
     265             : }
     266             : 
     267             : inline
     268           0 : pbes_expression quantifiers_inside_exists(const std::set<data::variable>& variables, const pbes_expression& x)
     269             : {
     270           0 :   quantifiers_inside_exists_builder f(variables);
     271           0 :   return f.apply(x);
     272             : }
     273             : 
     274             : } // namespace detail
     275             : 
     276             : /// \brief A rewriter that pushes quantifiers inside in a PBES expression.
     277             : class quantifiers_inside_rewriter
     278             : {
     279             :   public:
     280             :     /// \brief The term type
     281             :     typedef pbes_expression term_type;
     282             : 
     283             :     /// \brief The variable type
     284             :     typedef data::variable variable_type;
     285             : 
     286             :     /// \brief Rewrites a pbes expression.
     287             :     /// \param x A term
     288             :     /// \return The rewrite result.
     289           0 :     pbes_expression operator()(const pbes_expression& x) const
     290             :     {
     291           0 :       return detail::quantifiers_inside(x);
     292             :     }
     293             : };
     294             : 
     295             : } // namespace pbes_system
     296             : 
     297             : } // namespace mcrl2
     298             : 
     299             : #endif // MCRL2_PBES_REWRITERS_QUANTIFIERS_INSIDE_REWRITER_H

Generated by: LCOV version 1.13