Line data    Source code

       1             : // Author(s): Gijs Kant
       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/detail/bqnf_quantifier_rewriter.h
      10             : /// \brief Replaces universal quantifier over conjuncts with conjuncts over universal quantifiers:
      11             : /// rewrite_bqnf_expression(forall x . /\_i phi_i) =
      12             : ///   /\_i forall (x intersection free(phi_i)) . phi_i.
      13             : /// This rewriter is experimental.
      14             : #ifndef MCRL2_PBES_DETAIL_BQNF_QUANTIFIER_REWRITER_H
      15             : #define MCRL2_PBES_DETAIL_BQNF_QUANTIFIER_REWRITER_H
      16             : 
      17             : #include "mcrl2/pbes/detail/bqnf_visitor.h"
      18             : 
      19             : namespace mcrl2 {
      20             : 
      21             : namespace pbes_system {
      22             : 
      23             : namespace detail {
      24             : 
      25             : struct bqnf_quantifier_rewriter: public bqnf_visitor
      26             :   {
      27             :     /// \brief Constructor.
      28           1 :     bqnf_quantifier_rewriter()
      29           1 :     {
      30           1 :     }
      31             : 
      32             : 
      33             :     /// \brief Filters the expression e such that subexpressions that are data expression that
      34             :     /// do not refer to variables in the set d are discarded:
      35             :     /// filter(e, d) = e if e is a data expression and the intersection of free(e) and d is not empty;
      36             :     /// filter(e1 'op' e2, d) = filter(e1, d) 'op' filter(e2, d).
      37             :     /// \param e a simple PBES expression.
      38             :     /// \param d a set of variables.
      39             :     /// \return the filtered expression.
      40           0 :     virtual pbes_expression filter(const pbes_expression& e, const std::set<data::variable>& d)
      41             :     {
      42           0 :       assert(is_simple_expression(e));
      43           0 :       pbes_expression empty;
      44           0 :       if (is_data(e))
      45             :       {
      46           0 :         std::vector<data::variable> intersection;
      47           0 :         for (const data::variable& var: pbes_system::find_free_variables(e))
      48             :         {
      49           0 :           if (d.find(var) != d.end())
      50             :           {
      51           0 :             intersection.push_back(var);
      52             :           }
      53           0 :         }
      54           0 :         if (intersection.empty())
      55             :         {
      56           0 :           return e;
      57             :         }
      58             :         else
      59             :         {
      60           0 :           return empty;
      61             :         }
      62           0 :       }
      63           0 :       else if (is_and(e) || is_or(e) || is_imp(e))
      64             :       {
      65           0 :         pbes_expression l = filter(pbes_system::accessors::left(e), d);
      66           0 :         pbes_expression r = filter(pbes_system::accessors::right(e), d);
      67           0 :         if (l==empty && r==empty)
      68             :         {
      69           0 :           return empty;
      70             :         }
      71           0 :         else if (l==empty)
      72             :         {
      73           0 :           return r;
      74             :         }
      75           0 :         else if (r==empty)
      76             :         {
      77           0 :           if (is_imp(e))
      78             :           {
      79           0 :             return not_(l);
      80             :           }
      81             :           else
      82             :           {
      83           0 :             return l;
      84             :           }
      85             :         }
      86             :         else
      87             :         {
      88           0 :           if (is_and(e))
      89             :           {
      90           0 :             return and_(l, r);
      91             :           }
      92           0 :           else if (is_or(e))
      93             :           {
      94           0 :             return or_(l, r);
      95             :           }
      96             :           else // is_imp(e)
      97             :           {
      98           0 :             return imp(l, r);
      99             :           }
     100             :         }
     101           0 :       }
     102             :       else
     103             :       {
     104           0 :         std::clog << "filter: Unexpected expression: " << pp(e) << std::endl;
     105           0 :         throw(std::runtime_error("filter: Unexpected expression."));
     106             :       }
     107           0 :     }
     108             : 
     109             : 
     110             : 
     111             :     /// \brief Filters a 'guard' g with respect to a set of variables d and
     112             :     /// an expression phi_i such that parts of g that not relevant for phi_i
     113             :     /// are discarded.
     114             :     /// filter_guard(g, phi_i, d) = ( exists_{d intersects (free(g) - free(phi_i))} . filter(g, {d - free(phi_i)))
     115             :     ///   && filter(g, d intersects free(phi_i)).
     116             :     /// \param g a simple expression that functions as guard.
     117             :     /// \param phi_i a PBES expression.
     118             :     /// \param d a set of relevant variables.
     119             :     /// \return the expression g filtered with respect to phi_i and d.
     120           0 :     virtual pbes_expression filter_guard(const pbes_expression& g, const pbes_expression& phi_i, const data::variable_list& d)
     121             :     {
     122           0 :       pbes_expression result = true_();
     123           0 :       data::variable_list free_g = free_variables(g);
     124           0 :       std::set<data::variable> free_phi_i;
     125           0 :       for (const data::variable& v: pbes_system::find_free_variables(phi_i))
     126             :       {
     127           0 :         free_phi_i.insert(v);
     128           0 :       }
     129           0 :       std::set<data::variable> free_g_minus_free_phi_i;
     130           0 :       for (const data::variable& var: free_g)
     131             :       {
     132           0 :         if (free_phi_i.find(var)==free_phi_i.end()) { // !free_phi_i.contains(v)
     133           0 :           free_g_minus_free_phi_i.insert(var);
     134             :         }
     135             :       }
     136           0 :       std::vector<data::variable> d_intersects_free_g_minus_free_phi_i;
     137           0 :       std::set<data::variable> d_minus_free_phi_i;
     138           0 :       std::set<data::variable> d_intersects_free_phi_i;
     139           0 :       for (const data::variable& var: d)
     140             :       {
     141           0 :         if (free_g_minus_free_phi_i.find(var) != free_g_minus_free_phi_i.end()) // free_g_minus_free_phi_i.contains(v)
     142             :         {
     143           0 :           d_intersects_free_g_minus_free_phi_i.push_back(var);
     144             :         }
     145           0 :         if (free_phi_i.find(var) != free_phi_i.end()) // free_phi_i.contains(v)
     146             :         {
     147           0 :           d_intersects_free_phi_i.insert(var);
     148             :         }
     149             :         else
     150             :         {
     151           0 :           d_minus_free_phi_i.insert(var);
     152             :         }
     153             :       }
     154             :       // Now I have the sets I need; let's generate terms.
     155           0 :       pbes_expression e_1 = filter(g, d_minus_free_phi_i);
     156           0 :       if (!d_intersects_free_g_minus_free_phi_i.empty())
     157             :       {
     158             :         e_1 =
     159             : // data::exists(    // N.B. Removing this, since it does not make sense to convert a pbes_system::exists to a data::exists (Wieger).
     160           0 :             make_exists_(
     161           0 :             data::variable_list(d_intersects_free_g_minus_free_phi_i.begin(), d_intersects_free_g_minus_free_phi_i.end()),
     162           0 :             e_1)
     163             : // )
     164             :            ;
     165             :       }
     166           0 :       pbes_expression e_2 = filter(g, d_intersects_free_phi_i);
     167           0 :       pbes_expression empty;
     168           0 :       if (e_1 == empty)
     169             :       {
     170           0 :         if (e_2 != empty)
     171             :         {
     172           0 :           result = e_2;
     173             :         }
     174             :       }
     175             :       else
     176             :       {
     177           0 :         if (e_2 == empty)
     178             :         {
     179           0 :           result = e_1;
     180             :         }
     181             :         else
     182             :         {
     183           0 :           result = and_(e_1, e_2);
     184             :         }
     185             :       }
     186           0 :       return result;
     187           0 :     }
     188             : 
     189             : 
     190             :     /// \brief Rewrites a bounded universal quantifier expression.
     191             :     /// If the subexpression is a conjunction, the quantifier over the conjunction
     192             :     /// is transformed to a conjunction of quantifier expressions.
     193             :     /// rewrite_bounded_forall(forall x . phi => /\_i psi_i) =
     194             :     ///   /\_i forall (x intersection free(psi_i)) .
     195             :     ///   filter_guard(phi, psi_i, x) => rewrite_bqnf_expression(psi_i).
     196             :     /// \param e a PBES expression
     197             :     /// \return the expression resulting from the transformation.
     198           1 :     virtual pbes_expression rewrite_bounded_forall(const pbes_expression& e)
     199             :     {
     200             :       //std::clog << "rewrite_bounded_forall: " << pp(e) << std::endl;
     201           1 :       assert(is_forall(e));
     202           1 :       data::variable_list qvars = quantifier_variables(e);
     203           1 :       pbes_expression qexpr = pbes_system::accessors::arg(e);
     204           1 :       while (is_forall(qexpr)) {
     205           0 :         qvars = qvars + quantifier_variables(qexpr);
     206           0 :         qexpr = pbes_system::accessors::arg(qexpr);
     207             :       }
     208             :       // forall qvars . qexpr
     209           1 :       pbes_expression result;
     210           1 :       if (is_propositional_variable_instantiation(qexpr) || is_simple_expression(qexpr)) {
     211             :         // forall d . phi | forall d . X(e)
     212           0 :         result = e;
     213             :       } else {
     214           1 :         pbes_expression phi = is_or(qexpr) ? static_cast<const pbes_expression&>(true_()) : static_cast<const pbes_expression&>(false_());
     215           1 :         pbes_expression psi = qexpr;
     216           1 :         if (is_or(qexpr) || is_imp(qexpr)) {
     217           0 :           pbes_expression l = pbes_system::accessors::left(qexpr);
     218           0 :           pbes_expression r = pbes_system::accessors::right(qexpr);
     219           0 :           if (is_simple_expression(l)) {
     220           0 :             phi = l;
     221           0 :             psi = r;
     222             :           }
     223           0 :         }
     224           1 :         if (is_propositional_variable_instantiation(psi)) {
     225             :           // forall d . phi => X(e)
     226           0 :           result = e;
     227           1 :         } else if (!qvars.empty() || !(is_or(qexpr) ? is_true(phi) : is_false(phi))) {
     228             :           // forall d . phi => psi
     229           1 :           std::vector<pbes_expression> conjuncts;
     230           1 :           if (is_and(psi)) {
     231           1 :             conjuncts = split_conjuncts(psi);
     232             :           } else {
     233           0 :             conjuncts.push_back(psi);
     234             :           }
     235           1 :           pbes_expression conjunction = true_();
     236           3 :           for (std::vector<pbes_expression>::const_iterator c = conjuncts.begin(); c != conjuncts.end(); ++c) {
     237           2 :             pbes_expression phi_i = *c;
     238           2 :             pbes_expression r = rewrite_bqnf_expression(phi_i);
     239           2 :             if (is_or(qexpr)) {
     240           0 :               if (!is_true(phi)) {
     241           0 :                 phi = filter_guard(phi, r, qvars);
     242           0 :                 r = or_(phi, r);
     243             :               }
     244             :             } else {
     245           2 :               if (!is_false(phi)) {
     246           0 :                 phi = filter_guard(phi, r, qvars);
     247           0 :                 r = imp(phi, r);
     248             :               }
     249             :             }
     250           2 :             std::vector<data::variable> qvars_i;
     251           2 :             std::set<data::variable> free_phi_i;
     252           4 :             for (const data::variable& v : pbes_system::find_free_variables(phi_i))
     253             :             {
     254           2 :               free_phi_i.insert(v);
     255           2 :             }
     256           4 :             for (const data::variable& var: qvars)
     257             :             {
     258           2 :               if (free_phi_i.find(var) != free_phi_i.end()) // free_phi_i.contains(v)
     259             :               {
     260           2 :                 qvars_i.push_back(var);
     261             :               }
     262             :             }
     263             :             // qvars_i = qvars intersects free(phi_i)
     264           2 :             if (!qvars_i.empty()) {
     265           2 :               r = make_forall_(data::variable_list(qvars_i.begin(), qvars_i.end()), r);
     266             :             }
     267           2 :             if (is_true(conjunction)) {
     268           1 :               conjunction = r;
     269             :             } else {
     270           1 :               conjunction = and_(conjunction, r);
     271             :             }
     272           2 :           }
     273           1 :           result = conjunction;
     274           1 :         } else {
     275             :           // qexpr not of the form phi => psi
     276             :           //std::clog << "rewrite_bounded_forall: unexpected qexpr = " << pp(qexpr) << std::endl;
     277           0 :           throw(std::runtime_error("rewrite_bounded_forall: unexpected qexpr."));
     278             :         }
     279           1 :       }
     280           2 :       return result;
     281           1 :     }
     282             : 
     283             : 
     284             : 
     285             :     /// \brief Rewrites a bounded existential quantifier expression.
     286             :     /// rewrite_bounded_exists(exists v . phi) = exists v. rewrite_bqnf_expression(phi)
     287             :     /// \param e a PBES expression
     288             :     /// \return the expression resulting from the transformation.
     289           0 :     virtual pbes_expression rewrite_bounded_exists(const pbes_expression& e)
     290             :     {
     291             :       //std::clog << "rewrite_bounded_exists" << pp(e) << std::endl;
     292           0 :       assert(is_exists(e));
     293           0 :       pbes_expression qexpr = pbes_system::accessors::arg(e);
     294           0 :       data::variable_list qvars = quantifier_variables(e);
     295           0 :       while (is_exists(qexpr)) {
     296           0 :         qvars = qvars + quantifier_variables(qexpr);
     297           0 :         qexpr = pbes_system::accessors::arg(qexpr);
     298             :       }
     299           0 :       pbes_expression r = rewrite_bqnf_expression(qexpr);
     300           0 :       pbes_expression result = make_exists_(qvars, r);
     301           0 :       return result;
     302           0 :     }
     303             : 
     304             : 
     305             :     /// \brief Rewrites a conjunctive expression.
     306             :     /// rewrite_imp(/\_i phi_i) = /\_i rewrite_bqnf_expression(phi_i).
     307             :     /// \param e a PBES expression
     308             :     /// \return the expression resulting from the transformation.
     309           0 :     virtual pbes_expression rewrite_and(const pbes_expression& e)
     310             :     {
     311             :       //std::clog << "rewrite_and: " << pp(e) << std::endl;
     312           0 :       pbes_expression conjunction = true_();
     313           0 :       std::vector<pbes_equation> new_eqns;
     314           0 :       std::vector<pbes_expression> conjuncts = split_conjuncts(e);
     315           0 :       for (std::vector<pbes_expression>::const_iterator c = conjuncts.begin(); c != conjuncts.end(); ++c) {
     316           0 :         pbes_expression expr = *c;
     317           0 :         pbes_expression r = rewrite_bqnf_expression(expr);
     318           0 :         if (is_true(conjunction)) {
     319           0 :           conjunction = r;
     320             :         } else {
     321           0 :           conjunction = and_(conjunction, r);
     322             :         }
     323           0 :       }
     324           0 :       return conjunction;
     325           0 :     }
     326             : 
     327             : 
     328             :     /// \brief Rewrites a disjunctive expression.
     329             :     /// rewrite_imp(\/_i phi_i) = \/_i rewrite_bqnf_expression(phi_i).
     330             :     /// \param e a PBES expression
     331             :     /// \return the expression resulting from the transformation.
     332           2 :     virtual pbes_expression rewrite_or(const pbes_expression& e)
     333             :     {
     334             :       //std::clog << "rewrite_or: " << pp(e) << std::endl;
     335           2 :       pbes_expression disjunction = false_();
     336           2 :       std::vector<pbes_expression> new_exprs;
     337           2 :       std::vector<pbes_expression> disjuncts = split_disjuncts(e);
     338           6 :       for (std::vector<pbes_expression>::const_iterator d = disjuncts.begin(); d != disjuncts.end(); ++d) {
     339           4 :         pbes_expression expr = *d;
     340           4 :         pbes_expression r = rewrite_bqnf_expression(expr);
     341           4 :         if (is_false(disjunction)) {
     342           2 :           disjunction = r;
     343             :         } else {
     344           2 :           disjunction = or_(disjunction, r);
     345             :         }
     346           4 :       }
     347           4 :       return disjunction;
     348           2 :     }
     349             : 
     350             : 
     351             :     /// \brief Rewrites an implication:
     352             :     /// rewrite_imp(phi => psi) =
     353             :     ///   rewrite_bqnf_expression(phi) => rewrite_bqnf_expression(psi).
     354             :     /// \param e a PBES expression
     355             :     /// \return the expression resulting from the transformation.
     356           0 :     virtual pbes_expression rewrite_imp(const pbes_expression& e)
     357             :     {
     358             :       //std::clog << "rewrite_imp: " << pp(e) << std::endl;
     359           0 :       pbes_expression l = rewrite_bqnf_expression(pbes_system::accessors::left(e));
     360           0 :       pbes_expression r = rewrite_bqnf_expression(pbes_system::accessors::right(e));
     361           0 :       pbes_expression result = imp(l, r);
     362           0 :       return result;
     363           0 :     }
     364             : 
     365             : 
     366             :     /// \brief Rewrites a BQNF expression.
     367             :     /// Replaces universal quantifier over conjuncts with conjuncts over universal quantifiers:
     368             :     /// rewrite_bqnf_expression(forall x . /\_i phi_i) =
     369             :     ///   /\_i forall (x intersection free(phi_i)) . phi_i
     370             :     /// For subexpressions the transformation is done in the usual way:
     371             :     /// rewrite_bqnf_expression(phi 'op' psi) =
     372             :     ///   rewrite_bqnf_expression(phi) 'op' rewrite_bqnf_expression(psi).
     373             :     /// \param e a PBES expression
     374             :     /// \return the expression resulting from the transformation.
     375          10 :     virtual pbes_expression rewrite_bqnf_expression(const pbes_expression& e)
     376             :     {
     377             :       //std::clog << "rewrite_bqnf_expression: " << pp(e) << std::endl;
     378          10 :       pbes_expression result;
     379          10 :       if (is_propositional_variable_instantiation(e) || is_simple_expression(e)) {
     380             :         // Eqn of the form sigma X(d: D) = phi && Y(h(d, l)), with phi a simple formula.
     381             :         // Add sigma X(d) = e.
     382           7 :         result = e;
     383           3 :       } else if (is_forall(e)) {
     384           1 :         result = rewrite_bounded_forall(e);
     385           2 :       } else if (is_exists(e)) {
     386           0 :         result = rewrite_bounded_exists(e);
     387           2 :       } else if (is_or(e)) {
     388           2 :         result = rewrite_or(e);
     389           0 :       } else if (is_imp(e)) {
     390           0 :         result = rewrite_imp(e);
     391           0 :       } else if (is_and(e)) {
     392           0 :         result = rewrite_and(e);
     393             :       } else {
     394           0 :         std::clog << "Unexpected expression: " << pp(e) << std::endl;
     395           0 :         throw(std::runtime_error("Unexpected expression."));
     396             :       }
     397          10 :       return result;
     398           0 :     }
     399             : 
     400             :   };
     401             : 
     402             : } // namespace detail
     403             : 
     404             : } // namespace pbes_system
     405             : 
     406             : } // namespace mcrl2
     407             : 
     408             : #endif // MCRL2_PBES_DETAIL_BQNF_QUANTIFIER_REWRITER_H