mCRL2
Loading...
Searching...
No Matches
mutable_indexed_substitution.h
Go to the documentation of this file.
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//
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
27
28namespace mcrl2 {
29
30namespace data {
31
43template <typename VariableType = data::variable, typename ExpressionType = data_expression >
45{
46protected:
47 typedef atermpp::utilities::unordered_map < VariableType, ExpressionType > substitution_type;
48
57 mutable std::multiset<variable> m_variables_in_rhs;
58
59public:
60
62 typedef VariableType variable_type;
63
65 typedef ExpressionType expression_type;
66
69
73 {
74 }
75
77 const bool variables_in_rhs_set_is_defined,
78 const std::multiset<variable_type>& variables_in_rhs)
79 : m_substitution(substitution),
80 m_variables_in_rhs_set_is_defined(variables_in_rhs_set_is_defined),
81 m_variables_in_rhs(variables_in_rhs)
82 {
83 }
84
87 {
89 mutable_indexed_substitution < VariableType, ExpressionType >& m_super;
90
95 mutable_indexed_substitution < VariableType, ExpressionType >& super)
96 : m_variable(v),
97 m_super(super)
98 { }
99
102 {
103 assert(e.defined());
105 if (i!=m_super.m_substitution.end())
106 {
107 // Found.
108 assert(i->first==m_variable);
109 if (e==i->second) // No change in the substitution is required.
110 {
111 return;
112 }
114 {
115 std::set<variable_type> s=find_free_variables(i->second);
116 for(const variable& v: s)
117 {
118 // Remove one occurrence of v.
119 const typename std::multiset<variable_type>::const_iterator j=m_super.m_variables_in_rhs.find(v);
120 if (j!=m_super.m_variables_in_rhs.end())
121 {
123 }
124 }
125 }
126 if (e != m_variable)
127 {
128 i->second=e;
129 }
130 else
131 {
133 }
134 }
135 else
136 {
137 // Not found.
138 if (e!=m_variable)
139 {
141 }
142 }
143
145 {
146 std::set<variable_type> s1=find_free_variables(e);
147 m_super.m_variables_in_rhs.insert(s1.begin(),s1.end());
148 }
149 }
150 };
151
157 {
159 if (i==m_substitution.end()) // not found.
160 {
161 return v;
162 }
163 // no value assigned to v;
164 assert(i->first==v);
165 return i->second;
166 }
167
174 template <class ResultType>
175 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_core&>::value);
180 if (i==m_substitution.end()) // not found.
181 {
182 target=v;
183 return;
184 }
185 target=i->second;
186 }
187
194 void apply(const variable_type& v,
195 expression_type& target,
196 atermpp::detail::thread_aterm_pool& thread_aterm_pool)
197 {
199 if (i==m_substitution.end()) // not found.
200 {
201 target.assign(v, thread_aterm_pool);
202 return;
203 }
204 target.assign(i->second, thread_aterm_pool);
205 }
206
209 {
210 return assignment(v, *this);
211 }
212
214 void clear()
215 {
218 m_variables_in_rhs.clear();
219 }
220
227 {
230 }
231
233 template <typename Substitution>
234 bool operator==(const Substitution&) const
235 {
236 return false;
237 }
238
241 const std::multiset<variable_type>& variables_occurring_in_right_hand_sides() const
242 {
244 {
245 for(const auto& p: m_substitution)
246 {
247 std::set<variable_type> s=find_free_variables(p.second);
248 m_variables_in_rhs.insert(s.begin(),s.end());
249 }
251 }
252 return m_variables_in_rhs;
253 }
254
258 {
259 const std::multiset<variable>& variables_in_rhs=variables_occurring_in_right_hand_sides();
260 return variables_in_rhs.find(v)!=variables_in_rhs.end();
261 }
262
264 bool size()
265 {
266 return m_substitution.size();
267 }
268
270 bool empty()
271 {
272 return m_substitution.empty();
273 }
274
275public:
277 std::string to_string() const
278 {
279 std::stringstream result;
280 bool first = true;
281 result << "[";
282 for (const auto& p: m_substitution)
283 {
284 if (first)
285 {
286 first = false;
287 }
288 else
289 {
290 result << "; ";
291 }
292
293 result << p.first << " := " << p.second;
294 }
295 result << "]";
296 return result.str();
297 }
298
299};
300
301
302template <typename VariableType, typename ExpressionType>
304{
305 return out << sigma.to_string();
306}
307
308template <typename VariableType = variable, typename ExpressionType = data_expression>
310{
311 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
This file contains an implementation of the hash function to break circular header dependencies.
This is a thread's specific access to the global aterm pool which ensures that garbage collection and...
iterator find(const Args &... args)
Standard find function in a map.
std::pair< iterator, bool > emplace(Args &&... args)
const expression_type & operator()(const variable_type &v) const
Application operator; applies substitution to v.
ExpressionType expression_type
Type of expressions.
atermpp::utilities::unordered_map< VariableType, ExpressionType > substitution_type
mutable_indexed_substitution< VariableType, ExpressionType > clone()
Create a clone of the rewriter in which the underlying rewriter is copied, and not passed as a shared...
void apply(const variable_type &v, expression_type &target, atermpp::detail::thread_aterm_pool &thread_aterm_pool)
Application operator; applies substitution to v.
bool size()
Returns the number of assigned variables in the substitution.
bool operator==(const Substitution &) const
Compare substitutions.
void apply(const variable_type &v, ResultType &target)
Application operator; applies substitution to v.
const std::multiset< variable_type > & variables_occurring_in_right_hand_sides() const
Provides a multiset containing the variables in the rhs.
bool empty()
Returns true if the substitution is empty.
assignment operator[](variable_type const &v)
Index operator.
substitution_type m_substitution
Internal storage for substitutions. Required to be a container with random access through [] operator...
std::string to_string() const
string representation of the substitution. N.B. This is an expensive operation!
bool variable_occurs_in_a_rhs(const variable &v)
Checks whether a variable v occurs in one of the rhs's of the current substitution.
mutable_indexed_substitution(const substitution_type &substitution, const bool variables_in_rhs_set_is_defined, const std::multiset< variable_type > &variables_in_rhs)
\brief A data variable
Definition variable.h:28
The class data_expression.
static RewriterCompilingJitty::substitution_type & sigma(RewriterCompilingJitty *this_rewriter)
std::set< data::variable > substitution_variables(const Substitution &)
Returns the variables appearing in the right hand sides of the substitution.
Definition replace.h:161
std::set< data::variable > find_free_variables(const data::data_expression &x)
Definition data.cpp:99
std::ostream & operator<<(std::ostream &out, const abstraction &x)
Definition abstraction.h:94
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
Wrapper class for internal storage and substitution updates using operator()
mutable_indexed_substitution< VariableType, ExpressionType > & m_super
assignment(const variable_type &v, mutable_indexed_substitution< VariableType, ExpressionType > &super)
Constructor.
void operator=(const expression_type &e)
Actual assignment.