LCOV - code coverage report
Current view: top level - data/include/mcrl2/data - standard.h (source / functions) Hit Total Coverage
Test: mcrl2_coverage.info.cleaned Lines: 123 124 99.2 %
Date: 2024-03-08 02:52:28 Functions: 73 73 100.0 %
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/standard.h
      10             : /// \brief Standard functions that are available for all sorts.
      11             : 
      12             : #ifndef MCRL2_DATA_STANDARD_H
      13             : #define MCRL2_DATA_STANDARD_H
      14             : 
      15             : #include "mcrl2/core/detail/construction_utility.h"
      16             : #include "mcrl2/data/abstraction.h"
      17             : #include "mcrl2/data/data_equation.h"
      18             : 
      19             : 
      20             : namespace mcrl2
      21             : {
      22             : 
      23             : namespace data
      24             : {
      25             : 
      26             : // predeclare
      27             : namespace sort_bool
      28             : {
      29             : const basic_sort& bool_();
      30             : const function_symbol& false_();
      31             : const function_symbol& true_();
      32             : application and_(const data_expression&,const data_expression&);
      33             : application not_(const data_expression&);
      34             : bool is_bool(const sort_expression&);
      35             : } // namespace sort_bool
      36             : 
      37             : /// \cond INTERNAL_DOCS
      38             : namespace detail
      39             : {
      40             : 
      41             : /// \ Component to facilitate code generation
      42             : template < typename Derived >
      43             : struct symbol : public core::detail::singleton_identifier< Derived >
      44             : {
      45      893073 :   static bool is_symbol(const core::identifier_string& e)
      46             :   {
      47      893073 :     return e == core::detail::singleton_identifier< Derived >::instance();
      48             :   }
      49             : 
      50        1969 :   static bool is_application(const data_expression& e)
      51             :   {
      52        1969 :     return data::is_application(e) ? is_application(atermpp::down_cast<application>(e)) : false;
      53             :   }
      54             : 
      55      523449 :   static bool is_application(const application& e)
      56             :   {
      57      523449 :     return is_function_symbol(e.head());
      58             :   }
      59             : 
      60      523449 :   static bool is_function_symbol(const data_expression& e)
      61             :   {
      62      523449 :     return data::is_function_symbol(e) ? is_function_symbol(atermpp::down_cast<function_symbol>(e)) : false;
      63             :   }
      64             : 
      65      515209 :   static bool is_function_symbol(const function_symbol& e)
      66             :   {
      67      515209 :     return is_symbol(e.name());
      68             :   }
      69             : };
      70             : 
      71             : struct equal_symbol : public symbol< equal_symbol >
      72             : {
      73         110 :   static char const* initialise()
      74             :   {
      75         110 :     return "==";
      76             :   }
      77             : };
      78             : struct not_equal_symbol : public symbol< not_equal_symbol >
      79             : {
      80         110 :   static char const* initialise()
      81             :   {
      82         110 :     return "!=";
      83             :   }
      84             : };
      85             : struct if_symbol : public symbol< if_symbol >
      86             : {
      87         109 :   static char const* initialise()
      88             :   {
      89         109 :     return "if";
      90             :   }
      91             : };
      92             : struct less_symbol : public symbol< less_symbol >
      93             : {
      94         109 :   static char const* initialise()
      95             :   {
      96         109 :     return "<";
      97             :   }
      98             : };
      99             : struct less_equal_symbol : public symbol< less_equal_symbol >
     100             : {
     101         109 :   static char const* initialise()
     102             :   {
     103         109 :     return "<=";
     104             :   }
     105             : };
     106             : struct greater_symbol : public symbol< greater_symbol >
     107             : {
     108         109 :   static char const* initialise()
     109             :   {
     110         109 :     return ">";
     111             :   }
     112             : };
     113             : struct greater_equal_symbol : public symbol< greater_equal_symbol >
     114             : {
     115         109 :   static char const* initialise()
     116             :   {
     117         109 :     return ">=";
     118             :   }
     119             : };
     120             : } // namespace detail
     121             : /// \endcond
     122             : 
     123             : /// \brief Constructor for function symbol ==
     124             : /// \param[in] s A sort expression
     125             : /// \return function symbol equal_to
     126      600762 : inline function_symbol equal_to(const sort_expression& s)
     127             : {
     128     1201524 :   return function_symbol(detail::equal_symbol::instance(), make_function_sort_(s, s, sort_bool::bool_()));
     129             : }
     130             : 
     131             : /// \brief Recogniser for function ==
     132             : /// \param[in] e A data expression
     133             : /// \return true iff e is the function symbol matching ==
     134             : template < typename DataExpression >
     135             : inline bool is_equal_to_function_symbol(const DataExpression& e)
     136             : {
     137             :   return detail::equal_symbol::is_function_symbol(e);
     138             : }
     139             : 
     140             : /// \brief Application of function symbol ==
     141             : /// \param[in] arg0 A data expression
     142             : /// \param[in] arg1 A data expression
     143             : /// \return Application of == to a number of arguments
     144      524238 : inline application equal_to(const data_expression& arg0, const data_expression& arg1)
     145             : {
     146      524238 :   assert(arg0.sort() == arg1.sort());
     147     1048476 :   return equal_to(arg0.sort())(arg0, arg1);
     148             : }
     149             : 
     150             : /// \brief Recogniser for application of ==
     151             : /// \param[in] e A data expression
     152             : /// \return true iff e is an application of function symbol equal_to to a
     153             : ///     number of arguments
     154             : template < typename DataExpression >
     155      163292 : inline bool is_equal_to_application(const DataExpression& e)
     156             : {
     157      163292 :   return detail::equal_symbol::is_application(e);
     158             : }
     159             : 
     160             : /// \brief Constructor for function symbol !=
     161             : /// \param[in] s A sort expression
     162             : /// \return function symbol not_equal_to
     163      194554 : inline function_symbol not_equal_to(const sort_expression& s)
     164             : {
     165      389108 :   return function_symbol(detail::not_equal_symbol::instance(), make_function_sort_(s, s, sort_bool::bool_()));
     166             : }
     167             : 
     168             : /// \brief Recogniser for function !=
     169             : /// \param[in] e A data expression
     170             : /// \return true iff e is the function symbol matching !=
     171             : template < typename DataExpression >
     172             : inline bool is_not_equal_to_function_symbol(const DataExpression& e)
     173             : {
     174             :   return detail::not_equal_symbol::is_function_symbol(e);
     175             : }
     176             : 
     177             : /// \brief Application of function symbol !=
     178             : /// \param[in] arg0 A data expression
     179             : /// \param[in] arg1 A data expression
     180             : /// \return Application of != to a number of arguments
     181      118030 : inline application not_equal_to(const data_expression& arg0, const data_expression& arg1)
     182             : {
     183      118030 :   assert(arg0.sort() == arg1.sort());
     184      236060 :   return not_equal_to(arg0.sort())(arg0, arg1);
     185             : }
     186             : 
     187             : /// \brief Recogniser for application of !=
     188             : /// \param[in] e A data expression
     189             : /// \return true iff e is an application of function symbol not_equal_to to a
     190             : ///     number of arguments
     191             : template < typename DataExpression >
     192      102752 : inline bool is_not_equal_to_application(const DataExpression& e)
     193             : {
     194      102752 :   return detail::not_equal_symbol::is_application(e);
     195             : }
     196             : 
     197             : /// \brief Constructor for function symbol if
     198             : /// \param[in] s A sort expression
     199             : /// \return function symbol if_
     200      425052 : inline function_symbol if_(const sort_expression& s)
     201             : {
     202      850104 :   return function_symbol(detail::if_symbol::instance(), make_function_sort_(sort_bool::bool_(), s, s, s));
     203             : }
     204             : 
     205             : /// \brief Recogniser for function if
     206             : /// \param[in] e A data expression
     207             : /// \return true iff e is the function symbol matching if_
     208             : template < typename DataExpression >
     209           6 : inline bool is_if_function_symbol(const DataExpression& e)
     210             : {
     211           6 :   return detail::if_symbol::is_function_symbol(e);
     212             : }
     213             : 
     214             : /// \brief Application of function symbol if
     215             : /// \param[in] arg0 A data expression
     216             : /// \param[in] arg1 A data expression
     217             : /// \param[in] arg2 A data expression
     218             : /// \return Application of if to a number of arguments
     219      348051 : inline application if_(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
     220             : {
     221      348051 :   assert(sort_bool::is_bool(arg0.sort()));
     222      348051 :   assert(arg1.sort() == arg2.sort());
     223             : 
     224      696102 :   return if_(arg1.sort())(arg0, arg1, arg2);
     225             : }
     226             : 
     227             : /// \brief Recogniser for application of if
     228             : /// \param[in] e A data expression
     229             : /// \return true iff e is an application of function symbol if_ to a
     230             : ///     number of arguments
     231             : template < typename DataExpression >
     232       39520 : inline bool is_if_application(const DataExpression& e)
     233             : {
     234       39520 :   return detail::if_symbol::is_application(e);
     235             : }
     236             : 
     237             : /// \brief Constructor for function symbol <
     238             : /// \param[in] s A sort expression
     239             : /// \return function symbol less
     240      542480 : inline function_symbol less(const sort_expression& s)
     241             : {
     242     1084960 :   return function_symbol(detail::less_symbol::instance(), make_function_sort_(s, s, sort_bool::bool_()));
     243             : }
     244             : 
     245             : /// \brief Recogniser for function <
     246             : /// \param[in] e A data expression
     247             : /// \return true iff e is the function symbol matching <
     248             : template < typename DataExpression >
     249             : inline bool is_less_function_symbol(const DataExpression& e)
     250             : {
     251             :   return detail::less_symbol::is_function_symbol(e);
     252             : }
     253             : 
     254             : /// \brief Application of function symbol <
     255             : /// \param[in] arg0 A data expression
     256             : /// \param[in] arg1 A data expression
     257             : /// \return Application of < to a number of arguments
     258      466128 : inline application less(const data_expression& arg0, const data_expression& arg1)
     259             : {
     260      466128 :   assert(arg0.sort() == arg1.sort());
     261      932256 :   return less(arg0.sort())(arg0, arg1);
     262             : }
     263             : 
     264             : /// \brief Recogniser for application of <
     265             : /// \param[in] e A data expression
     266             : /// \return true iff e is an application of function symbol less to a
     267             : ///     number of arguments
     268             : template < typename DataExpression >
     269       60595 : inline bool is_less_application(const DataExpression& e)
     270             : {
     271       60595 :   return detail::less_symbol::is_application(e);
     272             : }
     273             : 
     274             : /// \brief Constructor for function symbol <=
     275             : /// \param[in] s A sort expression
     276             : /// \return function symbol less_equal
     277      556431 : inline function_symbol less_equal(const sort_expression& s)
     278             : {
     279     1112862 :   return function_symbol(detail::less_equal_symbol::instance(), make_function_sort_(s, s, sort_bool::bool_()));
     280             : }
     281             : 
     282             : /// \brief Recogniser for function <=
     283             : /// \param[in] e A data expression
     284             : /// \return true iff e is the function symbol matching <=
     285             : template < typename DataExpression >
     286             : inline bool is_less_equal_function_symbol(const DataExpression& e)
     287             : {
     288             :   return detail::less_equal_symbol::is_function_symbol(e);
     289             : }
     290             : 
     291             : /// \brief Application of function symbol <=
     292             : /// \param[in] arg0 A data expression
     293             : /// \param[in] arg1 A data expression
     294             : /// \return Application of <= to a number of arguments
     295      480079 : inline application less_equal(const data_expression& arg0, const data_expression& arg1)
     296             : {
     297      480079 :   assert(arg0.sort() == arg1.sort());
     298      960158 :   return less_equal(arg0.sort())(arg0, arg1);
     299             : }
     300             : 
     301             : /// \brief Recogniser for application of <=
     302             : /// \param[in] e A data expression
     303             : /// \return true iff e is an application of function symbol less_equal to a
     304             : ///     number of arguments
     305             : template < typename DataExpression >
     306       53106 : inline bool is_less_equal_application(const DataExpression& e)
     307             : {
     308       53106 :   return detail::less_equal_symbol::is_application(e);
     309             : }
     310             : 
     311             : /// \brief Constructor for function symbol >
     312             : /// \param[in] s A sort expression
     313             : /// \return function symbol greater
     314      161661 : inline function_symbol greater(const sort_expression& s)
     315             : {
     316      323322 :   return function_symbol(detail::greater_symbol::instance(), make_function_sort_(s, s, sort_bool::bool_()));
     317             : }
     318             : 
     319             : /// \brief Recogniser for function >
     320             : /// \param[in] e A data expression
     321             : /// \return true iff e is the function symbol matching >
     322             : template < typename DataExpression >
     323             : inline bool is_greater_function_symbol(const DataExpression& e)
     324             : {
     325             :   return detail::greater_symbol::is_function_symbol(e);
     326             : }
     327             : 
     328             : /// \brief Application of function symbol >
     329             : /// \param[in] arg0 A data expression
     330             : /// \param[in] arg1 A data expression
     331             : /// \return Application of > to a number of arguments
     332       85309 : inline application greater(const data_expression& arg0, const data_expression& arg1)
     333             : {
     334       85309 :   assert(arg0.sort() == arg1.sort());
     335      170618 :   return greater(arg0.sort())(arg0, arg1);
     336             : }
     337             : 
     338             : /// \brief Recogniser for application of >
     339             : /// \param[in] e A data expression
     340             : /// \return true iff e is an application of function symbol greater to a
     341             : ///     number of arguments
     342             : template < typename DataExpression >
     343       52623 : inline bool is_greater_application(const DataExpression& e)
     344             : {
     345       52623 :   return detail::greater_symbol::is_application(e);
     346             : }
     347             : 
     348             : /// \brief Constructor for function symbol >=
     349             : /// \param[in] s A sort expression
     350             : /// \return function symbol greater_equal
     351      148095 : inline function_symbol greater_equal(const sort_expression& s)
     352             : {
     353      296190 :   return function_symbol(detail::greater_equal_symbol::instance(), make_function_sort_(s, s, sort_bool::bool_()));
     354             : }
     355             : 
     356             : /// \brief Recogniser for function >=
     357             : /// \param[in] e A data expression
     358             : /// \return true iff e is the function symbol matching >=
     359             : template < typename DataExpression >
     360             : inline bool is_greater_equal_function_symbol(const DataExpression& e)
     361             : {
     362             :   return detail::greater_equal_symbol::is_function_symbol(e);
     363             : }
     364             : 
     365             : /// \brief Application of function symbol >=
     366             : /// \param[in] arg0 A data expression
     367             : /// \param[in] arg1 A data expression
     368             : /// \return Application of >= to a number of arguments
     369       71743 : inline application greater_equal(const data_expression& arg0, const data_expression& arg1)
     370             : {
     371       71743 :   assert(arg0.sort() == arg1.sort());
     372      143486 :   return greater_equal(arg0.sort())(arg0, arg1);
     373             : }
     374             : 
     375             : /// \brief Recogniser for application of >=
     376             : /// \param[in] e A data expression
     377             : /// \return true iff e is an application of function symbol greater_equal to a
     378             : ///     number of arguments
     379             : template < typename DataExpression >
     380       52489 : inline bool is_greater_equal_application(const DataExpression& e)
     381             : {
     382       52489 :   return detail::greater_equal_symbol::is_application(e);
     383             : }
     384             : 
     385             : /// \brief Give all standard system defined functions for sort s
     386             : /// \param[in] s A sort expression
     387             : /// \return All standard system defined functions for sort s
     388       71752 : inline function_symbol_vector standard_generate_functions_code(const sort_expression& s)
     389             : {
     390       71752 :   function_symbol_vector result;
     391       71752 :   result.push_back(equal_to(s));
     392       71752 :   result.push_back(not_equal_to(s));
     393       71752 :   result.push_back(if_(s));
     394       71752 :   result.push_back(less(s));
     395       71752 :   result.push_back(less_equal(s));
     396       71752 :   result.push_back(greater_equal(s));
     397       71752 :   result.push_back(greater(s));
     398             : 
     399       71752 :   return result;
     400           0 : }
     401             : 
     402             : /// \brief Give all standard system defined equations for sort s
     403             : /// \param[in] s A sort expression
     404             : /// \return All standard system defined equations for sort s
     405       71742 : inline data_equation_vector standard_generate_equations_code(const sort_expression& s)
     406             : {
     407       71742 :   data_equation_vector result;
     408      143484 :   variable b("b", sort_bool::bool_());
     409      143484 :   variable x("x", s);
     410      143484 :   variable y("y", s);
     411      143484 :   result.push_back(data_equation(variable_list({x}), equal_to(x, x), sort_bool::true_()));
     412      215226 :   result.push_back(data_equation(variable_list({x, y}), not_equal_to(x, y), sort_bool::not_(equal_to(x, y))));
     413      215226 :   result.push_back(data_equation(variable_list({x, y}), if_(sort_bool::true_(), x, y), x));
     414      215226 :   result.push_back(data_equation(variable_list({x, y}), if_(sort_bool::false_(), x, y), y));
     415      215226 :   result.push_back(data_equation(variable_list({b, x}), if_(b, x, x), x));
     416      143484 :   result.push_back(data_equation(variable_list({x}), less(x,x), sort_bool::false_()));
     417      143484 :   result.push_back(data_equation(variable_list({x}), less_equal(x,x), sort_bool::true_()));
     418      215226 :   result.push_back(data_equation(variable_list({x, y}), greater_equal(x,y), less_equal(y,x)));
     419      215226 :   result.push_back(data_equation(variable_list({x, y}), greater(x,y), less(y,x)));
     420             : 
     421             :   // For a function sort, add the equation f==g iff forall x.f(x)==g(x). This equation is not in the Specification and Analysis of Communicating Systems of 2014.
     422       71742 :   if (is_function_sort(s))
     423             :   {
     424       18434 :     const function_sort& fs = atermpp::down_cast<function_sort>(s);
     425       18434 :     variable_vector xvars,yvars;
     426       18434 :     std::size_t index=0;
     427       50671 :     for(const sort_expression& sort: fs.domain())
     428             :     {
     429       32237 :       std::stringstream xs;
     430       32237 :       xs << "x" << index;
     431       32237 :       ++index;
     432       32237 :       variable x(xs.str(),sort);
     433       32237 :       xvars.push_back(x);
     434       32237 :     }
     435       36868 :     variable f("f",s);
     436       36868 :     variable g("g",s);
     437       18434 :     variable_list xvar_list=variable_list(xvars.begin(),xvars.end());
     438       55302 :     result.push_back(data_equation(variable_list({ f, g }) + xvar_list,
     439       36868 :                                    equal_to(f,g),
     440       36868 :                                    abstraction(forall_binder(),xvar_list,
     441       36868 :                                       equal_to(
     442       36868 :                                           application(f,xvars.begin(),xvars.end()),
     443       36868 :                                           application(g,xvars.begin(),xvars.end())))));
     444       18434 :   }
     445             : 
     446      143484 :   return result;
     447       71742 : }
     448             : 
     449             : } // namespace data
     450             : } // namespace mcrl2
     451             : 
     452             : #endif // MCRL2_DATA_STANDARD_H

Generated by: LCOV version 1.14