real64.h

Go to the documentation of this file.

// Author(s): Jeroen Keiren
// Copyright: see the accompanying file COPYING or copy at
// https://github.com/mCRL2org/mCRL2/blob/master/COPYING
//
// Distributed under the Boost Software License, Version 1.0.
// (See accompanying file LICENSE_1_0.txt or copy at
// http://www.boost.org/LICENSE_1_0.txt)
//
 
#ifndef MCRL2_DATA_REAL64_H
#define MCRL2_DATA_REAL64_H
 
#include "functional"    // std::function
#include "mcrl2/utilities/exception.h"
#include "mcrl2/data/basic_sort.h"
#include "mcrl2/data/function_sort.h"
#include "mcrl2/data/function_symbol.h"
#include "mcrl2/data/application.h"
#include "mcrl2/data/data_equation.h"
#include "mcrl2/data/standard.h"
#include "mcrl2/data/bool.h"
#include "mcrl2/data/pos64.h"
#include "mcrl2/data/nat64.h"
#include "mcrl2/data/int64.h"
 
namespace mcrl2 {
 
  namespace data {
 
    namespace sort_real {
 
      inline
      const core::identifier_string& real_name()
      {
        static core::identifier_string real_name = core::identifier_string("Real");
        return real_name;
      }
 
      inline
      const basic_sort& real_()
      {
        static basic_sort real_ = basic_sort(real_name());
        return real_;
      }
 
      inline
      bool is_real(const sort_expression& e)
      {
        if (is_basic_sort(e))
        {
          return basic_sort(e) == real_();
        }
        return false;
      }
 
      inline
      function_symbol_vector real_generate_constructors_code()
      {
        function_symbol_vector result;
        return result;
      }
      inline
      function_symbol_vector real_mCRL2_usable_constructors()
      {
        function_symbol_vector result;
        return result;
      }
      // The typedef is the sort that maps a function symbol to an function that rewrites it as well as a string of a function that can be used to implement it
      typedef std::map<function_symbol,std::pair<std::function<void(data_expression&, const data_expression&)>, std::string> > implementation_map;
      inline
      implementation_map real_cpp_implementable_constructors()
      {
        implementation_map result;
        return result;
      }
 
      inline
      const core::identifier_string& creal_name()
      {
        static core::identifier_string creal_name = core::identifier_string("@cReal");
        return creal_name;
      }
 
      
      inline
      const function_symbol& creal()
      {
        static function_symbol creal(creal_name(), make_function_sort_(sort_int::int_(), sort_pos::pos(), real_()));
        return creal;
      }
 
      inline
      bool is_creal_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == creal();
        }
        return false;
      }
 
      
      inline
      application creal(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_real::creal()(arg0, arg1);
      }
 
      
      inline
      void make_creal(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_real::creal(),arg0, arg1);
      }
 
      inline
      bool is_creal_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_creal_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& pos2real_name()
      {
        static core::identifier_string pos2real_name = core::identifier_string("Pos2Real");
        return pos2real_name;
      }
 
      
      inline
      const function_symbol& pos2real()
      {
        static function_symbol pos2real(pos2real_name(), make_function_sort_(sort_pos::pos(), real_()));
        return pos2real;
      }
 
      inline
      bool is_pos2real_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == pos2real();
        }
        return false;
      }
 
      
      inline
      application pos2real(const data_expression& arg0)
      {
        return sort_real::pos2real()(arg0);
      }
 
      
      inline
      void make_pos2real(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_real::pos2real(),arg0);
      }
 
      inline
      bool is_pos2real_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_pos2real_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& nat2real_name()
      {
        static core::identifier_string nat2real_name = core::identifier_string("Nat2Real");
        return nat2real_name;
      }
 
      
      inline
      const function_symbol& nat2real()
      {
        static function_symbol nat2real(nat2real_name(), make_function_sort_(sort_nat::nat(), real_()));
        return nat2real;
      }
 
      inline
      bool is_nat2real_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == nat2real();
        }
        return false;
      }
 
      
      inline
      application nat2real(const data_expression& arg0)
      {
        return sort_real::nat2real()(arg0);
      }
 
      
      inline
      void make_nat2real(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_real::nat2real(),arg0);
      }
 
      inline
      bool is_nat2real_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_nat2real_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& int2real_name()
      {
        static core::identifier_string int2real_name = core::identifier_string("Int2Real");
        return int2real_name;
      }
 
      
      inline
      const function_symbol& int2real()
      {
        static function_symbol int2real(int2real_name(), make_function_sort_(sort_int::int_(), real_()));
        return int2real;
      }
 
      inline
      bool is_int2real_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == int2real();
        }
        return false;
      }
 
      
      inline
      application int2real(const data_expression& arg0)
      {
        return sort_real::int2real()(arg0);
      }
 
      
      inline
      void make_int2real(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_real::int2real(),arg0);
      }
 
      inline
      bool is_int2real_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_int2real_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& real2pos_name()
      {
        static core::identifier_string real2pos_name = core::identifier_string("Real2Pos");
        return real2pos_name;
      }
 
      
      inline
      const function_symbol& real2pos()
      {
        static function_symbol real2pos(real2pos_name(), make_function_sort_(real_(), sort_pos::pos()));
        return real2pos;
      }
 
      inline
      bool is_real2pos_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == real2pos();
        }
        return false;
      }
 
      
      inline
      application real2pos(const data_expression& arg0)
      {
        return sort_real::real2pos()(arg0);
      }
 
      
      inline
      void make_real2pos(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_real::real2pos(),arg0);
      }
 
      inline
      bool is_real2pos_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_real2pos_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& real2nat_name()
      {
        static core::identifier_string real2nat_name = core::identifier_string("Real2Nat");
        return real2nat_name;
      }
 
      
      inline
      const function_symbol& real2nat()
      {
        static function_symbol real2nat(real2nat_name(), make_function_sort_(real_(), sort_nat::nat()));
        return real2nat;
      }
 
      inline
      bool is_real2nat_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == real2nat();
        }
        return false;
      }
 
      
      inline
      application real2nat(const data_expression& arg0)
      {
        return sort_real::real2nat()(arg0);
      }
 
      
      inline
      void make_real2nat(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_real::real2nat(),arg0);
      }
 
      inline
      bool is_real2nat_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_real2nat_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& real2int_name()
      {
        static core::identifier_string real2int_name = core::identifier_string("Real2Int");
        return real2int_name;
      }
 
      
      inline
      const function_symbol& real2int()
      {
        static function_symbol real2int(real2int_name(), make_function_sort_(real_(), sort_int::int_()));
        return real2int;
      }
 
      inline
      bool is_real2int_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == real2int();
        }
        return false;
      }
 
      
      inline
      application real2int(const data_expression& arg0)
      {
        return sort_real::real2int()(arg0);
      }
 
      
      inline
      void make_real2int(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_real::real2int(),arg0);
      }
 
      inline
      bool is_real2int_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_real2int_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& maximum_name()
      {
        static core::identifier_string maximum_name = core::identifier_string("max");
        return maximum_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol maximum(const sort_expression& s0, const sort_expression& s1)
      {
        sort_expression target_sort;
        if (s0 == real_() && s1 == real_())
        {
          target_sort = real_();
        }
        else if (s0 == sort_pos::pos() && s1 == sort_int::int_())
        {
          target_sort = sort_pos::pos();
        }
        else if (s0 == sort_int::int_() && s1 == sort_pos::pos())
        {
          target_sort = sort_pos::pos();
        }
        else if (s0 == sort_nat::nat() && s1 == sort_int::int_())
        {
          target_sort = sort_nat::nat();
        }
        else if (s0 == sort_int::int_() && s1 == sort_nat::nat())
        {
          target_sort = sort_nat::nat();
        }
        else if (s0 == sort_int::int_() && s1 == sort_int::int_())
        {
          target_sort = sort_int::int_();
        }
        else if (s0 == sort_pos::pos() && s1 == sort_nat::nat())
        {
          target_sort = sort_pos::pos();
        }
        else if (s0 == sort_nat::nat() && s1 == sort_pos::pos())
        {
          target_sort = sort_pos::pos();
        }
        else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
        {
          target_sort = sort_nat::nat();
        }
        else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
        {
          target_sort = sort_pos::pos();
        }
        else
        {
          throw mcrl2::runtime_error("Cannot compute target sort for maximum with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
        }
 
        function_symbol maximum(maximum_name(), make_function_sort_(s0, s1, target_sort));
        return maximum;
      }
 
      inline
      bool is_maximum_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == maximum_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == maximum(real_(), real_()) || f == maximum(sort_pos::pos(), sort_int::int_()) || f == maximum(sort_int::int_(), sort_pos::pos()) || f == maximum(sort_nat::nat(), sort_int::int_()) || f == maximum(sort_int::int_(), sort_nat::nat()) || f == maximum(sort_int::int_(), sort_int::int_()) || f == maximum(sort_pos::pos(), sort_nat::nat()) || f == maximum(sort_nat::nat(), sort_pos::pos()) || f == maximum(sort_nat::nat(), sort_nat::nat()) || f == maximum(sort_pos::pos(), sort_pos::pos()));
        }
        return false;
      }
 
      
      inline
      application maximum(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_real::maximum(arg0.sort(), arg1.sort())(arg0, arg1);
      }
 
      
      inline
      void make_maximum(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_real::maximum(arg0.sort(), arg1.sort()),arg0, arg1);
      }
 
      inline
      bool is_maximum_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_maximum_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& minimum_name()
      {
        static core::identifier_string minimum_name = core::identifier_string("min");
        return minimum_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol minimum(const sort_expression& s0, const sort_expression& s1)
      {
        sort_expression target_sort;
        if (s0 == real_() && s1 == real_())
        {
          target_sort = real_();
        }
        else if (s0 == sort_int::int_() && s1 == sort_int::int_())
        {
          target_sort = sort_int::int_();
        }
        else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
        {
          target_sort = sort_nat::nat();
        }
        else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
        {
          target_sort = sort_pos::pos();
        }
        else
        {
          throw mcrl2::runtime_error("Cannot compute target sort for minimum with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
        }
 
        function_symbol minimum(minimum_name(), make_function_sort_(s0, s1, target_sort));
        return minimum;
      }
 
      inline
      bool is_minimum_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == minimum_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == minimum(real_(), real_()) || f == minimum(sort_int::int_(), sort_int::int_()) || f == minimum(sort_nat::nat(), sort_nat::nat()) || f == minimum(sort_pos::pos(), sort_pos::pos()));
        }
        return false;
      }
 
      
      inline
      application minimum(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_real::minimum(arg0.sort(), arg1.sort())(arg0, arg1);
      }
 
      
      inline
      void make_minimum(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_real::minimum(arg0.sort(), arg1.sort()),arg0, arg1);
      }
 
      inline
      bool is_minimum_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_minimum_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& abs_name()
      {
        static core::identifier_string abs_name = core::identifier_string("abs");
        return abs_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol abs(const sort_expression& s0)
      {
        sort_expression target_sort;
        if (s0 == real_())
        {
          target_sort = real_();
        }
        else if (s0 == sort_int::int_())
        {
          target_sort = sort_nat::nat();
        }
        else
        {
          throw mcrl2::runtime_error("Cannot compute target sort for abs with domain sorts " + pp(s0) + ". ");
        }
 
        function_symbol abs(abs_name(), make_function_sort_(s0, target_sort));
        return abs;
      }
 
      inline
      bool is_abs_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == abs_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 1 && (f == abs(real_()) || f == abs(sort_int::int_()));
        }
        return false;
      }
 
      
      inline
      application abs(const data_expression& arg0)
      {
        return sort_real::abs(arg0.sort())(arg0);
      }
 
      
      inline
      void make_abs(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_real::abs(arg0.sort()),arg0);
      }
 
      inline
      bool is_abs_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_abs_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& negate_name()
      {
        static core::identifier_string negate_name = core::identifier_string("-");
        return negate_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol negate(const sort_expression& s0)
      {
        sort_expression target_sort;
        if (s0 == real_())
        {
          target_sort = real_();
        }
        else if (s0 == sort_pos::pos())
        {
          target_sort = sort_int::int_();
        }
        else if (s0 == sort_nat::nat())
        {
          target_sort = sort_int::int_();
        }
        else if (s0 == sort_int::int_())
        {
          target_sort = sort_int::int_();
        }
        else
        {
          throw mcrl2::runtime_error("Cannot compute target sort for negate with domain sorts " + pp(s0) + ". ");
        }
 
        function_symbol negate(negate_name(), make_function_sort_(s0, target_sort));
        return negate;
      }
 
      inline
      bool is_negate_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == negate_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 1 && (f == negate(real_()) || f == negate(sort_pos::pos()) || f == negate(sort_nat::nat()) || f == negate(sort_int::int_()));
        }
        return false;
      }
 
      
      inline
      application negate(const data_expression& arg0)
      {
        return sort_real::negate(arg0.sort())(arg0);
      }
 
      
      inline
      void make_negate(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_real::negate(arg0.sort()),arg0);
      }
 
      inline
      bool is_negate_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_negate_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& succ_name()
      {
        static core::identifier_string succ_name = core::identifier_string("succ");
        return succ_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol succ(const sort_expression& s0)
      {
        sort_expression target_sort;
        if (s0 == real_())
        {
          target_sort = real_();
        }
        else if (s0 == sort_int::int_())
        {
          target_sort = sort_int::int_();
        }
        else if (s0 == sort_nat::nat())
        {
          target_sort = sort_pos::pos();
        }
        else if (s0 == sort_pos::pos())
        {
          target_sort = sort_pos::pos();
        }
        else
        {
          throw mcrl2::runtime_error("Cannot compute target sort for succ with domain sorts " + pp(s0) + ". ");
        }
 
        function_symbol succ(succ_name(), make_function_sort_(s0, target_sort));
        return succ;
      }
 
      inline
      bool is_succ_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == succ_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 1 && (f == succ(real_()) || f == succ(sort_int::int_()) || f == succ(sort_nat::nat()) || f == succ(sort_pos::pos()));
        }
        return false;
      }
 
      
      inline
      application succ(const data_expression& arg0)
      {
        return sort_real::succ(arg0.sort())(arg0);
      }
 
      
      inline
      void make_succ(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_real::succ(arg0.sort()),arg0);
      }
 
      inline
      bool is_succ_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_succ_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& pred_name()
      {
        static core::identifier_string pred_name = core::identifier_string("pred");
        return pred_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol pred(const sort_expression& s0)
      {
        sort_expression target_sort;
        if (s0 == real_())
        {
          target_sort = real_();
        }
        else if (s0 == sort_nat::nat())
        {
          target_sort = sort_int::int_();
        }
        else if (s0 == sort_int::int_())
        {
          target_sort = sort_int::int_();
        }
        else if (s0 == sort_pos::pos())
        {
          target_sort = sort_nat::nat();
        }
        else
        {
          throw mcrl2::runtime_error("Cannot compute target sort for pred with domain sorts " + pp(s0) + ". ");
        }
 
        function_symbol pred(pred_name(), make_function_sort_(s0, target_sort));
        return pred;
      }
 
      inline
      bool is_pred_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == pred_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 1 && (f == pred(real_()) || f == pred(sort_nat::nat()) || f == pred(sort_int::int_()) || f == pred(sort_pos::pos()));
        }
        return false;
      }
 
      
      inline
      application pred(const data_expression& arg0)
      {
        return sort_real::pred(arg0.sort())(arg0);
      }
 
      
      inline
      void make_pred(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_real::pred(arg0.sort()),arg0);
      }
 
      inline
      bool is_pred_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_pred_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& plus_name()
      {
        static core::identifier_string plus_name = core::identifier_string("+");
        return plus_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol plus(const sort_expression& s0, const sort_expression& s1)
      {
        sort_expression target_sort;
        if (s0 == real_() && s1 == real_())
        {
          target_sort = real_();
        }
        else if (s0 == sort_int::int_() && s1 == sort_int::int_())
        {
          target_sort = sort_int::int_();
        }
        else if (s0 == sort_pos::pos() && s1 == sort_nat::nat())
        {
          target_sort = sort_pos::pos();
        }
        else if (s0 == sort_nat::nat() && s1 == sort_pos::pos())
        {
          target_sort = sort_pos::pos();
        }
        else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
        {
          target_sort = sort_nat::nat();
        }
        else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
        {
          target_sort = sort_pos::pos();
        }
        else
        {
          throw mcrl2::runtime_error("Cannot compute target sort for plus with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
        }
 
        function_symbol plus(plus_name(), make_function_sort_(s0, s1, target_sort));
        return plus;
      }
 
      inline
      bool is_plus_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == plus_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == plus(real_(), real_()) || f == plus(sort_int::int_(), sort_int::int_()) || f == plus(sort_pos::pos(), sort_nat::nat()) || f == plus(sort_nat::nat(), sort_pos::pos()) || f == plus(sort_nat::nat(), sort_nat::nat()) || f == plus(sort_pos::pos(), sort_pos::pos()));
        }
        return false;
      }
 
      
      inline
      application plus(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_real::plus(arg0.sort(), arg1.sort())(arg0, arg1);
      }
 
      
      inline
      void make_plus(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_real::plus(arg0.sort(), arg1.sort()),arg0, arg1);
      }
 
      inline
      bool is_plus_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_plus_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& minus_name()
      {
        static core::identifier_string minus_name = core::identifier_string("-");
        return minus_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol minus(const sort_expression& s0, const sort_expression& s1)
      {
        sort_expression target_sort;
        if (s0 == real_() && s1 == real_())
        {
          target_sort = real_();
        }
        else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
        {
          target_sort = sort_int::int_();
        }
        else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
        {
          target_sort = sort_int::int_();
        }
        else if (s0 == sort_int::int_() && s1 == sort_int::int_())
        {
          target_sort = sort_int::int_();
        }
        else
        {
          throw mcrl2::runtime_error("Cannot compute target sort for minus with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
        }
 
        function_symbol minus(minus_name(), make_function_sort_(s0, s1, target_sort));
        return minus;
      }
 
      inline
      bool is_minus_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == minus_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == minus(real_(), real_()) || f == minus(sort_pos::pos(), sort_pos::pos()) || f == minus(sort_nat::nat(), sort_nat::nat()) || f == minus(sort_int::int_(), sort_int::int_()));
        }
        return false;
      }
 
      
      inline
      application minus(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_real::minus(arg0.sort(), arg1.sort())(arg0, arg1);
      }
 
      
      inline
      void make_minus(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_real::minus(arg0.sort(), arg1.sort()),arg0, arg1);
      }
 
      inline
      bool is_minus_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_minus_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& times_name()
      {
        static core::identifier_string times_name = core::identifier_string("*");
        return times_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol times(const sort_expression& s0, const sort_expression& s1)
      {
        sort_expression target_sort;
        if (s0 == real_() && s1 == real_())
        {
          target_sort = real_();
        }
        else if (s0 == sort_int::int_() && s1 == sort_int::int_())
        {
          target_sort = sort_int::int_();
        }
        else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
        {
          target_sort = sort_nat::nat();
        }
        else if (s0 == sort_pos::pos() && s1 == sort_pos::pos())
        {
          target_sort = sort_pos::pos();
        }
        else
        {
          throw mcrl2::runtime_error("Cannot compute target sort for times with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
        }
 
        function_symbol times(times_name(), make_function_sort_(s0, s1, target_sort));
        return times;
      }
 
      inline
      bool is_times_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == times_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == times(real_(), real_()) || f == times(sort_int::int_(), sort_int::int_()) || f == times(sort_nat::nat(), sort_nat::nat()) || f == times(sort_pos::pos(), sort_pos::pos()));
        }
        return false;
      }
 
      
      inline
      application times(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_real::times(arg0.sort(), arg1.sort())(arg0, arg1);
      }
 
      
      inline
      void make_times(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_real::times(arg0.sort(), arg1.sort()),arg0, arg1);
      }
 
      inline
      bool is_times_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_times_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& exp_name()
      {
        static core::identifier_string exp_name = core::identifier_string("exp");
        return exp_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol exp(const sort_expression& s0, const sort_expression& s1)
      {
        sort_expression target_sort;
        if (s0 == real_() && s1 == sort_int::int_())
        {
          target_sort = real_();
        }
        else if (s0 == sort_int::int_() && s1 == sort_nat::nat())
        {
          target_sort = sort_int::int_();
        }
        else if (s0 == sort_pos::pos() && s1 == sort_nat::nat())
        {
          target_sort = sort_pos::pos();
        }
        else if (s0 == sort_nat::nat() && s1 == sort_nat::nat())
        {
          target_sort = sort_nat::nat();
        }
        else
        {
          throw mcrl2::runtime_error("Cannot compute target sort for exp with domain sorts " + pp(s0) + ", " + pp(s1) + ". ");
        }
 
        function_symbol exp(exp_name(), make_function_sort_(s0, s1, target_sort));
        return exp;
      }
 
      inline
      bool is_exp_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == exp_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == exp(real_(), sort_int::int_()) || f == exp(sort_int::int_(), sort_nat::nat()) || f == exp(sort_pos::pos(), sort_nat::nat()) || f == exp(sort_nat::nat(), sort_nat::nat()));
        }
        return false;
      }
 
      
      inline
      application exp(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_real::exp(arg0.sort(), arg1.sort())(arg0, arg1);
      }
 
      
      inline
      void make_exp(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_real::exp(arg0.sort(), arg1.sort()),arg0, arg1);
      }
 
      inline
      bool is_exp_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_exp_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& divides_name()
      {
        static core::identifier_string divides_name = core::identifier_string("/");
        return divides_name;
      }
 
      // This function is not intended for public use and therefore not documented in Doxygen.
      inline
      function_symbol divides(const sort_expression& s0, const sort_expression& s1)
      {
        sort_expression target_sort(real_());
        function_symbol divides(divides_name(), make_function_sort_(s0, s1, target_sort));
        return divides;
      }
 
      inline
      bool is_divides_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          const function_symbol& f = atermpp::down_cast<function_symbol>(e);
          return f.name() == divides_name() && atermpp::down_cast<function_sort>(f.sort()).domain().size() == 2 && (f == divides(sort_pos::pos(), sort_pos::pos()) || f == divides(sort_nat::nat(), sort_nat::nat()) || f == divides(sort_int::int_(), sort_int::int_()) || f == divides(real_(), real_()));
        }
        return false;
      }
 
      
      inline
      application divides(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_real::divides(arg0.sort(), arg1.sort())(arg0, arg1);
      }
 
      
      inline
      void make_divides(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_real::divides(arg0.sort(), arg1.sort()),arg0, arg1);
      }
 
      inline
      bool is_divides_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_divides_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& floor_name()
      {
        static core::identifier_string floor_name = core::identifier_string("floor");
        return floor_name;
      }
 
      
      inline
      const function_symbol& floor()
      {
        static function_symbol floor(floor_name(), make_function_sort_(real_(), sort_int::int_()));
        return floor;
      }
 
      inline
      bool is_floor_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == floor();
        }
        return false;
      }
 
      
      inline
      application floor(const data_expression& arg0)
      {
        return sort_real::floor()(arg0);
      }
 
      
      inline
      void make_floor(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_real::floor(),arg0);
      }
 
      inline
      bool is_floor_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_floor_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& ceil_name()
      {
        static core::identifier_string ceil_name = core::identifier_string("ceil");
        return ceil_name;
      }
 
      
      inline
      const function_symbol& ceil()
      {
        static function_symbol ceil(ceil_name(), make_function_sort_(real_(), sort_int::int_()));
        return ceil;
      }
 
      inline
      bool is_ceil_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == ceil();
        }
        return false;
      }
 
      
      inline
      application ceil(const data_expression& arg0)
      {
        return sort_real::ceil()(arg0);
      }
 
      
      inline
      void make_ceil(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_real::ceil(),arg0);
      }
 
      inline
      bool is_ceil_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_ceil_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& round_name()
      {
        static core::identifier_string round_name = core::identifier_string("round");
        return round_name;
      }
 
      
      inline
      const function_symbol& round()
      {
        static function_symbol round(round_name(), make_function_sort_(real_(), sort_int::int_()));
        return round;
      }
 
      inline
      bool is_round_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == round();
        }
        return false;
      }
 
      
      inline
      application round(const data_expression& arg0)
      {
        return sort_real::round()(arg0);
      }
 
      
      inline
      void make_round(data_expression& result, const data_expression& arg0)
      {
        make_application(result, sort_real::round(),arg0);
      }
 
      inline
      bool is_round_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_round_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& reduce_fraction_name()
      {
        static core::identifier_string reduce_fraction_name = core::identifier_string("@redfrac");
        return reduce_fraction_name;
      }
 
      
      inline
      const function_symbol& reduce_fraction()
      {
        static function_symbol reduce_fraction(reduce_fraction_name(), make_function_sort_(sort_int::int_(), sort_int::int_(), real_()));
        return reduce_fraction;
      }
 
      inline
      bool is_reduce_fraction_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == reduce_fraction();
        }
        return false;
      }
 
      
      inline
      application reduce_fraction(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_real::reduce_fraction()(arg0, arg1);
      }
 
      
      inline
      void make_reduce_fraction(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_real::reduce_fraction(),arg0, arg1);
      }
 
      inline
      bool is_reduce_fraction_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_reduce_fraction_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& reduce_fraction_where_name()
      {
        static core::identifier_string reduce_fraction_where_name = core::identifier_string("@redfracwhr");
        return reduce_fraction_where_name;
      }
 
      
      inline
      const function_symbol& reduce_fraction_where()
      {
        static function_symbol reduce_fraction_where(reduce_fraction_where_name(), make_function_sort_(sort_nat::nat(), sort_int::int_(), sort_nat::nat(), real_()));
        return reduce_fraction_where;
      }
 
      inline
      bool is_reduce_fraction_where_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == reduce_fraction_where();
        }
        return false;
      }
 
      
      inline
      application reduce_fraction_where(const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        return sort_real::reduce_fraction_where()(arg0, arg1, arg2);
      }
 
      
      inline
      void make_reduce_fraction_where(data_expression& result, const data_expression& arg0, const data_expression& arg1, const data_expression& arg2)
      {
        make_application(result, sort_real::reduce_fraction_where(),arg0, arg1, arg2);
      }
 
      inline
      bool is_reduce_fraction_where_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_reduce_fraction_where_function_symbol(atermpp::down_cast<application>(e).head());
      }
 
      inline
      const core::identifier_string& reduce_fraction_helper_name()
      {
        static core::identifier_string reduce_fraction_helper_name = core::identifier_string("@redfrachlp");
        return reduce_fraction_helper_name;
      }
 
      
      inline
      const function_symbol& reduce_fraction_helper()
      {
        static function_symbol reduce_fraction_helper(reduce_fraction_helper_name(), make_function_sort_(real_(), sort_int::int_(), real_()));
        return reduce_fraction_helper;
      }
 
      inline
      bool is_reduce_fraction_helper_function_symbol(const atermpp::aterm& e)
      {
        if (is_function_symbol(e))
        {
          return atermpp::down_cast<function_symbol>(e) == reduce_fraction_helper();
        }
        return false;
      }
 
      
      inline
      application reduce_fraction_helper(const data_expression& arg0, const data_expression& arg1)
      {
        return sort_real::reduce_fraction_helper()(arg0, arg1);
      }
 
      
      inline
      void make_reduce_fraction_helper(data_expression& result, const data_expression& arg0, const data_expression& arg1)
      {
        make_application(result, sort_real::reduce_fraction_helper(),arg0, arg1);
      }
 
      inline
      bool is_reduce_fraction_helper_application(const atermpp::aterm& e)
      {
        return is_application(e) && is_reduce_fraction_helper_function_symbol(atermpp::down_cast<application>(e).head());
      }
      inline
      function_symbol_vector real_generate_functions_code()
      {
        function_symbol_vector result;
        result.push_back(sort_real::creal());
        result.push_back(sort_real::pos2real());
        result.push_back(sort_real::nat2real());
        result.push_back(sort_real::int2real());
        result.push_back(sort_real::real2pos());
        result.push_back(sort_real::real2nat());
        result.push_back(sort_real::real2int());
        result.push_back(sort_real::maximum(real_(), real_()));
        result.push_back(sort_real::minimum(real_(), real_()));
        result.push_back(sort_real::abs(real_()));
        result.push_back(sort_real::negate(real_()));
        result.push_back(sort_real::succ(real_()));
        result.push_back(sort_real::pred(real_()));
        result.push_back(sort_real::plus(real_(), real_()));
        result.push_back(sort_real::minus(real_(), real_()));
        result.push_back(sort_real::times(real_(), real_()));
        result.push_back(sort_real::exp(real_(), sort_int::int_()));
        result.push_back(sort_real::divides(sort_pos::pos(), sort_pos::pos()));
        result.push_back(sort_real::divides(sort_nat::nat(), sort_nat::nat()));
        result.push_back(sort_real::divides(sort_int::int_(), sort_int::int_()));
        result.push_back(sort_real::divides(real_(), real_()));
        result.push_back(sort_real::floor());
        result.push_back(sort_real::ceil());
        result.push_back(sort_real::round());
        result.push_back(sort_real::reduce_fraction());
        result.push_back(sort_real::reduce_fraction_where());
        result.push_back(sort_real::reduce_fraction_helper());
        return result;
      }
      
      inline
      function_symbol_vector real_generate_constructors_and_functions_code()
      {
        function_symbol_vector result=real_generate_functions_code();
        for(const function_symbol& f: real_generate_constructors_code())
        {
          result.push_back(f);
        }
        return result;
      }
      
      inline
      function_symbol_vector real_mCRL2_usable_mappings()
      {
        function_symbol_vector result;
        result.push_back(sort_real::creal());
        result.push_back(sort_real::pos2real());
        result.push_back(sort_real::nat2real());
        result.push_back(sort_real::int2real());
        result.push_back(sort_real::real2pos());
        result.push_back(sort_real::real2nat());
        result.push_back(sort_real::real2int());
        result.push_back(sort_real::maximum(real_(), real_()));
        result.push_back(sort_real::minimum(real_(), real_()));
        result.push_back(sort_real::abs(real_()));
        result.push_back(sort_real::negate(real_()));
        result.push_back(sort_real::succ(real_()));
        result.push_back(sort_real::pred(real_()));
        result.push_back(sort_real::plus(real_(), real_()));
        result.push_back(sort_real::minus(real_(), real_()));
        result.push_back(sort_real::times(real_(), real_()));
        result.push_back(sort_real::exp(real_(), sort_int::int_()));
        result.push_back(sort_real::divides(sort_pos::pos(), sort_pos::pos()));
        result.push_back(sort_real::divides(sort_nat::nat(), sort_nat::nat()));
        result.push_back(sort_real::divides(sort_int::int_(), sort_int::int_()));
        result.push_back(sort_real::divides(real_(), real_()));
        result.push_back(sort_real::floor());
        result.push_back(sort_real::ceil());
        result.push_back(sort_real::round());
        result.push_back(sort_real::reduce_fraction());
        result.push_back(sort_real::reduce_fraction_where());
        result.push_back(sort_real::reduce_fraction_helper());
        return result;
      }
 
 
      // The typedef is the sort that maps a function symbol to an function that rewrites it as well as a string of a function that can be used to implement it
      typedef std::map<function_symbol,std::pair<std::function<void(data_expression&, const data_expression&)>, std::string> > implementation_map;
      inline
      implementation_map real_cpp_implementable_mappings()
      {
        implementation_map result;
        return result;
      }
      inline
      const data_expression& left(const data_expression& e)
      {
        assert(is_creal_application(e) || is_maximum_application(e) || is_minimum_application(e) || is_plus_application(e) || is_minus_application(e) || is_times_application(e) || is_exp_application(e) || is_divides_application(e) || is_reduce_fraction_application(e) || is_reduce_fraction_helper_application(e));
        return atermpp::down_cast<application>(e)[0];
      }
 
      inline
      const data_expression& right(const data_expression& e)
      {
        assert(is_creal_application(e) || is_maximum_application(e) || is_minimum_application(e) || is_plus_application(e) || is_minus_application(e) || is_times_application(e) || is_exp_application(e) || is_divides_application(e) || is_reduce_fraction_application(e) || is_reduce_fraction_helper_application(e));
        return atermpp::down_cast<application>(e)[1];
      }
 
      inline
      const data_expression& arg(const data_expression& e)
      {
        assert(is_pos2real_application(e) || is_nat2real_application(e) || is_int2real_application(e) || is_real2pos_application(e) || is_real2nat_application(e) || is_real2int_application(e) || is_abs_application(e) || is_negate_application(e) || is_succ_application(e) || is_pred_application(e) || is_floor_application(e) || is_ceil_application(e) || is_round_application(e));
        return atermpp::down_cast<application>(e)[0];
      }
 
      inline
      const data_expression& arg1(const data_expression& e)
      {
        assert(is_reduce_fraction_where_application(e));
        return atermpp::down_cast<application>(e)[0];
      }
 
      inline
      const data_expression& arg2(const data_expression& e)
      {
        assert(is_reduce_fraction_where_application(e));
        return atermpp::down_cast<application>(e)[1];
      }
 
      inline
      const data_expression& arg3(const data_expression& e)
      {
        assert(is_reduce_fraction_where_application(e));
        return atermpp::down_cast<application>(e)[2];
      }
 
      inline
      data_equation_vector real_generate_equations_code()
      {
        variable vm("m",sort_nat::nat());
        variable vn("n",sort_nat::nat());
        variable vp("p",sort_pos::pos());
        variable vq("q",sort_pos::pos());
        variable vx("x",sort_int::int_());
        variable vy("y",sort_int::int_());
        variable vr("r",real_());
        variable vs("s",real_());
 
        data_equation_vector result;
        result.push_back(data_equation(variable_list({vp, vq, vx, vy}), equal_to(creal(vx, vp), creal(vy, vq)), equal_to(times(vx, sort_int::cint(sort_nat::pos2nat(vq))), times(vy, sort_int::cint(sort_nat::pos2nat(vp))))));
        result.push_back(data_equation(variable_list({vp, vq, vx, vy}), less(creal(vx, vp), creal(vy, vq)), less(times(vx, sort_int::cint(sort_nat::pos2nat(vq))), times(vy, sort_int::cint(sort_nat::pos2nat(vp))))));
        result.push_back(data_equation(variable_list({vp, vq, vx, vy}), less_equal(creal(vx, vp), creal(vy, vq)), less_equal(times(vx, sort_int::cint(sort_nat::pos2nat(vq))), times(vy, sort_int::cint(sort_nat::pos2nat(vp))))));
        result.push_back(data_equation(variable_list({vx}), int2real(vx), creal(vx, sort_pos::c1())));
        result.push_back(data_equation(variable_list({vn}), nat2real(vn), creal(sort_int::cint(vn), sort_pos::c1())));
        result.push_back(data_equation(variable_list({vp}), pos2real(vp), creal(sort_int::cint(sort_nat::pos2nat(vp)), sort_pos::c1())));
        result.push_back(data_equation(variable_list({vp, vx}), equal_to(vp, sort_pos::c1()), real2int(creal(vx, vp)), vx));
        result.push_back(data_equation(variable_list({vp, vx}), equal_to(vp, sort_pos::c1()), real2nat(creal(vx, vp)), sort_int::int2nat(vx)));
        result.push_back(data_equation(variable_list({vp, vx}), equal_to(vp, sort_pos::c1()), real2pos(creal(vx, vp)), sort_int::int2pos(vx)));
        result.push_back(data_equation(variable_list({vr, vs}), minimum(vr, vs), if_(less(vr, vs), vr, vs)));
        result.push_back(data_equation(variable_list({vr, vs}), maximum(vr, vs), if_(less(vr, vs), vs, vr)));
        result.push_back(data_equation(variable_list({vr}), abs(vr), if_(less(vr, creal(sort_int::cint(sort_nat::c0()), sort_pos::c1())), negate(vr), vr)));
        result.push_back(data_equation(variable_list({vp, vx}), negate(creal(vx, vp)), creal(negate(vx), vp)));
        result.push_back(data_equation(variable_list({vp, vx}), succ(creal(vx, vp)), creal(plus(vx, sort_int::cint(sort_nat::pos2nat(vp))), vp)));
        result.push_back(data_equation(variable_list({vp, vx}), pred(creal(vx, vp)), creal(minus(vx, sort_int::cint(sort_nat::pos2nat(vp))), vp)));
        result.push_back(data_equation(variable_list({vp, vq, vx, vy}), plus(creal(vx, vp), creal(vy, vq)), reduce_fraction(plus(times(vx, sort_int::cint(sort_nat::pos2nat(vq))), times(vy, sort_int::cint(sort_nat::pos2nat(vp)))), sort_int::cint(sort_nat::pos2nat(times(vp, vq))))));
        result.push_back(data_equation(variable_list({vp, vq, vx, vy}), minus(creal(vx, vp), creal(vy, vq)), reduce_fraction(minus(times(vx, sort_int::cint(sort_nat::pos2nat(vq))), times(vy, sort_int::cint(sort_nat::pos2nat(vp)))), sort_int::cint(sort_nat::pos2nat(times(vp, vq))))));
        result.push_back(data_equation(variable_list({vp, vq, vx, vy}), times(creal(vx, vp), creal(vy, vq)), reduce_fraction(times(vx, vy), sort_int::cint(sort_nat::pos2nat(times(vp, vq))))));
        result.push_back(data_equation(variable_list({vm, vp, vr}), sort_nat::equals_zero(vm), times(vr, creal(sort_int::cint(vm), vp)), creal(sort_int::cint(sort_nat::c0()), sort_pos::c1())));
        result.push_back(data_equation(variable_list({vm, vp, vr}), sort_nat::equals_zero(vm), times(creal(sort_int::cint(vm), vp), vr), creal(sort_int::cint(sort_nat::c0()), sort_pos::c1())));
        result.push_back(data_equation(variable_list({vp, vq, vx, vy}), not_equal_to(vy, sort_int::cint(sort_nat::c0())), divides(creal(vx, vp), creal(vy, vq)), reduce_fraction(times(vx, sort_int::cint(sort_nat::pos2nat(vq))), times(vy, sort_int::cint(sort_nat::pos2nat(vp))))));
        result.push_back(data_equation(variable_list({vp, vq}), divides(vp, vq), reduce_fraction(sort_int::cint(sort_nat::pos2nat(vp)), sort_int::cint(sort_nat::pos2nat(vq)))));
        result.push_back(data_equation(variable_list({vm, vn}), not_equal_to(vn, sort_nat::c0()), divides(vm, vn), reduce_fraction(sort_int::cint(vm), sort_int::cint(vn))));
        result.push_back(data_equation(variable_list({vx, vy}), not_equal_to(vy, sort_int::cint(sort_nat::c0())), divides(vx, vy), reduce_fraction(vx, vy)));
        result.push_back(data_equation(variable_list({vn, vp, vx}), exp(creal(vx, vp), sort_int::cint(vn)), reduce_fraction(exp(vx, vn), sort_int::cint(sort_nat::pos2nat(exp(vp, vn))))));
        result.push_back(data_equation(variable_list({vp, vq, vx}), not_equal_to(vx, sort_int::cint(sort_nat::c0())), exp(creal(vx, vp), sort_int::cneg(vq)), reduce_fraction(sort_int::cint(sort_nat::pos2nat(exp(vp, sort_nat::pos2nat(vq)))), exp(vx, sort_nat::pos2nat(vq)))));
        result.push_back(data_equation(variable_list({vp, vx}), floor(creal(vx, vp)), sort_int::div(vx, vp)));
        result.push_back(data_equation(variable_list({vr}), ceil(vr), negate(floor(negate(vr)))));
        result.push_back(data_equation(variable_list({vr}), round(vr), floor(plus(vr, creal(sort_int::cint(sort_nat::pos2nat(sort_pos::c1())), plus(sort_pos::c1(), sort_pos::c1()))))));
        result.push_back(data_equation(variable_list({vp, vx}), reduce_fraction(vx, sort_int::cneg(vp)), reduce_fraction(negate(vx), sort_int::cint(sort_nat::pos2nat(vp)))));
        result.push_back(data_equation(variable_list({vn, vx}), reduce_fraction(vx, sort_int::cint(vn)), reduce_fraction_where(vn, sort_int::div(vx, sort_nat::nat2pos(vn)), sort_int::mod(vx, sort_nat::nat2pos(vn)))));
        result.push_back(data_equation(variable_list({vm, vn, vx}), sort_nat::equals_zero(vm), reduce_fraction_where(vn, vx, vm), creal(vx, sort_pos::c1())));
        result.push_back(data_equation(variable_list({vm, vn, vx}), sort_nat::not_equals_zero(vm), reduce_fraction_where(vn, vx, vm), reduce_fraction_helper(reduce_fraction(sort_int::cint(vn), sort_int::cint(vm)), vx)));
        result.push_back(data_equation(variable_list({vp, vx, vy}), reduce_fraction_helper(creal(vx, vp), vy), creal(plus(sort_int::cint(sort_nat::pos2nat(vp)), times(vy, vx)), sort_int::int2pos(vx))));
        return result;
      }
 
    } // namespace sort_real_
 
  } // namespace data
 
} // namespace mcrl2
 
#endif // MCRL2_DATA_REAL64_H