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/data_equation.h
      10             : /// \brief The class data_equation.
      11             : 
      12             : #ifndef MCRL2_DATA_DATA_EQUATION_H
      13             : #define MCRL2_DATA_DATA_EQUATION_H
      14             : 
      15             : #include "mcrl2/data/basic_sort.h"
      16             : #include "mcrl2/data/function_symbol.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : 
      21             : namespace data
      22             : {
      23             : 
      24             : // predeclare
      25             : namespace sort_bool
      26             : {
      27             : function_symbol const& true_();
      28             : } // namespace sort_bool
      29             : 
      30             : //--- start generated class data_equation ---//
      31             : /// \\brief A data equation
      32             : class data_equation: public atermpp::aterm_appl
      33             : {
      34             :   public:
      35             :     /// \\brief Default constructor.
      36     3093782 :     data_equation()
      37     3093782 :       : atermpp::aterm_appl(core::detail::default_values::DataEqn)
      38     3093782 :     {}
      39             : 
      40             :     /// \\brief Constructor.
      41             :     /// \\param term A term
      42           0 :     explicit data_equation(const atermpp::aterm& term)
      43           0 :       : atermpp::aterm_appl(term)
      44             :     {
      45           0 :       assert(core::detail::check_term_DataEqn(*this));
      46           0 :     }
      47             : 
      48             :     /// \\brief Constructor.
      49      149247 :     data_equation(const variable_list& variables, const data_expression& condition, const data_expression& lhs, const data_expression& rhs)
      50      149247 :       : atermpp::aterm_appl(core::detail::function_symbol_DataEqn(), variables, condition, lhs, rhs)
      51      149247 :     {}
      52             : 
      53             :     /// \\brief Constructor.
      54             :     template <typename Container>
      55        4382 :     data_equation(const Container& variables, const data_expression& condition, const data_expression& lhs, const data_expression& rhs, typename atermpp::enable_if_container<Container, variable>::type* = nullptr)
      56        4382 :       : atermpp::aterm_appl(core::detail::function_symbol_DataEqn(), variable_list(variables.begin(), variables.end()), condition, lhs, rhs)
      57        4382 :     {}
      58             : 
      59             :     /// Move semantics
      60    10020909 :     data_equation(const data_equation&) noexcept = default;
      61    13706707 :     data_equation(data_equation&&) noexcept = default;
      62     1800532 :     data_equation& operator=(const data_equation&) noexcept = default;
      63        3197 :     data_equation& operator=(data_equation&&) noexcept = default;
      64             : 
      65     5444335 :     const variable_list& variables() const
      66             :     {
      67     5444335 :       return atermpp::down_cast<variable_list>((*this)[0]);
      68             :     }
      69             : 
      70     5193419 :     const data_expression& condition() const
      71             :     {
      72     5193419 :       return atermpp::down_cast<data_expression>((*this)[1]);
      73             :     }
      74             : 
      75    11934685 :     const data_expression& lhs() const
      76             :     {
      77    11934685 :       return atermpp::down_cast<data_expression>((*this)[2]);
      78             :     }
      79             : 
      80     4574102 :     const data_expression& rhs() const
      81             :     {
      82     4574102 :       return atermpp::down_cast<data_expression>((*this)[3]);
      83             :     }
      84             : //--- start user section data_equation ---//
      85             :     /// \brief Constructor.
      86             :     ///
      87             :     /// \param[in] variables The free variables of the data_equation.
      88             :     /// \param[in] lhs The left hand side of the data_equation.
      89             :     /// \param[in] rhs The right hand side of the data_equation.
      90             :     /// \post this is the data equation representing the input, with
      91             :     ///       condition true
      92             :     template < typename Container >
      93     2550487 :     data_equation(const Container& variables,
      94             :                   const data_expression& lhs,
      95             :                   const data_expression& rhs,
      96             :                   typename atermpp::enable_if_container< Container, variable >::type* = nullptr)
      97     2550487 :       : atermpp::aterm_appl(core::detail::function_symbol_DataEqn(), variable_list(variables.begin(),variables.end()), sort_bool::true_(), lhs, rhs)
      98     2550487 :     {}
      99             : 
     100             :     /// \brief Constructor.
     101             :     ///
     102             :     /// \param[in] lhs The left hand side of the data equation.
     103             :     /// \param[in] rhs The right hand side of the data equation.
     104             :     /// \post this is the data equations representing the input, without
     105             :     ///       variables, and condition true
     106       24503 :     data_equation(const data_expression& lhs,
     107             :                   const data_expression& rhs)
     108       24503 :       : atermpp::aterm_appl(core::detail::function_symbol_DataEqn(), variable_list(), sort_bool::true_(), lhs, rhs)
     109       24503 :     {}
     110             : //--- end user section data_equation ---//
     111             : };
     112             : 
     113             : /// \\brief Make_data_equation constructs a new term into a given address.
     114             : /// \\ \param t The reference into which the new data_equation is constructed. 
     115             : template <class... ARGUMENTS>
     116     2730468 : inline void make_data_equation(atermpp::aterm_appl& t, const ARGUMENTS&... args)
     117             : {
     118     2730468 :   atermpp::make_term_appl(t, core::detail::function_symbol_DataEqn(), args...);
     119     2730468 : }
     120             : 
     121             : /// \\brief list of data_equations
     122             : typedef atermpp::term_list<data_equation> data_equation_list;
     123             : 
     124             : /// \\brief vector of data_equations
     125             : typedef std::vector<data_equation>    data_equation_vector;
     126             : 
     127             : // prototype declaration
     128             : std::string pp(const data_equation& x);
     129             : 
     130             : /// \\brief Outputs the object to a stream
     131             : /// \\param out An output stream
     132             : /// \\param x Object x
     133             : /// \\return The output stream
     134             : inline
     135           1 : std::ostream& operator<<(std::ostream& out, const data_equation& x)
     136             : {
     137           1 :   return out << data::pp(x);
     138             : }
     139             : 
     140             : /// \\brief swap overload
     141             : inline void swap(data_equation& t1, data_equation& t2)
     142             : {
     143             :   t1.swap(t2);
     144             : }
     145             : //--- end generated class data_equation ---//
     146             : 
     147             : /// \brief Recognizer function.
     148             : /// \param[in] t A aterm appl of which it is checked whether it is a data_equation.
     149             : /// \returns True if the provided argument is a data_equation. 
     150     2886264 : inline bool is_data_equation(const atermpp::aterm_appl& t)
     151             : {
     152     2886264 :   return t.function()==core::detail::function_symbol_DataEqn();
     153             : }
     154             : 
     155             : // template function overloads
     156             : std::string pp(const data_equation_list& x);
     157             : std::string pp(const data_equation_vector& x);
     158             : data::data_equation translate_user_notation(const data::data_equation& x);
     159             : std::set<data::sort_expression> find_sort_expressions(const data::data_equation& x);
     160             : std::set<data::function_symbol> find_function_symbols(const data::data_equation& x);
     161             : 
     162             : } // namespace data
     163             : 
     164             : } // namespace mcrl2
     165             : 
     166             : #endif // MCRL2_DATA_DATA_EQUATION_H
     167             :