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

Generated by: LCOV version 1.12