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/substitutions.h 10 : /// \brief add your file description here. 11 : 12 : #ifndef MCRL2_PBES_SUBSTITUTIONS_H 13 : #define MCRL2_PBES_SUBSTITUTIONS_H 14 : 15 : #include "mcrl2/data/substitutions/mutable_map_substitution.h" 16 : #include "mcrl2/pbes/replace.h" 17 : 18 : namespace mcrl2 { 19 : 20 : namespace pbes_system { 21 : 22 : /** \brief Substitution function for propositional variables 23 : * 24 : * Model of Substitution. 25 : * 26 : **/ 27 : class propositional_variable_substitution 28 : { 29 : public: 30 : // maps X to (phi, d), where X(d) is the propositional variable corresponding to X 31 : typedef std::map<core::identifier_string, std::pair<pbes_expression, data::variable_list> > map_type; 32 : 33 : typedef map_type::iterator iterator; 34 : typedef map_type::const_iterator const_iterator; 35 : 36 : protected: 37 : map_type m_map; 38 : 39 : public: 40 : /// \brief type used to represent variables 41 : typedef propositional_variable_instantiation variable_type; 42 : 43 : /// \brief type used to represent expressions 44 : typedef pbes_expression expression_type; 45 : 46 : /// \brief Apply this substitution to a single variable expression. 47 : /// \param[in] v The variable for which to give the associated expression. 48 : /// \return expression equivalent to s(e), or a reference to such an expression. 49 121 : pbes_expression operator()(const variable_type& v) const 50 : { 51 121 : auto i = m_map.find(v.name()); 52 121 : if (i == m_map.end()) 53 : { 54 65 : return v; 55 : } 56 56 : pbes_expression phi = i->second.first; 57 56 : const data::variable_list& d = i->second.second; 58 56 : const data::data_expression_list& e = v.parameters(); 59 56 : data::mutable_map_substitution<> sigma; 60 56 : auto j = d.begin(); 61 56 : auto k = e.begin(); 62 178 : for (; j != d.end(); ++j, ++k) 63 : { 64 122 : sigma[*j] = *k; 65 : } 66 : 67 : // return phi[d := e] 68 56 : phi = pbes_system::replace_variables_capture_avoiding(phi, sigma); 69 56 : return phi; 70 56 : } 71 : 72 : /// \brief Wrapper class for internal storage and substitution updates using operator() 73 : class assignment 74 : { 75 : private: 76 : const propositional_variable& m_variable; 77 : map_type& m_map; 78 : 79 : public: 80 : 81 : /// \brief Constructor. 82 : /// 83 : /// \param[in] v a variable. 84 : /// \param[in] m a mapping of variables to expressions. 85 87 : assignment(const propositional_variable& v, map_type& m) : 86 87 : m_variable(v), m_map(m) 87 87 : { } 88 : 89 : /** \brief Assigns expression on the right-hand side 90 : * \param[in] e the expression to associate to the variable for the owning substitution object 91 : * \code 92 : * template< typename E, typename V > 93 : * void example(V const& v, E const& e) { 94 : * substitution< E, V > s; // substitution 95 : * 96 : * s[v] = e; 97 : * 98 : * assert(s(v) == e); 99 : * \endcode 100 : **/ 101 87 : void operator=(const pbes_expression& e) 102 : { 103 87 : m_map[m_variable.name()] = std::make_pair(e, m_variable.parameters()); 104 87 : } 105 : }; 106 : 107 : propositional_variable_substitution() = default; 108 : 109 : propositional_variable_substitution(const map_type& other) 110 : : m_map(other) 111 : { 112 : } 113 : 114 : /** \brief Update substitution for a single variable 115 : * 116 : * \param[in] v the variable for which to update the value 117 : * 118 : * \code 119 : * template< typename E, typename V > 120 : * void example(V const& v, E const& e) { 121 : * substitution< E, V > s; // substitution 122 : * 123 : * std::cout << s(x) << std::endl; // prints x 124 : * 125 : * s[v] = e; 126 : * 127 : * std::cout << s(x) << std::endl; // prints e 128 : * } 129 : * \endcode 130 : * 131 : * \return expression assignment for variable v, effect 132 : **/ 133 87 : assignment operator[](const propositional_variable& v) 134 : { 135 87 : return { v, this->m_map }; 136 : } 137 : 138 : /// \brief Constructor. Initializes the substitution with the assignment X := phi. 139 87 : propositional_variable_substitution(const propositional_variable& X, const pbes_expression& phi) 140 87 : { 141 87 : (*this)[X] = phi; 142 87 : } 143 : 144 : /// \brief Returns an iterator pointing to the beginning of the sequence of assignments 145 : const_iterator begin() const 146 : { 147 : return m_map.begin(); 148 : } 149 : 150 : /// \brief Returns an iterator pointing past the end of the sequence of assignments 151 : const_iterator end() const 152 : { 153 : return m_map.end(); 154 : } 155 : 156 : /// \brief Returns an iterator pointing to the beginning of the sequence of assignments 157 : iterator begin() 158 : { 159 : return this->m_map.begin(); 160 : } 161 : 162 : /// \brief Returns an iterator pointing past the end of the sequence of assignments 163 : iterator end() 164 : { 165 : return this->m_map.end(); 166 : } 167 : 168 : /// \brief Returns an iterator that references the expression associated with v or is equal to m_map.end() 169 : iterator find(const variable_type &v) 170 : { 171 : return this->m_map.find(static_cast<core::identifier_string>(v)); 172 : } 173 : 174 : /// \brief Removes the substitution to the propositional variable v. 175 : map_type::size_type erase(const propositional_variable& v) 176 : { 177 : return m_map.erase(static_cast<core::identifier_string>(v)); 178 : } 179 : 180 : /// \brief Returns an iterator that references the expression associated with v or is equal to m_map.end() 181 : const_iterator find(variable_type const& v) const 182 : { 183 : return m_map.find(static_cast<core::identifier_string>(v)); 184 : } 185 : 186 : /// \brief Returns true if the sequence of assignments is empty 187 : bool empty() const 188 : { 189 : return this->m_map.empty(); 190 : } 191 : }; 192 : 193 : } // namespace pbes_system 194 : 195 : } // namespace mcrl2 196 : 197 : #endif // MCRL2_PBES_SUBSTITUTIONS_H