Line data Source code
1 : // Author(s): Jeroen Keiren
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/data/substitutions/mutable_indexed_substitution.h
10 : /// \brief add your file description here.
11 :
12 : // The code below contains an experiment to replace the classical mutable_indexed_substitution
13 : // by a std::unordered_map from variables to expressions. This is up to 1.5 times
14 : // slower in most state space generations when there are not too many variables, which is
15 : // typical for state space generation without complex sum operations or quantifiers.
16 : // When a large number of variables exist, generally generated as fresh variables,
17 : // std::unordered_map can perform much better, leading to the time to generate a
18 : // state space with a factor 2.
19 :
20 :
21 : #ifndef MCRL2_DATA_SUBSTITUTIONS_MUTABLE_INDEXED_SUBSTITUTION_H
22 : #define MCRL2_DATA_SUBSTITUTIONS_MUTABLE_INDEXED_SUBSTITUTION_H
23 :
24 : #include "mcrl2/atermpp/standard_containers/unordered_map.h"
25 : #include "mcrl2/atermpp/standard_containers/detail/unordered_map_implementation.h"
26 : #include "mcrl2/data/data_expression.h"
27 :
28 : namespace mcrl2 {
29 :
30 : namespace data {
31 :
32 : /// \brief Generic substitution function.
33 : /// \details This substitution assumes a function variable -> std::size_t, that, for
34 : /// each variable gives a unique index. The substitutions are stored
35 : /// internally as a vector, mapping std::size_t to expression.
36 : /// Provided that, given a variable, its index can be computed in O(1)
37 : /// time, insertion is O(1) amortized, and lookup is O(1).
38 : /// Memory required is O(n) where n is the largest index used.
39 : /// This substitution can maintain the variables occurring in the rhs of
40 : /// expressions. If it is requested that whether a variable occurs in a rhs,
41 : /// the substitution automatically maintains these variables. This requires
42 : /// time O(n log n) per rhs, where n is the size of the rhs.
43 : template <typename VariableType = data::variable, typename ExpressionType = data_expression >
44 : class mutable_indexed_substitution
45 : {
46 : protected:
47 : typedef atermpp::utilities::unordered_map < VariableType, ExpressionType > substitution_type;
48 :
49 : /// \brief Internal storage for substitutions.
50 : /// Required to be a container with random access through [] operator.
51 : /// It is essential to store the variable also in the container, as it might be that
52 : /// this variable is not used anywhere although it has a valid assignment. This happens
53 : /// for instance when the assignment is already parsed, while the expression to which it
54 : /// needs to be applied must still be parsed.
55 : substitution_type m_substitution;
56 : mutable bool m_variables_in_rhs_set_is_defined;
57 : mutable std::multiset<variable> m_variables_in_rhs;
58 :
59 : public:
60 :
61 : /// \brief Type of variables
62 : typedef VariableType variable_type;
63 :
64 : /// \brief Type of expressions
65 : typedef ExpressionType expression_type;
66 :
67 : using argument_type = variable_type;
68 : using result_type = expression_type;
69 :
70 : /// \brief Default constructor
71 20912 : mutable_indexed_substitution()
72 20912 : : m_variables_in_rhs_set_is_defined(false)
73 : {
74 20912 : }
75 :
76 0 : mutable_indexed_substitution(const substitution_type& substitution,
77 : const bool variables_in_rhs_set_is_defined,
78 : const std::multiset<variable_type>& variables_in_rhs)
79 0 : : m_substitution(substitution),
80 0 : m_variables_in_rhs_set_is_defined(variables_in_rhs_set_is_defined),
81 0 : m_variables_in_rhs(variables_in_rhs)
82 : {
83 0 : }
84 :
85 : /// \brief Wrapper class for internal storage and substitution updates using operator()
86 : struct assignment
87 : {
88 : const variable_type& m_variable;
89 : mutable_indexed_substitution < VariableType, ExpressionType >& m_super;
90 :
91 : /// \brief Constructor.
92 : /// \param[in] v a variable.
93 : /// \param[in] super A reference to the surrounding indexed substitution.
94 220952 : assignment(const variable_type& v,
95 : mutable_indexed_substitution < VariableType, ExpressionType >& super)
96 220952 : : m_variable(v),
97 220952 : m_super(super)
98 220952 : { }
99 :
100 : /// \brief Actual assignment
101 220952 : void operator=(const expression_type& e)
102 : {
103 220952 : assert(e.defined());
104 220952 : const typename substitution_type::iterator i = m_super.m_substitution.find(m_variable);
105 220952 : if (i!=m_super.m_substitution.end())
106 : {
107 : // Found.
108 104034 : assert(i->first==m_variable);
109 104034 : if (e==i->second) // No change in the substitution is required.
110 : {
111 10167 : return;
112 : }
113 93867 : if (m_super.m_variables_in_rhs_set_is_defined)
114 : {
115 1568 : std::set<variable_type> s=find_free_variables(i->second);
116 1568 : for(const variable& v: s)
117 : {
118 : // Remove one occurrence of v.
119 0 : const typename std::multiset<variable_type>::const_iterator j=m_super.m_variables_in_rhs.find(v);
120 0 : if (j!=m_super.m_variables_in_rhs.end())
121 : {
122 0 : m_super.m_variables_in_rhs.erase(j);
123 : }
124 : }
125 1568 : }
126 93867 : if (e != m_variable)
127 : {
128 7544 : i->second=e;
129 : }
130 : else
131 : {
132 86323 : m_super.m_substitution.erase(i);
133 : }
134 : }
135 : else
136 : {
137 : // Not found.
138 116918 : if (e!=m_variable)
139 : {
140 99616 : m_super.m_substitution.emplace(m_variable,e);
141 : }
142 : }
143 :
144 210785 : if (e != m_variable && m_super.m_variables_in_rhs_set_is_defined)
145 : {
146 1567 : std::set<variable_type> s1=find_free_variables(e);
147 1567 : m_super.m_variables_in_rhs.insert(s1.begin(),s1.end());
148 1567 : }
149 : }
150 : };
151 :
152 : /// \brief Application operator; applies substitution to v.
153 : /// \param v The variable to which the subsitution is applied.
154 : /// \result The value to which v is mapped, or v itself if v is not
155 : /// mapped to a value.
156 25208 : const expression_type& operator()(const variable_type& v) const
157 : {
158 25208 : typename substitution_type::const_iterator i=m_substitution.find(v);
159 25208 : if (i==m_substitution.end()) // not found.
160 : {
161 22154 : return v;
162 : }
163 : // no value assigned to v;
164 3054 : assert(i->first==v);
165 3054 : return i->second;
166 : }
167 :
168 : /// \brief Application operator; applies substitution to v.
169 : /// \details This must deliver an expression, and not a reference
170 : /// to an expression, as the expressions are stored in
171 : /// a vector that can be resized and moved.
172 : /// \param v The variable to which the subsitution is applied.
173 : /// \param target The target into which the substitution is stored.
174 : template <class ResultType>
175 0 : void apply(const variable_type& v, ResultType& target)
176 : {
177 : static_assert(std::is_same<ResultType&,expression_type&>::value ||
178 : std::is_same<ResultType&,atermpp::unprotected_aterm&>::value);
179 0 : const typename substitution_type::const_iterator i=m_substitution.find(v);
180 0 : if (i==m_substitution.end()) // not found.
181 : {
182 0 : target=v;
183 0 : return;
184 : }
185 0 : target=i->second;
186 : }
187 :
188 : /// \brief Application operator; applies substitution to v.
189 : /// \details This must deliver an expression, and not a reference
190 : /// to an expression, as the expressions are stored in
191 : /// a vector that can be resized and moved.
192 : /// \param v The variable to which the subsitution is applied.
193 : /// \param target The target into which the substitution is stored.
194 488555 : void apply(const variable_type& v,
195 : expression_type& target,
196 : atermpp::detail::thread_aterm_pool& thread_aterm_pool)
197 : {
198 488555 : const typename substitution_type::iterator i=m_substitution.find(v);
199 488555 : if (i==m_substitution.end()) // not found.
200 : {
201 296634 : target.assign(v, thread_aterm_pool);
202 296634 : return;
203 : }
204 191921 : target.assign(i->second, thread_aterm_pool);
205 : }
206 :
207 : /// \brief Index operator.
208 220952 : assignment operator[](variable_type const& v)
209 : {
210 220952 : return assignment(v, *this);
211 : }
212 :
213 : /// \brief Clear substitutions.
214 : void clear()
215 : {
216 : m_substitution.clear();
217 : m_variables_in_rhs_set_is_defined=false;
218 : m_variables_in_rhs.clear();
219 : }
220 :
221 : /// \brief Create a clone of the rewriter in which the underlying rewriter is
222 : /// copied, and not passed as a shared pointer.
223 : /// \details This is useful when the rewriter is used in different parallel
224 : /// processes. One rewriter can only be used sequentially. \return A rewriter,
225 : /// with a copy of the underlying jitty, jittyc or jittyp rewriting engine.
226 0 : mutable_indexed_substitution<VariableType, ExpressionType> clone()
227 : {
228 : return mutable_indexed_substitution<VariableType, ExpressionType>(
229 0 : m_substitution, m_variables_in_rhs_set_is_defined, m_variables_in_rhs);
230 : }
231 :
232 : /// \brief Compare substitutions
233 : template <typename Substitution>
234 : bool operator==(const Substitution&) const
235 : {
236 : return false;
237 : }
238 :
239 : /// \brief Provides a multiset containing the variables in the rhs.
240 : /// \return A multiset with variables in the right hand side.
241 3588 : const std::multiset<variable_type>& variables_occurring_in_right_hand_sides() const
242 : {
243 3588 : if (!m_variables_in_rhs_set_is_defined)
244 : {
245 720 : for(const auto& p: m_substitution)
246 : {
247 198 : std::set<variable_type> s=find_free_variables(p.second);
248 198 : m_variables_in_rhs.insert(s.begin(),s.end());
249 : }
250 261 : m_variables_in_rhs_set_is_defined=true;
251 : }
252 3588 : return m_variables_in_rhs;
253 : }
254 :
255 : /// \brief Checks whether a variable v occurs in one of the rhs's of the current substitution.
256 : /// \return A boolean indicating whether v occurs in sigma(x) for some variable x.
257 3370 : bool variable_occurs_in_a_rhs(const variable& v)
258 : {
259 3370 : const std::multiset<variable>& variables_in_rhs=variables_occurring_in_right_hand_sides();
260 3370 : return variables_in_rhs.find(v)!=variables_in_rhs.end();
261 : }
262 :
263 : /// \brief Returns the number of assigned variables in the substitution.
264 : bool size()
265 : {
266 : return m_substitution.size();
267 : }
268 :
269 : /// \brief Returns true if the substitution is empty.
270 88648 : bool empty()
271 : {
272 88648 : return m_substitution.empty();
273 : }
274 :
275 : public:
276 : /// \brief string representation of the substitution. N.B. This is an expensive operation!
277 1 : std::string to_string() const
278 : {
279 1 : std::stringstream result;
280 1 : bool first = true;
281 1 : result << "[";
282 3 : for (const auto& p: m_substitution)
283 : {
284 1 : if (first)
285 : {
286 1 : first = false;
287 : }
288 : else
289 : {
290 0 : result << "; ";
291 : }
292 :
293 1 : result << p.first << " := " << p.second;
294 : }
295 1 : result << "]";
296 2 : return result.str();
297 1 : }
298 :
299 : };
300 :
301 :
302 : template <typename VariableType, typename ExpressionType>
303 0 : std::ostream& operator<<(std::ostream& out, const mutable_indexed_substitution<VariableType, ExpressionType>& sigma)
304 : {
305 0 : return out << sigma.to_string();
306 : }
307 :
308 : template <typename VariableType = variable, typename ExpressionType = data_expression>
309 218 : std::multiset<variable> substitution_variables(const mutable_indexed_substitution<VariableType, ExpressionType>& sigma)
310 : {
311 218 : return sigma.variables_occurring_in_right_hand_sides();
312 : }
313 :
314 : } // namespace data
315 :
316 : } // namespace mcrl2
317 :
318 : #endif // MCRL2_DATA_SUBSTITUTIONS_MUTABLE_INDEXED_SUBSTITUTION_H
|
