LCOV - code coverage report
Current view: top level - modal_formula/include/mcrl2/modal_formula - resolve_name_clashes.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 24 117 20.5 %
Date: 2020-02-21 00:44:40 Functions: 8 28 28.6 %
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/detail/state_formula_name_clash_resolver.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_MODAL_FORMULA_RESOLVE_NAME_CLASHES_H
      13             : #define MCRL2_MODAL_FORMULA_RESOLVE_NAME_CLASHES_H
      14             : 
      15             : #include "mcrl2/modal_formula/builder.h"
      16             : #include "mcrl2/utilities/detail/container_utility.h"
      17             : 
      18             : namespace mcrl2::state_formulas {
      19             : 
      20             : namespace detail
      21             : {
      22             : 
      23             : template <typename Derived>
      24          12 : class state_variable_name_clash_resolver: public state_formulas::state_formula_builder<Derived>
      25             : {
      26             :   public:
      27             :     typedef state_formulas::state_formula_builder<Derived> super;
      28             : 
      29             :     using super::enter;
      30             :     using super::leave;
      31             :     using super::apply;
      32             : 
      33             :     typedef std::map<core::identifier_string, std::vector<core::identifier_string> > name_map;
      34             : 
      35             :     /// \brief The stack of names.
      36             :     name_map m_names;
      37             : 
      38             :     /// \brief Generator for fresh variable names.
      39             :     utilities::number_postfix_generator m_generator;
      40             : 
      41             :     /// \brief Pops the name of the stack
      42          12 :     void pop(const core::identifier_string& name)
      43             :     {
      44          12 :       m_names[name].pop_back();
      45          12 :     }
      46             : 
      47             :     /// \brief Pushes name on the stack.
      48          12 :     void push(const core::identifier_string& name)
      49             :     {
      50          12 :       std::vector<core::identifier_string>& names = m_names[name];
      51          12 :       if (names.empty())
      52             :       {
      53           6 :         names.push_back(name);
      54             :       }
      55             :       else
      56             :       {
      57           6 :         names.push_back(m_generator(std::string(name) + "_"));
      58             :       }
      59          12 :     }
      60             : 
      61          12 :     void enter(const mu& x)
      62             :     {
      63          12 :       push(x.name());
      64          12 :     }
      65             : 
      66          12 :     void leave(const mu& x)
      67             :     {
      68          12 :       pop(x.name());
      69          12 :     }
      70             : 
      71           0 :     void enter(const nu& x)
      72             :     {
      73           0 :       push(x.name());
      74           0 :     }
      75             : 
      76           0 :     void leave(const nu& x)
      77             :     {
      78           0 :       pop(x.name());
      79           0 :     }
      80             : 
      81             :     // Rename variable
      82          12 :     state_formula apply(const mu& x)
      83             :     {
      84          12 :       enter(x);
      85             :       // N.B. If the two lines below are replace by
      86             :       //   state_formula result = mu(m_names[x.name()].back(), x.assignments(), (*this)(x.operand()));
      87             :       // a memory error occurs with the clang and intel compilers!
      88          24 :       core::identifier_string name = m_names[x.name()].back();
      89          12 :       state_formula result = mu(name, x.assignments(), apply(x.operand()));
      90          12 :       leave(x);
      91          24 :       return result;
      92             :     }
      93             : 
      94             :     // Rename variable
      95           0 :     state_formula apply(const nu& x)
      96             :     {
      97           0 :       enter(x);
      98             :       // N.B. If the two lines below are replace by
      99             :       //   state_formula result = nu(m_names[x.name()].back(), x.assignments(), (*this)(x.operand()));
     100             :       // a memory error occurs with the clang and intel compilers!
     101           0 :       core::identifier_string name = m_names[x.name()].back();
     102           0 :       state_formula result = nu(name, x.assignments(), apply(x.operand()));
     103           0 :       leave(x);
     104           0 :       return result;
     105             :     }
     106             : 
     107             :     // Rename variable
     108             :     state_formula operator()(const variable& x)
     109             :     {
     110             :       return variable(m_names[x.name()].back(), x.arguments());
     111             :     }
     112             : };
     113             : 
     114           0 : class state_formula_data_variable_name_clash_resolver: public state_formulas::data_expression_builder<state_formula_data_variable_name_clash_resolver>
     115             : {
     116             :   public:
     117             :     typedef state_formulas::data_expression_builder<state_formula_data_variable_name_clash_resolver> super;
     118             : 
     119             :     using super::enter;
     120             :     using super::leave;
     121             :     using super::apply;
     122             : 
     123             :     data::set_identifier_generator& generator;
     124             :     std::multiset<data::variable> bound_variables;
     125             :     std::map<data::variable, std::vector<data::variable>> substitutions;
     126             : 
     127           0 :     explicit state_formula_data_variable_name_clash_resolver(data::set_identifier_generator& generator_)
     128           0 :      : generator(generator_)
     129           0 :     {}
     130             : 
     131           0 :     void insert(const data::variable& v)
     132             :     {
     133           0 :       if (utilities::detail::contains(bound_variables, v))
     134             :       {
     135           0 :         substitutions[v].push_back(data::variable(generator(v.name()), v.sort()));
     136             :       }
     137           0 :       bound_variables.insert(v);
     138           0 :     }
     139             : 
     140           0 :     void erase(const data::variable& v)
     141             :     {
     142           0 :       bound_variables.erase(v);
     143           0 :       auto i = substitutions.find(v);
     144           0 :       if (i != substitutions.end())
     145             :       {
     146           0 :         i->second.pop_back();
     147           0 :         if (i->second.empty())
     148             :         {
     149           0 :           substitutions.erase(i);
     150             :         }
     151             :       }
     152           0 :     }
     153             : 
     154           0 :     data::assignment_list apply_assignments(const data::assignment_list& x)
     155             :     {
     156           0 :       auto sigma = [&](const data::variable& v) -> data::data_expression
     157             :       {
     158           0 :         auto i = substitutions.find(v);
     159           0 :         if (i == substitutions.end())
     160             :         {
     161           0 :           return v;
     162             :         }
     163           0 :         return i->second.back();
     164           0 :       };
     165             : 
     166           0 :       return data::assignment_list(x.begin(), x.end(), [&](const data::assignment& a)
     167             :         {
     168           0 :           return data::assignment(atermpp::down_cast<data::variable>(sigma(a.lhs())), data::replace_free_variables(a.rhs(), sigma));
     169           0 :         }
     170           0 :       );
     171             :     }
     172             : 
     173           0 :     data::variable_list apply_variables(const data::variable_list& x)
     174             :     {
     175           0 :       auto sigma = [&](const data::variable& v) -> data::data_expression
     176             :       {
     177           0 :         auto i = substitutions.find(v);
     178           0 :         if (i == substitutions.end())
     179             :         {
     180           0 :           return v;
     181             :         }
     182           0 :         return i->second.back();
     183           0 :       };
     184             : 
     185           0 :       return data::variable_list(x.begin(), x.end(), [&](const data::variable& v)
     186             :                                    {
     187           0 :                                      return atermpp::down_cast<data::variable>(sigma(v));
     188           0 :                                    }
     189           0 :       );
     190             :     }
     191             : 
     192           0 :     state_formula apply(const mu& x)
     193             :     {
     194           0 :       for (const data::assignment& a: x.assignments())
     195             :       {
     196           0 :         insert(a.lhs());
     197             :       }
     198           0 :       state_formula result = mu(x.name(), apply_assignments(x.assignments()), apply(x.operand()));
     199           0 :       for (const data::assignment& a: x.assignments())
     200             :       {
     201           0 :         erase(a.lhs());
     202             :       }
     203           0 :       return result;
     204             :     }
     205             : 
     206           0 :     state_formula apply(const nu& x)
     207             :     {
     208           0 :       for (const data::assignment& a: x.assignments())
     209             :       {
     210           0 :         insert(a.lhs());
     211             :       }
     212           0 :       state_formula result = nu(x.name(), apply_assignments(x.assignments()), apply(x.operand()));
     213           0 :       for (const data::assignment& a: x.assignments())
     214             :       {
     215           0 :         erase(a.lhs());
     216             :       }
     217           0 :       return result;
     218             :     }
     219             : 
     220           0 :     state_formula apply(const forall& x)
     221             :     {
     222           0 :       for (const data::variable& v: x.variables())
     223             :       {
     224           0 :         insert(v);
     225             :       }
     226           0 :       state_formula result = forall(apply_variables(x.variables()), apply(x.body()));
     227           0 :       for (const data::variable& v: x.variables())
     228             :       {
     229           0 :         erase(v);
     230             :       }
     231           0 :       return result;
     232             :     }
     233             : 
     234           0 :     state_formula apply(const exists& x)
     235             :     {
     236           0 :       for (const data::variable& v: x.variables())
     237             :       {
     238           0 :         insert(v);
     239             :       }
     240           0 :       state_formula result = exists(apply_variables(x.variables()), apply(x.body()));
     241           0 :       for (const data::variable& v: x.variables())
     242             :       {
     243           0 :         erase(v);
     244             :       }
     245           0 :       return result;
     246             :     }
     247             : 
     248           0 :     data::data_expression apply(const data::data_expression& x)
     249             :     {
     250           0 :       auto sigma = [&](const data::variable& v) -> data::data_expression
     251             :       {
     252           0 :         auto i = substitutions.find(v);
     253           0 :         if (i == substitutions.end())
     254             :         {
     255           0 :           return v;
     256             :         }
     257           0 :         return i->second.back();
     258           0 :       };
     259             : 
     260           0 :       return data::replace_free_variables(x, sigma);
     261             :     }
     262             : };
     263             : 
     264             : } // namespace detail
     265             : 
     266             : /// \brief Resolves name clashes in state variables of formula x
     267             : inline
     268           6 : state_formula resolve_state_variable_name_clashes(const state_formula& x)
     269             : {
     270           6 :   return core::make_apply_builder<detail::state_variable_name_clash_resolver>().apply(x);
     271             : }
     272             : 
     273             : /// \brief Resolves name clashes in data variables of formula x
     274             : inline
     275           0 : state_formula resolve_state_formula_data_variable_name_clashes(const state_formula& x, const std::set<core::identifier_string>& context_ids = std::set<core::identifier_string>())
     276             : {
     277           0 :   data::set_identifier_generator generator;
     278           0 :   generator.add_identifiers(state_formulas::find_identifiers(x));
     279           0 :   generator.add_identifiers(context_ids);
     280           0 :   detail::state_formula_data_variable_name_clash_resolver f(generator);
     281           0 :   return f.apply(x);
     282             : }
     283             : 
     284             : } // namespace mcrl2::state_formulas
     285             : 
     286             : #endif // MCRL2_MODAL_FORMULA_RESOLVE_NAME_CLASHES_H

Generated by: LCOV version 1.13