Line data    Source code

       1             : // Author(s): Jeroen Keiren and Jan Friso Groote
       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/real_utilities.h
      10             : /// \brief Contains a number of auxiliary functions to recognize reals. 
      11             : 
      12             : 
      13             : #ifndef MCRL2_DATA_REAL_UTILITIES_H
      14             : #define MCRL2_DATA_REAL_UTILITIES_H
      15             : 
      16             : #include "mcrl2/data/standard_numbers_utility.h"
      17             : 
      18             : namespace mcrl2
      19             : {
      20             : namespace data
      21             : {
      22             : namespace sort_real
      23             : {
      24             : 
      25         664 : inline data_expression& real_zero()
      26             : {
      27         664 :   static data_expression real_zero=sort_real::real_("0");
      28         664 :   return real_zero;
      29             : }
      30             : 
      31          69 : inline data_expression& real_one()
      32             : {
      33          69 :   static data_expression real_one=sort_real::real_("1");
      34          69 :   return real_one;
      35             : }
      36             : 
      37          51 : inline bool is_zero(const atermpp::aterm& e)
      38             : {
      39          51 :   return (e==real_zero());
      40             : }
      41             : 
      42          34 : inline bool is_one(const atermpp::aterm& e)
      43             : {
      44          34 :   return (e==real_one());
      45             : }
      46             : 
      47             : /// \brief Functions that returns true if e is a closed real number larger than zero.
      48           7 : inline bool is_larger_zero(const atermpp::aterm_appl& e)
      49             : {
      50           7 :   if (sort_real::is_creal_application(e))
      51             :   { 
      52           7 :     const application& ea=atermpp::down_cast<application>(e);
      53           7 :     return sort_int::is_cint_application(ea[0]) && 
      54          14 :            sort_nat::is_natural_constant(atermpp::down_cast<application>(ea[0])[0]) && 
      55          14 :            e!=real_zero();
      56             :   }
      57           0 :   return false;
      58             : }
      59             : 
      60             : 
      61             : } // namespace real
      62             : } // namespace data
      63             : 
      64             : } // namespace mcrl2
      65             : 
      66             : #endif // MCRL2_DATA_REAL_UTILITIES_H
      67             : 
      68             :