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/data/set_comprehension.h 10 : /// \brief add your file description here. 11 : 12 : #ifndef MCRL2_DATA_SET_COMPREHENSION_H 13 : #define MCRL2_DATA_SET_COMPREHENSION_H 14 : 15 : #include "mcrl2/data/abstraction.h" 16 : 17 : namespace mcrl2 { 18 : 19 : namespace data { 20 : 21 : /// \brief universal quantification. 22 : /// 23 : class set_comprehension: public abstraction 24 : { 25 : public: 26 : 27 : /// Constructor. 28 : /// 29 : /// \param[in] d An aterm. 30 : /// \pre d has the interal structure of an abstraction. 31 : /// \pre d is a universal quantification. 32 31 : explicit set_comprehension(const aterm& d) 33 31 : : abstraction(d) 34 : { 35 31 : assert(is_abstraction(d)); 36 31 : assert(static_cast<abstraction>(d).binding_operator() == set_comprehension_binder()); 37 31 : } 38 : 39 : /// Constructor. 40 : /// 41 : /// \param[in] variables A nonempty list of binding variables (objects of type variable). 42 : /// \param[in] body The body of the set_comprehension abstraction. 43 : /// \pre variables is not empty. 44 : template < typename Container > 45 : set_comprehension(const Container& variables, 46 : const data_expression& body, 47 : typename atermpp::enable_if_container< Container, variable >::type* = nullptr) 48 : : abstraction(set_comprehension_binder(), variables, body) 49 : { 50 : assert(!variables.empty()); 51 : } 52 : 53 : /// Move semantics 54 : set_comprehension(const set_comprehension&) noexcept = default; 55 : set_comprehension(set_comprehension&&) noexcept = default; 56 : set_comprehension& operator=(const set_comprehension&) noexcept = default; 57 : set_comprehension& operator=(set_comprehension&&) noexcept = default; 58 : 59 : }; // class set_comprehension 60 : 61 : template <class... ARGUMENTS> 62 25 : void make_set_comprehension(atermpp::aterm& result, ARGUMENTS... arguments) 63 : { 64 25 : make_abstraction(result, set_comprehension_binder(), arguments...); 65 25 : } 66 : 67 : 68 : //--- start generated class set_comprehension ---// 69 : // prototype declaration 70 : std::string pp(const set_comprehension& x); 71 : 72 : /// \\brief Outputs the object to a stream 73 : /// \\param out An output stream 74 : /// \\param x Object x 75 : /// \\return The output stream 76 : inline 77 : std::ostream& operator<<(std::ostream& out, const set_comprehension& x) 78 : { 79 : return out << data::pp(x); 80 : } 81 : 82 : /// \\brief swap overload 83 : inline void swap(set_comprehension& t1, set_comprehension& t2) 84 : { 85 : t1.swap(t2); 86 : } 87 : //--- end generated class set_comprehension ---// 88 : 89 : } // namespace data 90 : 91 : } // namespace mcrl2 92 : 93 : #endif // MCRL2_DATA_SET_COMPREHENSION_H