LCOV - code coverage report
Current view: top level - modal_formula/include/mcrl2/modal_formula - replace.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 11 12 91.7 %
Date: 2020-04-01 00:44:46 Functions: 4 4 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/modal_formula/replace.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_MODAL_FORMULA_REPLACE_H
      13             : #define MCRL2_MODAL_FORMULA_REPLACE_H
      14             : 
      15             : #include "mcrl2/lps/replace.h"
      16             : #include "mcrl2/modal_formula/replace_capture_avoiding.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : 
      21             : namespace action_formulas
      22             : {
      23             : 
      24             : //--- start generated action_formulas replace code ---//
      25             : template <typename T, typename Substitution>
      26             : void replace_sort_expressions(T& x,
      27             :                               const Substitution& sigma,
      28             :                               bool innermost,
      29             :                               typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
      30             :                              )
      31             : {
      32             :   data::detail::make_replace_sort_expressions_builder<action_formulas::sort_expression_builder>(sigma, innermost).update(x);
      33             : }
      34             : 
      35             : template <typename T, typename Substitution>
      36             : T replace_sort_expressions(const T& x,
      37             :                            const Substitution& sigma,
      38             :                            bool innermost,
      39             :                            typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
      40             :                           )
      41             : {
      42             :   return data::detail::make_replace_sort_expressions_builder<action_formulas::sort_expression_builder>(sigma, innermost).apply(x);
      43             : }
      44             : 
      45             : template <typename T, typename Substitution>
      46             : void replace_data_expressions(T& x,
      47             :                               const Substitution& sigma,
      48             :                               bool innermost,
      49             :                               typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
      50             :                              )
      51             : {
      52             :   data::detail::make_replace_data_expressions_builder<action_formulas::data_expression_builder>(sigma, innermost).update(x);
      53             : }
      54             : 
      55             : template <typename T, typename Substitution>
      56             : T replace_data_expressions(const T& x,
      57             :                            const Substitution& sigma,
      58             :                            bool innermost,
      59             :                            typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
      60             :                           )
      61             : {
      62             :   return data::detail::make_replace_data_expressions_builder<action_formulas::data_expression_builder>(sigma, innermost).apply(x);
      63             : }
      64             : 
      65             : template <typename T, typename Substitution>
      66             : void replace_variables(T& x,
      67             :                        const Substitution& sigma,
      68             :                        typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
      69             :                       )
      70             : {
      71             :   core::make_update_apply_builder<action_formulas::data_expression_builder>(sigma).update(x);
      72             : }
      73             : 
      74             : template <typename T, typename Substitution>
      75             : T replace_variables(const T& x,
      76             :                     const Substitution& sigma,
      77             :                     typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
      78             :                    )
      79             : {
      80             :   return core::make_update_apply_builder<action_formulas::data_expression_builder>(sigma).apply(x);
      81             : }
      82             : 
      83             : template <typename T, typename Substitution>
      84             : void replace_all_variables(T& x,
      85             :                            const Substitution& sigma,
      86             :                            typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
      87             :                           )
      88             : {
      89             :   core::make_update_apply_builder<action_formulas::variable_builder>(sigma).update(x);
      90             : }
      91             : 
      92             : template <typename T, typename Substitution>
      93             : T replace_all_variables(const T& x,
      94             :                         const Substitution& sigma,
      95             :                         typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
      96             :                        )
      97             : {
      98             :   return core::make_update_apply_builder<action_formulas::variable_builder>(sigma).apply(x);
      99             : }
     100             : 
     101             : /// \brief Applies the substitution sigma to x.
     102             : /// \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     103             : template <typename T, typename Substitution>
     104             : void replace_free_variables(T& x,
     105             :                             const Substitution& sigma,
     106             :                             typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     107             :                            )
     108             : {
     109             :   assert(data::is_simple_substitution(sigma));
     110             :   data::detail::make_replace_free_variables_builder<action_formulas::data_expression_builder, action_formulas::add_data_variable_builder_binding>(sigma).update(x);
     111             : }
     112             : 
     113             : /// \brief Applies the substitution sigma to x.
     114             : /// \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     115             : template <typename T, typename Substitution>
     116             : T replace_free_variables(const T& x,
     117             :                          const Substitution& sigma,
     118             :                          typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     119             :                         )
     120             : {
     121             :   assert(data::is_simple_substitution(sigma));
     122             :   return data::detail::make_replace_free_variables_builder<action_formulas::data_expression_builder, action_formulas::add_data_variable_builder_binding>(sigma).apply(x);
     123             : }
     124             : 
     125             : /// \brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables.
     126             : /// \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     127             : template <typename T, typename Substitution, typename VariableContainer>
     128             : void replace_free_variables(T& x,
     129             :                             const Substitution& sigma,
     130             :                             const VariableContainer& bound_variables,
     131             :                             typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     132             :                            )
     133             : {
     134             :   assert(data::is_simple_substitution(sigma));
     135             :   data::detail::make_replace_free_variables_builder<action_formulas::data_expression_builder, action_formulas::add_data_variable_builder_binding>(sigma).update(x, bound_variables);
     136             : }
     137             : 
     138             : /// \brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables.
     139             : /// \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     140             : template <typename T, typename Substitution, typename VariableContainer>
     141             : T replace_free_variables(const T& x,
     142             :                          const Substitution& sigma,
     143             :                          const VariableContainer& bound_variables,
     144             :                          typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     145             :                         )
     146             : {
     147             :   assert(data::is_simple_substitution(sigma));
     148             :   return data::detail::make_replace_free_variables_builder<action_formulas::data_expression_builder, action_formulas::add_data_variable_builder_binding>(sigma).apply(x, bound_variables);
     149             : }
     150             : //--- end generated action_formulas replace code ---//
     151             : 
     152             : } // namespace action_formulas
     153             : 
     154             : namespace regular_formulas
     155             : {
     156             : 
     157             : //--- start generated regular_formulas replace code ---//
     158             : template <typename T, typename Substitution>
     159             : void replace_sort_expressions(T& x,
     160             :                               const Substitution& sigma,
     161             :                               bool innermost,
     162             :                               typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     163             :                              )
     164             : {
     165             :   data::detail::make_replace_sort_expressions_builder<regular_formulas::sort_expression_builder>(sigma, innermost).update(x);
     166             : }
     167             : 
     168             : template <typename T, typename Substitution>
     169             : T replace_sort_expressions(const T& x,
     170             :                            const Substitution& sigma,
     171             :                            bool innermost,
     172             :                            typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     173             :                           )
     174             : {
     175             :   return data::detail::make_replace_sort_expressions_builder<regular_formulas::sort_expression_builder>(sigma, innermost).apply(x);
     176             : }
     177             : 
     178             : template <typename T, typename Substitution>
     179             : void replace_data_expressions(T& x,
     180             :                               const Substitution& sigma,
     181             :                               bool innermost,
     182             :                               typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     183             :                              )
     184             : {
     185             :   data::detail::make_replace_data_expressions_builder<regular_formulas::data_expression_builder>(sigma, innermost).update(x);
     186             : }
     187             : 
     188             : template <typename T, typename Substitution>
     189             : T replace_data_expressions(const T& x,
     190             :                            const Substitution& sigma,
     191             :                            bool innermost,
     192             :                            typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     193             :                           )
     194             : {
     195             :   return data::detail::make_replace_data_expressions_builder<regular_formulas::data_expression_builder>(sigma, innermost).apply(x);
     196             : }
     197             : 
     198             : template <typename T, typename Substitution>
     199             : void replace_variables(T& x,
     200             :                        const Substitution& sigma,
     201             :                        typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     202             :                       )
     203             : {
     204             :   core::make_update_apply_builder<regular_formulas::data_expression_builder>(sigma).update(x);
     205             : }
     206             : 
     207             : template <typename T, typename Substitution>
     208             : T replace_variables(const T& x,
     209             :                     const Substitution& sigma,
     210             :                     typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     211             :                    )
     212             : {
     213             :   return core::make_update_apply_builder<regular_formulas::data_expression_builder>(sigma).apply(x);
     214             : }
     215             : 
     216             : template <typename T, typename Substitution>
     217             : void replace_all_variables(T& x,
     218             :                            const Substitution& sigma,
     219             :                            typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     220             :                           )
     221             : {
     222             :   core::make_update_apply_builder<regular_formulas::variable_builder>(sigma).update(x);
     223             : }
     224             : 
     225             : template <typename T, typename Substitution>
     226             : T replace_all_variables(const T& x,
     227             :                         const Substitution& sigma,
     228             :                         typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     229             :                        )
     230             : {
     231             :   return core::make_update_apply_builder<regular_formulas::variable_builder>(sigma).apply(x);
     232             : }
     233             : 
     234             : /// \brief Applies the substitution sigma to x.
     235             : /// \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     236             : template <typename T, typename Substitution>
     237             : void replace_free_variables(T& x,
     238             :                             const Substitution& sigma,
     239             :                             typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     240             :                            )
     241             : {
     242             :   assert(data::is_simple_substitution(sigma));
     243             :   data::detail::make_replace_free_variables_builder<regular_formulas::data_expression_builder, regular_formulas::add_data_variable_builder_binding>(sigma).update(x);
     244             : }
     245             : 
     246             : /// \brief Applies the substitution sigma to x.
     247             : /// \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     248             : template <typename T, typename Substitution>
     249             : T replace_free_variables(const T& x,
     250             :                          const Substitution& sigma,
     251             :                          typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     252             :                         )
     253             : {
     254             :   assert(data::is_simple_substitution(sigma));
     255             :   return data::detail::make_replace_free_variables_builder<regular_formulas::data_expression_builder, regular_formulas::add_data_variable_builder_binding>(sigma).apply(x);
     256             : }
     257             : 
     258             : /// \brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables.
     259             : /// \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     260             : template <typename T, typename Substitution, typename VariableContainer>
     261             : void replace_free_variables(T& x,
     262             :                             const Substitution& sigma,
     263             :                             const VariableContainer& bound_variables,
     264             :                             typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     265             :                            )
     266             : {
     267             :   assert(data::is_simple_substitution(sigma));
     268             :   data::detail::make_replace_free_variables_builder<regular_formulas::data_expression_builder, regular_formulas::add_data_variable_builder_binding>(sigma).update(x, bound_variables);
     269             : }
     270             : 
     271             : /// \brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables.
     272             : /// \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     273             : template <typename T, typename Substitution, typename VariableContainer>
     274             : T replace_free_variables(const T& x,
     275             :                          const Substitution& sigma,
     276             :                          const VariableContainer& bound_variables,
     277             :                          typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     278             :                         )
     279             : {
     280             :   assert(data::is_simple_substitution(sigma));
     281             :   return data::detail::make_replace_free_variables_builder<regular_formulas::data_expression_builder, regular_formulas::add_data_variable_builder_binding>(sigma).apply(x, bound_variables);
     282             : }
     283             : //--- end generated regular_formulas replace code ---//
     284             : 
     285             : } // namespace regular_formulas
     286             : 
     287             : namespace state_formulas
     288             : {
     289             : 
     290             : //--- start generated state_formulas replace code ---//
     291             : template <typename T, typename Substitution>
     292             : void replace_sort_expressions(T& x,
     293             :                               const Substitution& sigma,
     294             :                               bool innermost,
     295             :                               typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     296             :                              )
     297             : {
     298             :   data::detail::make_replace_sort_expressions_builder<state_formulas::sort_expression_builder>(sigma, innermost).update(x);
     299             : }
     300             : 
     301             : template <typename T, typename Substitution>
     302             : T replace_sort_expressions(const T& x,
     303             :                            const Substitution& sigma,
     304             :                            bool innermost,
     305             :                            typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     306             :                           )
     307             : {
     308             :   return data::detail::make_replace_sort_expressions_builder<state_formulas::sort_expression_builder>(sigma, innermost).apply(x);
     309             : }
     310             : 
     311             : template <typename T, typename Substitution>
     312             : void replace_data_expressions(T& x,
     313             :                               const Substitution& sigma,
     314             :                               bool innermost,
     315             :                               typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     316             :                              )
     317             : {
     318             :   data::detail::make_replace_data_expressions_builder<state_formulas::data_expression_builder>(sigma, innermost).update(x);
     319             : }
     320             : 
     321             : template <typename T, typename Substitution>
     322             : T replace_data_expressions(const T& x,
     323             :                            const Substitution& sigma,
     324             :                            bool innermost,
     325             :                            typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     326             :                           )
     327             : {
     328             :   return data::detail::make_replace_data_expressions_builder<state_formulas::data_expression_builder>(sigma, innermost).apply(x);
     329             : }
     330             : 
     331             : template <typename T, typename Substitution>
     332             : void replace_variables(T& x,
     333             :                        const Substitution& sigma,
     334             :                        typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     335             :                       )
     336             : {
     337             :   core::make_update_apply_builder<state_formulas::data_expression_builder>(sigma).update(x);
     338             : }
     339             : 
     340             : template <typename T, typename Substitution>
     341             : T replace_variables(const T& x,
     342             :                     const Substitution& sigma,
     343             :                     typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     344             :                    )
     345             : {
     346             :   return core::make_update_apply_builder<state_formulas::data_expression_builder>(sigma).apply(x);
     347             : }
     348             : 
     349             : template <typename T, typename Substitution>
     350             : void replace_all_variables(T& x,
     351             :                            const Substitution& sigma,
     352             :                            typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     353             :                           )
     354             : {
     355             :   core::make_update_apply_builder<state_formulas::variable_builder>(sigma).update(x);
     356             : }
     357             : 
     358             : template <typename T, typename Substitution>
     359             : T replace_all_variables(const T& x,
     360             :                         const Substitution& sigma,
     361             :                         typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     362             :                        )
     363             : {
     364             :   return core::make_update_apply_builder<state_formulas::variable_builder>(sigma).apply(x);
     365             : }
     366             : 
     367             : /// \brief Applies the substitution sigma to x.
     368             : /// \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     369             : template <typename T, typename Substitution>
     370             : void replace_free_variables(T& x,
     371             :                             const Substitution& sigma,
     372             :                             typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     373             :                            )
     374             : {
     375             :   assert(data::is_simple_substitution(sigma));
     376             :   data::detail::make_replace_free_variables_builder<state_formulas::data_expression_builder, state_formulas::add_data_variable_builder_binding>(sigma).update(x);
     377             : }
     378             : 
     379             : /// \brief Applies the substitution sigma to x.
     380             : /// \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     381             : template <typename T, typename Substitution>
     382             : T replace_free_variables(const T& x,
     383             :                          const Substitution& sigma,
     384             :                          typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     385             :                         )
     386             : {
     387             :   assert(data::is_simple_substitution(sigma));
     388             :   return data::detail::make_replace_free_variables_builder<state_formulas::data_expression_builder, state_formulas::add_data_variable_builder_binding>(sigma).apply(x);
     389             : }
     390             : 
     391             : /// \brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables.
     392             : /// \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     393             : template <typename T, typename Substitution, typename VariableContainer>
     394             : void replace_free_variables(T& x,
     395             :                             const Substitution& sigma,
     396             :                             const VariableContainer& bound_variables,
     397             :                             typename std::enable_if<!std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     398             :                            )
     399             : {
     400             :   assert(data::is_simple_substitution(sigma));
     401             :   data::detail::make_replace_free_variables_builder<state_formulas::data_expression_builder, state_formulas::add_data_variable_builder_binding>(sigma).update(x, bound_variables);
     402             : }
     403             : 
     404             : /// \brief Applies the substitution sigma to x, where the elements of bound_variables are treated as bound variables.
     405             : /// \pre { The substitution sigma must have the property that FV(sigma(x)) is included in {x} for all variables x. }
     406             : template <typename T, typename Substitution, typename VariableContainer>
     407             : T replace_free_variables(const T& x,
     408             :                          const Substitution& sigma,
     409             :                          const VariableContainer& bound_variables,
     410             :                          typename std::enable_if<std::is_base_of<atermpp::aterm, T>::value>::type* = nullptr
     411             :                         )
     412             : {
     413             :   assert(data::is_simple_substitution(sigma));
     414             :   return data::detail::make_replace_free_variables_builder<state_formulas::data_expression_builder, state_formulas::add_data_variable_builder_binding>(sigma).apply(x, bound_variables);
     415             : }
     416             : //--- end generated state_formulas replace code ---//
     417             : 
     418             : namespace detail
     419             : {
     420             : 
     421             : /// \cond INTERNAL_DOCS
     422             : template <template <class> class Builder, class Substitution>
     423             : struct substitute_state_formulas_builder: public Builder<substitute_state_formulas_builder<Builder, Substitution> >
     424             : {
     425             :   typedef Builder<substitute_state_formulas_builder<Builder, Substitution> > super;
     426             :   using super::enter;
     427             :   using super::leave;
     428             :   using super::update;
     429             :   using super::apply;
     430             : 
     431             :   Substitution sigma;
     432             :   bool innermost;
     433             : 
     434           1 :   substitute_state_formulas_builder(Substitution sigma_, bool innermost_)
     435             :     : sigma(sigma_),
     436           1 :       innermost(innermost_)
     437           1 :   {}
     438             : 
     439           5 :   state_formula apply(const state_formula& x)
     440             :   {
     441           5 :     if (innermost)
     442             :     {
     443          10 :       state_formula y = super::apply(x);
     444           5 :       return sigma(y);
     445             :     }
     446           0 :     return sigma(x);
     447             :   }
     448             : };
     449             : 
     450             : template <template <class> class Builder, class Substitution>
     451             : substitute_state_formulas_builder<Builder, Substitution>
     452           1 : make_replace_state_formulas_builder(Substitution sigma, bool innermost)
     453             : {
     454           1 :   return substitute_state_formulas_builder<Builder, Substitution>(sigma, innermost);
     455             : }
     456             : /// \endcond
     457             : 
     458             : } // namespace detail
     459             : 
     460             : template <typename T, typename Substitution>
     461             : void replace_state_formulas(T& x,
     462             :                               Substitution sigma,
     463             :                               bool innermost = true,
     464             :                               typename std::enable_if< !std::is_base_of< atermpp::aterm, T >::value>::type* = 0
     465             :                              )
     466             : {
     467             :   state_formulas::detail::make_replace_state_formulas_builder<state_formulas::state_formula_builder>(sigma, innermost).update(x);
     468             : }
     469             : 
     470             : template <typename T, typename Substitution>
     471           1 : T replace_state_formulas(const T& x,
     472             :                            Substitution sigma,
     473             :                            bool innermost = true,
     474             :                            typename std::enable_if< std::is_base_of< atermpp::aterm, T >::value>::type* = nullptr
     475             :                           )
     476             : {
     477           1 :   return state_formulas::detail::make_replace_state_formulas_builder<state_formulas::state_formula_builder>(sigma, innermost).apply(x);
     478             : }
     479             : 
     480             : } // namespace state_formulas
     481             : 
     482             : } // namespace mcrl2
     483             : 
     484             : #endif // MCRL2_MODAL_FORMULA_REPLACE_H

Generated by: LCOV version 1.13