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/atermpp/aterm_appl.h
10 : /// \brief The term_appl class represents function application.
11 :
12 : #ifndef MCRL2_ATERMPP_ATERM_APPL_H
13 : #define MCRL2_ATERMPP_ATERM_APPL_H
14 :
15 : #include "mcrl2/atermpp/detail/aterm_appl_iterator.h"
16 : #include "mcrl2/atermpp/detail/aterm_list.h"
17 : #include "mcrl2/atermpp/detail/global_aterm_pool.h"
18 : #include "mcrl2/utilities/type_traits.h"
19 :
20 : namespace atermpp
21 : {
22 :
23 : template <class Term>
24 : class term_appl: public aterm
25 : {
26 : protected:
27 : /// \brief Constructor.
28 : /// \param t A pointer internal data structure from which the term is constructed.
29 : /// \details This function is explicitly protected such that is not used in common code.
30 : explicit term_appl(detail::_term_appl *t)
31 : : aterm(reinterpret_cast<detail::_aterm*>(t))
32 : {
33 : static_assert(std::is_base_of<aterm, Term>::value,"Term must be derived from an aterm");
34 : static_assert(sizeof(Term)==sizeof(std::size_t),"Term derived from an aterm must not have extra fields");
35 : }
36 :
37 : public:
38 : /// The type of object, T stored in the term_appl.
39 : typedef Term value_type;
40 :
41 : /// Pointer to T.
42 : typedef Term* pointer;
43 :
44 : /// Reference to T.
45 : typedef Term& reference;
46 :
47 : /// Const reference to T.
48 : typedef const Term const_reference;
49 :
50 : /// An unsigned integral type.
51 : typedef std::size_t size_type;
52 :
53 : /// A signed integral type.
54 : typedef ptrdiff_t difference_type;
55 :
56 : /// Iterator used to iterate through an term_appl.
57 : typedef term_appl_iterator<Term> iterator;
58 :
59 : /// Const iterator used to iterate through an term_appl.
60 : typedef term_appl_iterator<Term> const_iterator;
61 :
62 : /// \brief Default constructor.
63 988717 : term_appl():aterm()
64 988717 : {}
65 :
66 : /// \brief Explicit constructor from an aterm.
67 : /// \param t The aterm from which the term is constructed.
68 10029731636 : explicit term_appl(const aterm& t)
69 10029731636 : : aterm(t)
70 : {
71 10029731636 : assert(type_is_appl());
72 : static_assert(std::is_base_of<aterm, Term>::value,"Term must be derived from an aterm");
73 : static_assert(sizeof(Term)==sizeof(std::size_t),"Term derived from an aterm must not have extra fields");
74 10029731636 : }
75 :
76 : /// This class has user-declared copy constructor so declare default copy and move operators.
77 203149628 : term_appl(const term_appl& other) noexcept = default;
78 9801948 : term_appl& operator=(const term_appl& other) noexcept = default;
79 116170187 : term_appl(term_appl&& other) noexcept = default;
80 44718078 : term_appl& operator=(term_appl&& other) noexcept = default;
81 :
82 : /// \brief Constructor that provides an aterm_appl based on a function symbol and forward iterator providing the arguments.
83 : /// \details The iterator range is traversed more than once. If only one traversal is required
84 : /// use term_appl with a TermConverter argument. But this function
85 : /// is substantially less efficient.
86 : /// The length of the iterator range must match the arity of the function symbol.
87 : /// \param sym A function symbol.
88 : /// \param begin The start of a range of elements.
89 : /// \param end The end of a range of elements.
90 : template <class ForwardIterator,
91 : typename std::enable_if<mcrl2::utilities::is_iterator<ForwardIterator>::value>::type* = nullptr,
92 : typename std::enable_if<!std::is_same<typename ForwardIterator::iterator_category, std::input_iterator_tag>::value>::type* = nullptr,
93 : typename std::enable_if<!std::is_same<typename ForwardIterator::iterator_category, std::output_iterator_tag>::value>::type* = nullptr>
94 336509 : term_appl(const function_symbol& sym,
95 : ForwardIterator begin,
96 : ForwardIterator end)
97 336509 : {
98 336509 : detail::g_thread_term_pool().create_appl_dynamic(*this, sym, begin, end);
99 : static_assert((std::is_base_of<aterm, Term>::value),"Term must be derived from an aterm");
100 : static_assert(sizeof(Term)==sizeof(std::size_t),"Term derived from an aterm must not have extra fields");
101 : static_assert(!std::is_same<typename ForwardIterator::iterator_category, std::input_iterator_tag>::value,
102 : "A forward iterator has more requirements than an input iterator.");
103 : static_assert(!std::is_same<typename ForwardIterator::iterator_category, std::output_iterator_tag>::value,
104 : "A forward iterator has more requirements than an output iterator.");
105 336509 : }
106 :
107 : /// \brief Constructor that provides an aterm_appl based on a function symbol and an input iterator providing the arguments.
108 : /// \details The given iterator is traversed only once. So it can be used with an input iterator.
109 : /// This means that the TermConverter is applied exactly once to each element.
110 : /// The length of the iterator range must be equal to the arity of the function symbol.
111 : /// \param sym A function symbol.
112 : /// \param begin The start of a range of elements.
113 : /// \param end The end of a range of elements.
114 : template <class InputIterator,
115 : typename std::enable_if<mcrl2::utilities::is_iterator<InputIterator>::value>::type* = nullptr,
116 : typename std::enable_if<std::is_same<typename InputIterator::iterator_category, std::input_iterator_tag>::value>::type* = nullptr>
117 : term_appl(const function_symbol& sym,
118 : InputIterator begin,
119 : InputIterator end)
120 : : term_appl(sym, begin, end, [](const Term& term) -> const Term& { return term; } )
121 : {
122 : static_assert((std::is_base_of<aterm, Term>::value),"Term must be derived from an aterm");
123 : static_assert(sizeof(Term)==sizeof(std::size_t),"Term derived from an aterm must not have extra fields");
124 : static_assert(std::is_same<typename InputIterator::iterator_category, std::input_iterator_tag>::value,
125 : "The InputIterator is missing the input iterator tag.");
126 : }
127 :
128 : /// \details The given iterator is traversed only once. So it can be used with an input iterator.
129 : /// This means that the TermConverter is applied exactly once to each element.
130 : /// The length of the iterator range must be equal to the arity of the function symbol.
131 : /// \param sym A function symbol.
132 : /// \param begin The start of a range of elements.
133 : /// \param end The end of a range of elements.
134 : /// \param converter An class or lambda term containing an operator Term operator()(const Term& t) which is
135 : /// applied to each each element in the iterator range before it becomes an argument of this term.
136 : template <class InputIterator,
137 : class TermConverter,
138 : typename std::enable_if<mcrl2::utilities::is_iterator<InputIterator>::value>::type* = nullptr>
139 792454 : term_appl(const function_symbol& sym,
140 : InputIterator begin,
141 : InputIterator end,
142 : TermConverter converter)
143 792454 : {
144 792454 : detail::g_thread_term_pool().create_appl_dynamic(*this, sym, converter, begin, end);
145 : static_assert(std::is_base_of<aterm, Term>::value,"Term must be derived from an aterm");
146 : static_assert(sizeof(Term)==sizeof(std::size_t),"Term derived from an aterm must not have extra fields");
147 : static_assert(!std::is_same<typename InputIterator::iterator_category, std::output_iterator_tag>::value,
148 : "The InputIterator has the output iterator tag.");
149 792454 : }
150 :
151 : /// \brief Constructor.
152 : /// \param sym A function symbol.
153 894361 : term_appl(const function_symbol& sym)
154 894361 : {
155 894361 : detail::g_thread_term_pool().create_term(*this, sym);
156 : static_assert(std::is_base_of<aterm, Term>::value,"Term must be derived from an aterm");
157 : static_assert(sizeof(Term)==sizeof(std::size_t),"Term derived from an aterm must not have extra fields");
158 894361 : }
159 :
160 : /// \brief Constructor for n-arity function application.
161 : /// \param symbol A function symbol.
162 : /// \param arguments The arguments of the function application.
163 : template<typename ...Terms>
164 32213543 : term_appl(const function_symbol& symbol, const Terms& ...arguments)
165 32213543 : {
166 32213543 : detail::g_thread_term_pool().create_appl<Term>(*this, symbol, arguments...);
167 : static_assert(detail::are_terms<Terms...>::value, "Arguments of function application should be terms.");
168 : static_assert(std::is_base_of<aterm, Term>::value,"Term must be derived from an aterm");
169 : static_assert(sizeof(Term)==sizeof(std::size_t),"Term derived from an aterm must not have extra fields");
170 32213543 : }
171 :
172 : /// \brief Returns the function symbol belonging to an aterm_appl.
173 : /// \return The function symbol of this term.
174 7503377051 : const function_symbol& function() const
175 : {
176 7503377051 : return m_term->function();
177 : }
178 :
179 : /// \brief Returns the number of arguments of this term.
180 : /// \return The number of arguments of this term.
181 12678165161 : size_type size() const
182 : {
183 12678165161 : return m_term->function().arity();
184 : }
185 :
186 : /// \brief Returns true if the term has no arguments.
187 : /// \return True if this term has no arguments.
188 9971 : bool empty() const
189 : {
190 9971 : return size()==0;
191 : }
192 :
193 : /// \brief Returns an iterator pointing to the first argument.
194 : /// \return An iterator pointing to the first argument.
195 285789042 : const_iterator begin() const
196 : {
197 285789042 : return const_iterator(reinterpret_cast<const Term*>(&(reinterpret_cast<const detail::_term_appl*>(m_term)->arg(0))));
198 : }
199 :
200 : /// \brief Returns a const_iterator pointing past the last argument.
201 : /// \return A const_iterator pointing past the last argument.
202 285815840 : const_iterator end() const
203 : {
204 285815840 : return const_iterator(reinterpret_cast<const Term*>(&reinterpret_cast<const detail::_term_appl*>(m_term)->arg(size())));
205 : }
206 :
207 : /// \brief Returns the largest possible number of arguments.
208 : /// \return The largest possible number of arguments.
209 : constexpr size_type max_size() const
210 : {
211 : return std::numeric_limits<size_type>::max();
212 : }
213 :
214 : /// \brief Returns the i-th argument.
215 : /// \param i A positive integer.
216 : /// \return The argument with the given index.
217 5827225130 : const Term& operator[](const size_type i) const
218 : {
219 5827225130 : assert(i < size()); // Check the bounds.
220 5827225130 : return reinterpret_cast<const detail::_term_appl*>(m_term)->arg(i);
221 : }
222 : };
223 :
224 :
225 : /// \brief Constructor an aterm_appl in a variable based on a function symbol and an forward iterator providing the arguments.
226 : /// \details The iterator range is traversed more than once. If only one traversal is required
227 : /// use term_appl with a TermConverter argument. But this function
228 : /// is substantially less efficient.
229 : /// The length of the iterator range must match the arity of the function symbol.
230 : /// \param target The variable in which the result will be put. This variable may be used for scratch purposes.
231 : /// \param sym A function symbol.
232 : /// \param begin The start of a range of elements.
233 : /// \param end The end of a range of elements.
234 : template <class Term,
235 : class ForwardIterator,
236 : typename std::enable_if<mcrl2::utilities::is_iterator<ForwardIterator>::value>::type* = nullptr,
237 : typename std::enable_if<!std::is_same<typename ForwardIterator::iterator_category, std::input_iterator_tag>::value>::type* = nullptr,
238 : typename std::enable_if<!std::is_same<typename ForwardIterator::iterator_category, std::output_iterator_tag>::value>::type* = nullptr>
239 775668 : void make_term_appl(Term& target,
240 : const function_symbol& sym,
241 : ForwardIterator begin,
242 : ForwardIterator end)
243 : {
244 775668 : detail::g_thread_term_pool().create_appl_dynamic(target, sym, begin, end);
245 :
246 : static_assert((std::is_base_of<aterm, Term>::value),"Term must be derived from an aterm");
247 : static_assert(sizeof(Term)==sizeof(std::size_t),"Term derived from an aterm must not have extra fields");
248 : static_assert(!std::is_same<typename ForwardIterator::iterator_category, std::input_iterator_tag>::value,
249 : "A forward iterator has more requirements than an input iterator.");
250 : static_assert(!std::is_same<typename ForwardIterator::iterator_category, std::output_iterator_tag>::value,
251 : "A forward iterator has more requirements than an output iterator.");
252 775668 : }
253 :
254 :
255 : /// \brief Constructor an aterm_appl in a variable based on a function symbol and an input iterator providing the arguments.
256 : /// \details The given iterator is traversed only once. So it can be used with an input iterator.
257 : /// This means that the TermConverter is applied exactly once to each element.
258 : /// The length of the iterator range must be equal to the arity of the function symbol.
259 : /// \param target The variable in which the result will be put. This variable may be used for scratch purposes.
260 : /// \param sym A function symbol.
261 : /// \param begin The start of a range of elements.
262 : /// \param end The end of a range of elements.
263 : template <class Term,
264 : class InputIterator,
265 : typename std::enable_if<mcrl2::utilities::is_iterator<InputIterator>::value>::type* = nullptr,
266 : typename std::enable_if<std::is_same<typename InputIterator::iterator_category, std::input_iterator_tag>::value>::type* = nullptr>
267 : void make_term_appl(Term& target,
268 : const function_symbol& sym,
269 : InputIterator begin,
270 : InputIterator end)
271 : {
272 : make_term_appl(target, sym, begin, end, [](const Term& term) -> const Term& { return term; } );
273 :
274 : static_assert((std::is_base_of<aterm, Term>::value),"Term must be derived from an aterm");
275 : static_assert(sizeof(Term)==sizeof(std::size_t),"Term derived from an aterm must not have extra fields");
276 : static_assert(std::is_same<typename InputIterator::iterator_category, std::input_iterator_tag>::value,
277 : "The InputIterator is missing the input iterator tag.");
278 : }
279 :
280 : /// \brief Constructor an aterm_appl in a variable based on a function symbol and an forward iterator providing the arguments.
281 : /// \details The given iterator is traversed only once. So it can be used with an input iterator.
282 : /// This means that the TermConverter is applied exactly once to each element.
283 : /// The length of the iterator range must be equal to the arity of the function symbol.
284 : /// \param target The variable in which the result will be put. This variable may be used for scratch purposes.
285 : /// \param sym A function symbol.
286 : /// \param begin The start of a range of elements.
287 : /// \param end The end of a range of elements.
288 : /// \param converter An class or lambda term containing an operator Term operator()(const Term& t) which is
289 : /// applied to each each element in the iterator range before it becomes an argument of this term.
290 : template <class Term,
291 : class InputIterator,
292 : class TermConverter,
293 : typename std::enable_if<mcrl2::utilities::is_iterator<InputIterator>::value>::type* = nullptr>
294 9469023 : void make_term_appl(Term& target,
295 : const function_symbol& sym,
296 : InputIterator begin,
297 : InputIterator end,
298 : TermConverter converter)
299 : {
300 9469023 : detail::g_thread_term_pool().create_appl_dynamic(target, sym, converter, begin, end);
301 :
302 : static_assert(std::is_base_of<aterm, Term>::value,"Term must be derived from an aterm");
303 : static_assert(sizeof(Term)==sizeof(std::size_t),"Term derived from an aterm must not have extra fields");
304 : static_assert(!std::is_same<typename InputIterator::iterator_category, std::output_iterator_tag>::value,
305 : "The InputIterator has the output iterator tag.");
306 9469023 : }
307 :
308 : /// \brief Make an term_appl consisting of a single function symbol.
309 : /// \param target The variable in which the result will be put. This variable may be used for scratch purposes.
310 : /// \param sym A function symbol.
311 : template <class Term>
312 : void make_term_appl(Term& target,
313 : const function_symbol& sym)
314 : {
315 : detail::g_thread_term_pool().create_term(target, sym);
316 :
317 : static_assert(std::is_base_of<aterm, Term>::value,"Term must be derived from an aterm");
318 : static_assert(sizeof(Term)==sizeof(std::size_t),"Term derived from an aterm must not have extra fields");
319 : }
320 :
321 : /// \brief Make an aterm application for n-arity function application.
322 : /// \param target The variable in which the result will be put. This variable may be used for scratch purposes.
323 : /// \param symbol A function symbol.
324 : /// \param arguments The arguments of the function application.
325 : template<class Term,
326 : typename ...Terms>
327 27824178 : void make_term_appl(Term& target, const function_symbol& symbol, const Terms& ...arguments)
328 : {
329 27824178 : detail::g_thread_term_pool().create_appl(target, symbol, arguments...);
330 :
331 : // TODO: enable the static_assert below. Doesn't seem to work properly now.
332 : // static_assert(detail::are_terms_or_functions<Terms...>::value, "Arguments of function application should be terms.");
333 : static_assert(std::is_base_of<aterm, Term>::value,"Term must be derived from an aterm");
334 : static_assert(sizeof(Term)==sizeof(std::size_t),"Term derived from an aterm must not have extra fields");
335 27824176 : }
336 :
337 : /// \brief Constructor for n-arity function application with an index.
338 : /// \param target The variable in which the result will be put. This variable may be used for scratch purposes.
339 : /// \param symbol A function symbol.
340 : /// \param arguments The arguments of the function application.
341 : template<class Term,
342 : class INDEX_TYPE,
343 : typename ...Terms>
344 19721037 : void make_term_appl_with_index(aterm& target, const function_symbol& symbol, const Terms& ...arguments)
345 : {
346 19721037 : detail::g_thread_term_pool().create_appl_index<Term, INDEX_TYPE>(target, symbol, arguments...);
347 : // TODO: enable the static_assert below. Doesn't seem to work properly now.
348 : // static_assert(detail::are_terms_or_functions<Terms...>::value, "Arguments of function application should be terms.");
349 : static_assert(std::is_base_of<aterm, Term>::value,"Term must be derived from an aterm");
350 : static_assert(sizeof(Term)==sizeof(std::size_t),"Term derived from an aterm must not have extra fields");
351 19721037 : }
352 :
353 : typedef term_appl<aterm> aterm_appl;
354 :
355 : } // namespace atermpp
356 :
357 : namespace std
358 : {
359 :
360 : /// \brief Swaps two term_applss.
361 : /// \details This operation is more efficient than exchanging terms by an assignment,
362 : /// as swapping does not require to change the protection of terms.
363 : /// \param t1 The first term.
364 : /// \param t2 The second term.
365 : template <class T>
366 : inline void swap(atermpp::term_appl<T>& t1, atermpp::term_appl<T>& t2) noexcept
367 : {
368 : t1.swap(t2);
369 : }
370 :
371 : /// \brief Standard hash function.
372 : template<class T>
373 : struct hash<atermpp::term_appl<T> >
374 : {
375 10 : std::size_t operator()(const atermpp::term_appl<T>& t) const
376 : {
377 10 : return std::hash<atermpp::aterm>()(t);
378 : }
379 : };
380 : } // namespace std
381 :
382 : #endif // MCRL2_ATERMPP_ATERM_APPL_H
|
