Line data    Source code

       1             : // Author(s): Wieger Wesselink
       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/undefined.h
      10             : /// \brief add your file description here.
      11             : 
      12             : #ifndef MCRL2_DATA_UNDEFINED_H
      13             : #define MCRL2_DATA_UNDEFINED_H
      14             : 
      15             : #include "mcrl2/data/real.h"
      16             : 
      17             : namespace mcrl2 {
      18             : 
      19             : namespace data {
      20             : 
      21             : /// \brief Returns an index that corresponds to 'undefined'
      22             : inline
      23        5286 : constexpr std::size_t undefined_index()
      24             : {
      25        5286 :   return std::size_t(-1);
      26             : }
      27             : 
      28             : /// \brief Returns a data variable that corresponds to 'undefined'
      29             : inline
      30          66 : const data::variable& undefined_variable()
      31             : {
      32          66 :   static data::variable v("@undefined_variable", data::sort_expression());
      33          66 :   return v;
      34             : }
      35             : 
      36             : /// \brief Returns a data variable that corresponds to 'undefined'
      37             : inline
      38         776 : const data::variable& undefined_real_variable()
      39             : {
      40         776 :   static data::variable v("@undefined_real_variable", data::sort_real::real_());
      41         776 :   return v;
      42             : }
      43             : 
      44             : /// \brief Returns a sort expression that corresponds to 'undefined'
      45             : inline
      46             : const data::sort_expression& undefined_sort_expression()
      47             : {
      48             :   static data::basic_sort v("@undefined_sort_expression");
      49             :   return v;
      50             : }
      51             : 
      52             : /// \brief Returns a data expression that corresponds to 'undefined'
      53             : inline
      54        3928 : const data::data_expression& undefined_data_expression()
      55             : {
      56        3928 :   static data::variable v("@undefined_data_expression", data::sort_expression());
      57        3928 :   return v;
      58             : }
      59             : 
      60             : /// \brief Returns a data expression of type Real that corresponds to 'undefined'
      61             : inline
      62      266295 : const data::data_expression& undefined_real()
      63             : {
      64      266295 :   static data::variable r("@undefined_real", data::sort_real::real_());
      65      266295 :   return r;
      66             : }
      67             : 
      68             : } // namespace data
      69             : 
      70             : } // namespace mcrl2
      71             : 
      72             : #endif // MCRL2_DATA_UNDEFINED_H