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/variable.h
      10             : /// \brief The class variable.
      11             : 
      12             : #ifndef MCRL2_DATA_VARIABLE_H
      13             : #define MCRL2_DATA_VARIABLE_H
      14             : 
      15             : #include "mcrl2/atermpp/aterm_appl.h"
      16             : #include "mcrl2/core/identifier_string.h"
      17             : #include "mcrl2/data/data_expression.h"
      18             : 
      19             : namespace mcrl2
      20             : {
      21             : 
      22             : namespace data
      23             : {
      24             : 
      25             : //--- start generated class variable ---//
      26             : /// \\brief A data variable
      27             : class variable: public data_expression
      28             : {
      29             :   public:
      30             : 
      31             : 
      32             :     /// Move semantics
      33    12230189 :     variable(const variable&) noexcept = default;
      34       93211 :     variable(variable&&) noexcept = default;
      35     4367689 :     variable& operator=(const variable&) noexcept = default;
      36       29888 :     variable& operator=(variable&&) noexcept = default;
      37             : 
      38    16450686 :     const core::identifier_string& name() const
      39             :     {
      40    16450686 :       return atermpp::down_cast<core::identifier_string>((*this)[0]);
      41             :     }
      42             : 
      43    22464074 :     const sort_expression& sort() const
      44             :     {
      45    22464074 :       return atermpp::down_cast<sort_expression>((*this)[1]);
      46             :     }
      47             : //--- start user section variable ---//
      48             :     /// \brief Default constructor.
      49       17839 :     variable()
      50       17839 :       : data_expression(core::detail::default_values::DataVarId)
      51       17839 :     {}
      52             : 
      53             :     /// \brief Constructor.
      54             :     /// \param term A term
      55    27997992 :     explicit variable(const atermpp::aterm& term)
      56    27997992 :       : data_expression(term)
      57             :     {
      58    27997992 :       assert(core::detail::check_term_DataVarId(*this));
      59    27997992 :     }
      60             : 
      61             :     /// \brief Constructor.
      62       62813 :     variable(const core::identifier_string& name, const sort_expression& sort)
      63       62813 :     {
      64       62813 :       atermpp::make_term_appl(*this, core::detail::function_symbol_DataVarId(), name, sort);
      65       62813 :     }
      66             : 
      67             : 
      68             :     /// \brief Constructor.
      69      552222 :     variable(const std::string& name, const sort_expression& sort)
      70      552222 :     {
      71      552222 :       atermpp::make_term_appl(*this, core::detail::function_symbol_DataVarId(), core::identifier_string(name), sort);
      72      552222 :     }
      73             : 
      74             : //--- end user section variable ---//
      75             : };
      76             : 
      77             : /// \\brief Make_variable constructs a new term into a given address.
      78             : /// \\ \param t The reference into which the new variable is constructed. 
      79             : template <class... ARGUMENTS>
      80    14438594 : inline void make_variable(atermpp::aterm_appl& t, const ARGUMENTS&... args)
      81             : {
      82    14438594 :   atermpp::make_term_appl(t, core::detail::function_symbol_DataVarId(), args...);
      83    14438594 : }
      84             : 
      85             : /// \\brief list of variables
      86             : typedef atermpp::term_list<variable> variable_list;
      87             : 
      88             : /// \\brief vector of variables
      89             : typedef std::vector<variable>    variable_vector;
      90             : 
      91             : // prototype declaration
      92             : std::string pp(const variable& x);
      93             : 
      94             : /// \\brief Outputs the object to a stream
      95             : /// \\param out An output stream
      96             : /// \\param x Object x
      97             : /// \\return The output stream
      98             : inline
      99        2084 : std::ostream& operator<<(std::ostream& out, const variable& x)
     100             : {
     101        2084 :   return out << data::pp(x);
     102             : }
     103             : 
     104             : /// \\brief swap overload
     105           0 : inline void swap(variable& t1, variable& t2)
     106             : {
     107           0 :   t1.swap(t2);
     108           0 : }
     109             : //--- end generated class variable ---//
     110             : 
     111             : 
     112             : // template function overloads
     113             : std::string pp(const variable_list& x);
     114             : std::string pp(const variable_vector& x);
     115             : std::string pp(const std::set<variable>& x);
     116             : std::string pp(const std::set<variable>& x);
     117             : std::set<data::variable> find_all_variables(const data::variable& x);
     118             : std::set<data::variable> find_all_variables(const data::variable_list& x);
     119             : std::set<core::identifier_string> find_identifiers(const data::variable_list& x);
     120             : 
     121             : } // namespace data
     122             : 
     123             : } // namespace mcrl2
     124             : 
     125             : 
     126             : namespace std 
     127             : {
     128             : 
     129             : template<>
     130             : struct hash<mcrl2::data::variable>
     131             : {
     132             :   // Default constructor, required for const qualified hash functions. 
     133      836811 :     hash()
     134      836811 :     {}
     135             :   
     136      836811 :     std::size_t operator()(const mcrl2::data::variable& v) const
     137             :     {
     138             :       const hash<atermpp::aterm> hasher; 
     139      836811 :       return hasher(v);
     140             :     }
     141             : };
     142             :   
     143             : } // namespace std
     144             : 
     145             : #endif // MCRL2_DATA_VARIABLE_H
     146             :