LCOV - code coverage report
Current view: top level - data/include/mcrl2/data - data_expression.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 73 75 97.3 %
Date: 2024-03-08 02:52:28 Functions: 30 31 96.8 %
Legend: Lines: hit not hit

          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_expression.h
      10             : /// \brief The class data_expression.
      11             : 
      12             : #ifndef MCRL2_DATA_DATA_EXPRESSION_H
      13             : #define MCRL2_DATA_DATA_EXPRESSION_H
      14             : 
      15             : #include "mcrl2/data/container_sort.h"
      16             : #include "mcrl2/data/function_sort.h"
      17             : #include "mcrl2/data/untyped_sort.h"
      18             : 
      19             : namespace mcrl2
      20             : {
      21             : 
      22             : namespace data
      23             : {
      24             : 
      25             : /// \brief Returns true if the term t is an abstraction
      26    91231582 : inline bool is_abstraction(const atermpp::aterm& x)
      27             : {
      28    91231582 :   return x.function() == core::detail::function_symbols::Binder;
      29             : }
      30             : 
      31             : /// \brief Returns true if the term t is a lambda abstraction
      32      329696 : inline bool is_lambda(const atermpp::aterm_appl& x)
      33             : {
      34      329696 :   return is_abstraction(x) && atermpp::down_cast<const atermpp::aterm_appl>(x[0]).function() == core::detail::function_symbols::Lambda;
      35             : }
      36             : 
      37             : /// \brief Returns true if the term t is a universal quantification
      38      354593 : inline bool is_forall(const atermpp::aterm_appl& x)
      39             : {
      40      354593 :   return is_abstraction(x) && atermpp::down_cast<const atermpp::aterm_appl>(x[0]).function() == core::detail::function_symbols::Forall;
      41             : }
      42             : 
      43             : /// \brief Returns true if the term t is an existential quantification
      44      328675 : inline bool is_exists(const atermpp::aterm_appl& x)
      45             : {
      46      328675 :   return is_abstraction(x) && atermpp::down_cast<const atermpp::aterm_appl>(x[0]).function() == core::detail::function_symbols::Exists;
      47             : }
      48             : 
      49             : /// \brief Returns true if the term t is a set comprehension
      50      320302 : inline bool is_set_comprehension(const atermpp::aterm_appl& x)
      51             : {
      52      320302 :   return is_abstraction(x) && atermpp::down_cast<const atermpp::aterm_appl>(x[0]).function() == core::detail::function_symbols::SetComp;
      53             : }
      54             : 
      55             : /// \brief Returns true if the term t is a bag comprehension
      56      320274 : inline bool is_bag_comprehension(const atermpp::aterm_appl& x)
      57             : {
      58      320274 :   return is_abstraction(x) && atermpp::down_cast<const atermpp::aterm_appl>(x[0]).function() == core::detail::function_symbols::BagComp;
      59             : }
      60             : 
      61             : /// \brief Returns true if the term t is a set/bag comprehension.
      62      287096 : inline bool is_untyped_set_or_bag_comprehension(const atermpp::aterm_appl& x)
      63             : {
      64      287096 :   return is_abstraction(x) && atermpp::down_cast<const atermpp::aterm_appl>(x[0]).function() == core::detail::function_symbols::UntypedSetBagComp;
      65             : }
      66             : 
      67             : /// \brief Returns true if the term t is a function symbol
      68   134152701 : inline bool is_function_symbol(const atermpp::aterm_appl& x)
      69             : {
      70   134152701 :   return x.function() == core::detail::function_symbols::OpId;
      71             : }
      72             : 
      73             : /// \brief Returns true if the term t is a variable
      74   128147615 : inline bool is_variable(const atermpp::aterm& x)
      75             : {
      76   128147615 :   return x.function() == core::detail::function_symbols::DataVarId;
      77             : }
      78             : 
      79             : /// \brief Returns true if the term t is an application
      80             : /// \details This function is inefficient as the arity of a term must 
      81             : ///          be determined and an inspection must take place in an 
      82             : ///          array of function symbols. Therefore, there is an more efficient overload
      83             : ///          is_application(const data_expression& x).
      84     5847076 : inline bool is_application(const atermpp::aterm_appl& x)
      85             : {
      86     5847076 :   return core::detail::gsIsDataAppl(x);
      87             : }
      88             : 
      89             : /// \brief Returns true if the term t is an application, but it does not check
      90             : ///        whether an application symbol of sufficient arity exists, assuming
      91             : ///        this is ok.
      92       18824 : inline bool is_application_no_check(const atermpp::aterm_appl& x)
      93             : {
      94       18824 :   return core::detail::gsIsDataAppl_no_check(x);
      95             : }
      96             : 
      97             : /// \brief Returns true if the term t is a where clause
      98    37623800 : inline bool is_where_clause(const atermpp::aterm_appl& x)
      99             : {
     100    37623800 :   return x.function() == core::detail::function_symbols::Whr;
     101             : }
     102             : 
     103             : /// \brief Returns true if the term t is an identifier
     104    29392018 : inline bool is_untyped_identifier(const atermpp::aterm_appl& x)
     105             : {
     106    29392018 :   return x.function() == core::detail::function_symbols::UntypedIdentifier;
     107             : }
     108             : 
     109             : class application; // prototype
     110             : 
     111             : /// \brief data expression.
     112             : ///
     113             : /// A data expression can be any of:
     114             : /// - variable
     115             : /// - function symbol
     116             : /// - application
     117             : /// - abstraction
     118             : /// - where clause
     119             : /// - set enumeration
     120             : /// - bag enumeration
     121             : 
     122             : //--- start generated class data_expression ---//
     123             : /// \\brief A data expression
     124             : class data_expression: public atermpp::aterm_appl
     125             : {
     126             :   public:
     127             :     /// \\brief Default constructor.
     128     7867927 :     data_expression()
     129     7867927 :       : atermpp::aterm_appl(core::detail::default_values::DataExpr)
     130     7867927 :     {}
     131             : 
     132             :     /// \\brief Constructor.
     133             :     /// \\param term A term
     134   204385585 :     explicit data_expression(const atermpp::aterm& term)
     135   204385585 :       : atermpp::aterm_appl(term)
     136             :     {
     137   204385585 :       assert(core::detail::check_rule_DataExpr(*this));
     138   204385585 :     }
     139             : 
     140             :     /// Move semantics
     141    31700282 :     data_expression(const data_expression&) noexcept = default;
     142     5473792 :     data_expression(data_expression&&) noexcept = default;
     143     5825910 :     data_expression& operator=(const data_expression&) noexcept = default;
     144      442365 :     data_expression& operator=(data_expression&&) noexcept = default;
     145             : //--- start user section data_expression ---//
     146             :     /// \brief A function to efficiently determine whether a data expression is 
     147             :     ///        made by the default constructor.
     148      726474 :     bool is_default_data_expression() const
     149             :     {
     150      726474 :       return *this==core::detail::default_values::DataExpr;
     151             :     }
     152             : 
     153             :     application operator()(const data_expression& e) const;
     154             : 
     155             :     application operator()(const data_expression& e1,
     156             :                            const data_expression& e2) const;
     157             : 
     158             :     application operator()(const data_expression& e1,
     159             :                            const data_expression& e2,
     160             :                            const data_expression& e3) const;
     161             : 
     162             :     application operator()(const data_expression& e1,
     163             :                            const data_expression& e2,
     164             :                            const data_expression& e3,
     165             :                            const data_expression& e4) const;
     166             : 
     167             :     /// \brief Returns the sort of the data expression
     168             : 
     169             :     sort_expression sort() const;
     170             : 
     171             :     private:
     172             :       // The following methods are not to be used in a data_expression.
     173             :       // They are restricted to a data_appl. 
     174             :       const_iterator begin() const;
     175             :       const_iterator end() const;
     176             : 
     177             : //--- end user section data_expression ---//
     178             : };
     179             : 
     180             : /// \\brief list of data_expressions
     181             : typedef atermpp::term_list<data_expression> data_expression_list;
     182             : 
     183             : /// \\brief vector of data_expressions
     184             : typedef std::vector<data_expression>    data_expression_vector;
     185             : 
     186             : // prototype declaration
     187             : std::string pp(const data_expression& x);
     188             : 
     189             : /// \\brief Outputs the object to a stream
     190             : /// \\param out An output stream
     191             : /// \\param x Object x
     192             : /// \\return The output stream
     193             : inline
     194        2957 : std::ostream& operator<<(std::ostream& out, const data_expression& x)
     195             : {
     196        2957 :   return out << data::pp(x);
     197             : }
     198             : 
     199             : /// \\brief swap overload
     200             : inline void swap(data_expression& t1, data_expression& t2)
     201             : {
     202             :   t1.swap(t2);
     203             : }
     204             : //--- end generated class data_expression ---//
     205             : 
     206             : inline void make_data_expression(data_expression& result)
     207             : {
     208             :   static_cast<atermpp::aterm_appl&>(result)=core::detail::default_values::DataExpr;
     209             : }
     210             : 
     211             : /// \brief Test for a data_expression expression
     212             : /// \param x A term
     213             : /// \return True if it is a data_expression expression
     214             : inline
     215      287077 : bool is_data_expression(const atermpp::aterm_appl& x)
     216             : {
     217      287077 :   return is_lambda(x)                           ||
     218      287077 :          is_forall(x)                           ||
     219      287071 :          is_exists(x)                           ||
     220      287071 :          is_set_comprehension(x)                ||
     221      287071 :          is_bag_comprehension(x)                ||
     222      287071 :          is_untyped_set_or_bag_comprehension(x) ||
     223      557722 :          is_function_symbol(x)                  ||
     224      270651 :          is_variable(x)                         ||
     225      270184 :          is_application(x)                      ||
     226      779891 :          is_where_clause(x)                     ||
     227      492814 :          is_untyped_identifier(x);
     228             : }
     229             : 
     230             : /// \brief Converts an container with data expressions to data_expression_list
     231             : /// \param r A range of data expressions.
     232             : /// \note This function uses implementation details of the iterator type
     233             : /// and hence is sometimes efficient than copying all elements of the list.
     234             : template < typename Container >
     235           0 : inline data_expression_list make_data_expression_list(Container const& r, typename atermpp::enable_if_container< Container, data_expression >::type* = nullptr)
     236             : {
     237           0 :   return data_expression_list(r.begin(),r.end());
     238             : }
     239             : 
     240             : class variable;
     241             : 
     242             : // template function overloads
     243             : std::string pp(const data_expression_list& x);
     244             : std::string pp(const data_expression_vector& x);
     245             : data::data_expression translate_user_notation(const data::data_expression& x);
     246             : std::set<data::sort_expression> find_sort_expressions(const data::data_expression& x);
     247             : std::set<data::variable> find_all_variables(const data::data_expression& x);
     248             : std::set<data::variable> find_all_variables(const data::data_expression_list& x);
     249             : std::set<data::variable> find_free_variables(const data::data_expression& x);
     250             : std::set<data::variable> find_free_variables(const data::data_expression_list& x);
     251             : bool search_variable(const data::data_expression& x, const data::variable& v);
     252             : 
     253             : inline
     254        2534 : bool is_constant(const data_expression& x)
     255             : {
     256        2534 :   return find_free_variables(x).empty();
     257             : }
     258             : 
     259             : typedef atermpp::term_list<variable> variable_list;
     260             : variable_list free_variables(const data_expression& x);
     261             : 
     262             : } // namespace data
     263             : 
     264             : } // namespace mcrl2
     265             : 
     266             : // The trick of including application.h only at this point is needed to break
     267             : // the circular dependencies between application and data_expression. This
     268             : // dependency was introduced to allow the application operator to be defined for
     269             : // all data expression types.
     270             : #ifndef MCRL2_DATA_APPLICATION_H
     271             : #include "mcrl2/data/application.h"
     272             : #endif
     273             : 
     274             : namespace mcrl2
     275             : {
     276             : namespace data
     277             : {
     278             : /// \brief Returns true if the term t is an application.
     279             : /// \param t The variable that is checked. 
     280    35016930 : inline bool is_application(const data_expression& t)
     281             : {
     282    65145626 :   return !(is_function_symbol(t) ||
     283    30128696 :            is_variable(t) ||
     284    26542038 :            is_where_clause(t) ||
     285    26541455 :            is_abstraction(t) ||
     286    61545426 :            is_untyped_identifier(t));
     287             : } 
     288             : 
     289             : /// \brief Transform a variable_list into a data_expression_list
     290             : inline 
     291        4769 : const data_expression_list& variable_list_to_data_expression_list(const variable_list& l)
     292             : {
     293        4769 :   return atermpp::down_cast<data_expression_list>(static_cast<const atermpp::aterm&>(l));
     294             : }
     295             : 
     296             : /// \brief Apply a data expression to a data expression.
     297             : inline
     298     3140591 : application data_expression::operator()(const data_expression& e) const
     299             : {
     300     3140591 :   return application(*this, e);
     301             : }
     302             : 
     303             : /// \brief Apply data expression to two data expressions
     304             : inline
     305     4469594 : application data_expression::operator()(const data_expression& e1, const data_expression& e2) const
     306             : {
     307     4469594 :   return application(*this, e1, e2);
     308             : }
     309             : 
     310             : /// \brief Apply data expression to three data expressions
     311             : inline
     312      825045 : application data_expression::operator()(const data_expression& e1, const data_expression& e2, const data_expression& e3) const
     313             : {
     314      825045 :   return application(*this, e1, e2, e3);
     315             : }
     316             : 
     317             : /// \brief Apply data expression to four data expressions
     318             : inline
     319      122892 : application data_expression::operator()(const data_expression& e1, const data_expression& e2, const data_expression& e3, const data_expression& e4) const
     320             : {
     321      122892 :   return application(*this, e1, e2, e3, e4);
     322             : }
     323             : 
     324             : } // namespace data
     325             : } // namespace mcrl2
     326             : 
     327             : 
     328             : namespace std
     329             : {
     330             : 
     331             : template<>
     332             : struct hash<mcrl2::data::data_expression>
     333             : {
     334        4740 :     std::size_t operator()(const mcrl2::data::data_expression& v) const
     335             :     {
     336             :       const hash<atermpp::aterm> hasher;
     337        4740 :       return hasher(v);
     338             :     }
     339             : };
     340             : 
     341             : } // namespace std
     342             : 
     343             : 
     344             : 
     345             : #endif // MCRL2_DATA_DATA_EXPRESSION_H
     346             : 

Generated by: LCOV version 1.14