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