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/data/rewriters/quantifiers_inside_rewriter.h"
      16             : #include "mcrl2/pbes/builder.h"
      17             : #include "mcrl2/pbes/join.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             : template <typename BinaryOperation>
      30           0 : std::tuple<pbes_expression, pbes_expression> compute_Phi_Psi(const std::vector<pbes_expression>& X, const std::set<data::variable>& V, BinaryOperation op, pbes_expression empty_sequence_result)
      31             : {
      32             :   using utilities::detail::set_difference;
      33             :   using utilities::detail::set_intersection;
      34             : 
      35           0 :   std::vector<std::set<data::variable>> vars; // free variables
      36           0 :   for (const pbes_expression& x_j: X)
      37             :   {
      38           0 :     vars.push_back(set_intersection(find_free_variables(x_j), V));
      39             :   }
      40           0 :   auto j = std::min_element(vars.begin(), vars.end(),
      41           0 :                             [&](const std::set<data::variable>& x, const std::set<data::variable>& y)
      42             :                             {
      43           0 :                               return x.size() < y.size();
      44             :                             }
      45             :   );
      46           0 :   const std::set<data::variable>& Z = *j;
      47             : 
      48           0 :   std::vector<pbes_expression> phi;
      49           0 :   std::vector<pbes_expression> psi;
      50           0 :   for (std::size_t i = 0; i < X.size(); i++)
      51             :   {
      52           0 :     if (std::includes(Z.begin(), Z.end(), vars[i].begin(), vars[i].end()))
      53             :     {
      54           0 :       phi.push_back(X[i]);
      55             :     }
      56             :     else
      57             :     {
      58           0 :       psi.push_back(X[i]);
      59             :     }
      60             :   }
      61           0 :   pbes_expression Phi = utilities::detail::join(phi.begin(), phi.end(), op, empty_sequence_result);
      62           0 :   pbes_expression Psi = utilities::detail::join(psi.begin(), psi.end(), op, empty_sequence_result);
      63           0 :   return { Phi, Psi };
      64           0 : }
      65             : 
      66             : struct quantifiers_inside_builder: public pbes_expression_builder<quantifiers_inside_builder>
      67             : {
      68             :   typedef pbes_expression_builder<quantifiers_inside_builder> super;
      69             :   using super::apply;
      70             : 
      71             :   template <class T>
      72           0 :   void apply(T& result, const forall& x)
      73             :   {
      74           0 :     pbes_expression const& phi = x.body();
      75           0 :     std::set<data::variable> W = data::detail::make_variable_set(x.variables());
      76           0 :     apply(result, phi);
      77           0 :     result = quantifiers_inside_forall(W, result);
      78           0 :   }
      79             : 
      80             :   template <class T>
      81           0 :   void apply(T& result, const exists& x)
      82             :   {
      83           0 :     pbes_expression const& phi = x.body();
      84           0 :     std::set<data::variable> W = data::detail::make_variable_set(x.variables());
      85           0 :     apply(result, phi);
      86           0 :     result = quantifiers_inside_exists(W, result);
      87           0 :   }
      88             : };
      89             : 
      90             : struct quantifiers_inside_forall_builder: public data_expression_builder<quantifiers_inside_forall_builder>
      91             : {
      92             :   typedef data_expression_builder<quantifiers_inside_forall_builder> super;
      93             :   using super::apply;
      94             : 
      95             :   const std::set<data::variable>& V;
      96             : 
      97           0 :   explicit quantifiers_inside_forall_builder(const std::set<data::variable>& V_)
      98           0 :       : V(V_)
      99           0 :   {}
     100             : 
     101           0 :   static pbes_expression make_forall_(const data::variable_list& vars, const pbes_expression& body)
     102             :   {
     103           0 :     return vars.empty() ? body : forall(vars, body);
     104             :   }
     105             : 
     106             :   // default case
     107             :   template <typename T>
     108           0 :   pbes_expression apply_default(const T& x)
     109             :   {
     110             :     using utilities::detail::set_intersection;
     111           0 :     std::set<data::variable> W = set_intersection(V, find_free_variables(x));
     112           0 :     return make_forall_(data::variable_list(W.begin(), W.end()), x);
     113           0 :   }
     114             : 
     115             :   template <class T>
     116           0 :   void apply(T& result, const forall& x)
     117             :   {
     118             :     using utilities::detail::set_union;
     119           0 :     std::set<data::variable> W = data::detail::make_variable_set(x.variables());
     120           0 :     result = quantifiers_inside_forall(set_union(V, W), x.body());
     121           0 :   }
     122             : 
     123             :   template <class T>
     124           0 :   void apply(T& result, const not_& x)
     125             :   {
     126           0 :     const auto& phi = x.operand();
     127           0 :     result = not_(quantifiers_inside_exists(V, phi));
     128           0 :   }
     129             : 
     130             :   template <class T>
     131           0 :   void apply(T& result, const and_& x)
     132             :   {
     133           0 :     const pbes_expression& phi = x.left();
     134           0 :     const pbes_expression& psi = x.right();
     135           0 :     make_and_(result, quantifiers_inside_forall(V, phi), quantifiers_inside_forall(V, psi));
     136           0 :   }
     137             : 
     138             :   template <class T>
     139           0 :   void apply(T& result, const or_& x)
     140             :   {
     141             :     using utilities::detail::set_difference;
     142             :     using utilities::detail::set_intersection;
     143             :     typedef core::term_traits<pbes_expression> tr;
     144             : 
     145           0 :     std::vector<pbes_expression> X;
     146           0 :     utilities::detail::split(x, std::back_inserter(X), tr::is_or, tr::left, tr::right);
     147           0 :     const auto [Phi, Psi] = compute_Phi_Psi(X, V, tr::or_, tr::false_());
     148           0 :     if (is_false(Psi))
     149             :     {
     150           0 :       result = make_forall_(data::detail::make_variable_list(set_intersection(V, find_free_variables(x))), x);
     151           0 :       return;
     152             :     }
     153           0 :     std::set<data::variable> vars_Phi = find_free_variables(Phi);
     154           0 :     std::set<data::variable> vars_Psi = find_free_variables(Psi);
     155           0 :     optimized_or(result,
     156             :                  quantifiers_inside_forall(set_difference(set_intersection(V, vars_Phi), vars_Psi), Phi),
     157             :                  quantifiers_inside_forall(set_difference(set_intersection(V, vars_Psi), vars_Phi), Psi));
     158           0 :     result = make_forall_(data::detail::make_variable_list(set_intersection(V, set_intersection(vars_Phi, vars_Psi))),
     159             :                           result);
     160           0 :   }
     161             : 
     162             :   template <class T>
     163           0 :   void apply(T& result, const imp& x)
     164             :   {
     165           0 :     result = quantifiers_inside_forall(V, or_(not_(x.left()), x.right()));
     166           0 :   }
     167             : 
     168             :   template <class T>
     169           0 :   void apply(T& result, const propositional_variable_instantiation& x)
     170             :   {
     171           0 :     result = apply_default(x);
     172           0 :   }
     173             : 
     174             :   template <class T>
     175           0 :   void apply(T& result, const exists& x)
     176             :   {
     177           0 :     result = apply_default(x);
     178           0 :   }
     179             : 
     180             :   template <class T>
     181           0 :   void apply(T& result, const data::data_expression& x)
     182             :   {
     183           0 :     result = data::detail::quantifiers_inside_forall(V, x);
     184           0 :   }
     185             : };
     186             : 
     187             : struct quantifiers_inside_exists_builder: public pbes_expression_builder<quantifiers_inside_exists_builder>
     188             : {
     189             :   typedef pbes_expression_builder<quantifiers_inside_exists_builder> super;
     190             :   using super::apply;
     191             : 
     192             :   const std::set<data::variable>& V;
     193             : 
     194           0 :   explicit quantifiers_inside_exists_builder(const std::set<data::variable>& V_)
     195           0 :       : V(V_)
     196           0 :   {}
     197             : 
     198           0 :   static pbes_expression make_exists_(const data::variable_list& vars, const pbes_expression& body)
     199             :   {
     200           0 :     return vars.empty() ? body : exists(vars, body);
     201             :   }
     202             : 
     203             :   // default case
     204             :   template <typename T>
     205           0 :   pbes_expression apply_default(const T& x)
     206             :   {
     207             :     using utilities::detail::set_intersection;
     208           0 :     std::set<data::variable> W = set_intersection(V, find_free_variables(x));
     209           0 :     return make_exists_(data::variable_list(W.begin(), W.end()), x);
     210           0 :   }
     211             : 
     212             :   template <class T>
     213           0 :   void apply(T& result, const exists& x)
     214             :   {
     215             :     using utilities::detail::set_union;
     216           0 :     std::set<data::variable> W = data::detail::make_variable_set(x.variables());
     217           0 :     result = quantifiers_inside_exists(set_union(V, W), x.body());
     218           0 :   }
     219             : 
     220             :   template <class T>
     221           0 :   void apply(T& result, const not_& x)
     222             :   {
     223           0 :     const auto& phi = x.operand();
     224           0 :     result = not_(quantifiers_inside_forall(V, phi));
     225           0 :   }
     226             : 
     227             :   template <class T>
     228           0 :   void apply(T& result, const or_& x)
     229             :   {
     230           0 :     const pbes_expression& phi = x.left();
     231           0 :     const pbes_expression& psi = x.right();
     232           0 :     result = or_(quantifiers_inside_exists(V, phi), quantifiers_inside_exists(V, psi));
     233           0 :   }
     234             : 
     235             :   template <class T>
     236           0 :   void apply(T& result, const and_& x)
     237             :   {
     238             :     using utilities::detail::set_difference;
     239             :     using utilities::detail::set_intersection;
     240             :     typedef core::term_traits<pbes_expression> tr;
     241             : 
     242           0 :     std::vector<pbes_expression> X;
     243           0 :     utilities::detail::split(x, std::back_inserter(X), tr::is_and, tr::left, tr::right);
     244           0 :     const auto [Phi, Psi] = compute_Phi_Psi(X, V, tr::and_, tr::true_());
     245           0 :     if (is_true(Psi))
     246             :     {
     247           0 :       result = make_exists_(data::detail::make_variable_list(set_intersection(V, find_free_variables(x))), x);
     248           0 :       return;
     249             :     }
     250           0 :     std::set<data::variable> vars_Phi = find_free_variables(Phi);
     251           0 :     std::set<data::variable> vars_Psi = find_free_variables(Psi);
     252           0 :     optimized_and(result,
     253             :                   quantifiers_inside_exists(set_difference(set_intersection(V, vars_Phi), vars_Psi), Phi),
     254             :                   quantifiers_inside_exists(set_difference(set_intersection(V, vars_Psi), vars_Phi), Psi));
     255           0 :     result = make_exists_(data::detail::make_variable_list(set_intersection(V, set_intersection(vars_Phi, vars_Psi))),
     256             :                           result);
     257           0 :   }
     258             : 
     259             :   template <class T>
     260           0 :   void apply(T& result, const imp& x)
     261             :   {
     262           0 :     result = quantifiers_inside_exists(V, and_(not_(x.left()), x.right()));
     263           0 :   }
     264             : 
     265             :   template <class T>
     266           0 :   void apply(T& result, const propositional_variable_instantiation& x)
     267             :   {
     268           0 :     result = apply_default(x);
     269           0 :   }
     270             : 
     271             :   template <class T>
     272           0 :   void apply(T& result, const forall& x)
     273             :   {
     274           0 :     result = apply_default(x);
     275           0 :   }
     276             : 
     277             :   template <class T>
     278           0 :   void apply(T& result, const data::data_expression& x)
     279             :   {
     280           0 :     result = data::detail::quantifiers_inside_exists(V, x);
     281           0 :   }
     282             : };
     283             : 
     284             : inline
     285           0 : pbes_expression quantifiers_inside(const pbes_expression& x)
     286             : {
     287             :   quantifiers_inside_builder f;
     288           0 :   pbes_expression result;
     289           0 :   f.apply(result, x);
     290           0 :   return result;
     291           0 : }
     292             : 
     293             : inline
     294           0 : pbes_expression quantifiers_inside_forall(const std::set<data::variable>& variables, const pbes_expression& x)
     295             : {
     296           0 :   quantifiers_inside_forall_builder f(variables);
     297           0 :   pbes_expression result;
     298           0 :   f.apply(result, x);
     299           0 :   return result;
     300           0 : }
     301             : 
     302             : inline
     303           0 : pbes_expression quantifiers_inside_exists(const std::set<data::variable>& variables, const pbes_expression& x)
     304             : {
     305           0 :   quantifiers_inside_exists_builder f(variables);
     306           0 :   pbes_expression result;
     307           0 :   f.apply(result, x);
     308           0 :   return result;
     309           0 : }
     310             : 
     311             : } // namespace detail
     312             : 
     313             : /// \brief A rewriter that pushes quantifiers inside in a PBES expression.
     314             : class quantifiers_inside_rewriter
     315             : {
     316             :   public:
     317             :     /// \brief The term type
     318             :     typedef pbes_expression term_type;
     319             : 
     320             :     /// \brief The variable type
     321             :     typedef data::variable variable_type;
     322             : 
     323             :     /// \brief Rewrites a pbes expression.
     324             :     /// \param x A term
     325             :     /// \return The rewrite result.
     326           0 :     pbes_expression operator()(const pbes_expression& x) const
     327             :     {
     328           0 :       return detail::quantifiers_inside(x);
     329             :     }
     330             : };
     331             : 
     332             : } // namespace pbes_system
     333             : 
     334             : } // namespace mcrl2
     335             : 
     336             : #endif // MCRL2_PBES_REWRITERS_QUANTIFIERS_INSIDE_REWRITER_H