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