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/bag_comprehension.h 10 : /// \brief add your file description here. 11 : 12 : #ifndef MCRL2_DATA_BAG_COMPREHENSION_H 13 : #define MCRL2_DATA_BAG_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 bag_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 16 : explicit bag_comprehension(const aterm& d) 33 16 : : abstraction(d) 34 : { 35 16 : assert(is_abstraction(d)); 36 16 : assert(static_cast<abstraction>(d).binding_operator() == bag_comprehension_binder()); 37 16 : } 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 bag_comprehension abstraction. 43 : /// \pre variables is not empty. 44 : template < typename Container > 45 : bag_comprehension(const Container& variables, 46 : const data_expression& body, 47 : typename atermpp::enable_if_container< Container, variable >::type* = nullptr) 48 : : abstraction(bag_comprehension_binder(), variables, body) 49 : { 50 : assert(!variables.empty()); 51 : } 52 : 53 : /// Move semantics 54 : bag_comprehension(const bag_comprehension&) noexcept = default; 55 : bag_comprehension(bag_comprehension&&) noexcept = default; 56 : bag_comprehension& operator=(const bag_comprehension&) noexcept = default; 57 : bag_comprehension& operator=(bag_comprehension&&) noexcept = default; 58 : 59 : }; // class bag_comprehension 60 : 61 : template <class... ARGUMENTS> 62 16 : void make_bag_comprehension(atermpp::aterm& result, ARGUMENTS... arguments) 63 : { 64 16 : make_abstraction(result, bag_comprehension_binder(), arguments...); 65 16 : } 66 : 67 : 68 : //--- start generated class bag_comprehension ---// 69 : // prototype declaration 70 : std::string pp(const bag_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 bag_comprehension& x) 78 : { 79 : return out << data::pp(x); 80 : } 81 : 82 : /// \\brief swap overload 83 : inline void swap(bag_comprehension& t1, bag_comprehension& t2) 84 : { 85 : t1.swap(t2); 86 : } 87 : //--- end generated class bag_comprehension ---// 88 : 89 : } // namespace data 90 : 91 : } // namespace mcrl2 92 : 93 : #endif // MCRL2_DATA_BAG_COMPREHENSION_H