machine_word.h

Go to the documentation of this file.

// Author(s): Jan Friso Groote
// 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_DETAIL_MACHINE_WORD_H
#define MCRL2_DATA_DETAIL_MACHINE_WORD_H
 
#include <limits>
#include "mcrl2/data/bool.h"
#include "mcrl2/data/machine_number.h"
#include "mcrl2/data/machine_word.h"
 
namespace mcrl2
{
 
namespace data
{
 
namespace sort_machine_word
{
 
namespace detail
{
 
/* Below standard operations on machine numbers are implemented.  */
 
inline const machine_number& zero_word()
{
  static const machine_number zero=machine_number(0);
  return zero;
}
 
inline const machine_number& one_word()
{
  static const machine_number one=machine_number(1);
  return one;
}
 
inline const machine_number& two_word()
{
  static const machine_number two=machine_number(2);
  return two;
}
 
inline const machine_number& three_word()
{
  static const machine_number three=machine_number(3);
  return three;
}
 
inline const machine_number& four_word()
{
  static const machine_number four=machine_number(4);
  return four;
}
 
inline const machine_number& max_word()
{
  static const machine_number max=machine_number(std::numeric_limits<std::size_t>::max());
  return max;
}
 
inline bool equals_zero_word(const std::size_t n)
{
  return n==0;
}
 
inline bool equals_one_word(const std::size_t n)
{
  return n==1;
}
 
inline bool equals_max_word(const std::size_t n)
{
  return n==std::numeric_limits<std::size_t>::max();
}
 
inline std::size_t succ_word(const std::size_t n)
{
  return 1+n;
}
 
inline bool equal_word(const std::size_t n1, const std::size_t n2)
{
  return n1==n2;
}
 
inline bool less_word(const std::size_t n1, const std::size_t n2)
{
  return n1<n2;
}
 
inline bool less_equal_word(const std::size_t n1, const std::size_t n2)
{
  return n1<=n2;
}
 
inline std::size_t add_word(const std::size_t n1, const std::size_t n2)
{
  return n1+n2;
}
 
inline std::size_t add_with_carry_word(const std::size_t n1, const std::size_t n2)
{
  return n1+n2+1;
}
 
inline bool add_overflow_word(const std::size_t n1, const std::size_t n2)
{
  if (n1+n2<n1)
  {
    return true;  // In this case there is an overflow.
  }
 return false; // No overflow. 
}
 
inline bool add_with_carry_overflow_word(const std::size_t n1, const std::size_t n2)
{
  if (n1+n2+1<n1)
  {
    return true;  // In this case there is an overflow.
  }
  return false; // No overflow. 
}
 
inline std::size_t times_word(const std::size_t n1, const std::size_t n2)
{
  return n1*n2;
}
 
inline std::size_t times_with_carry_word(const std::size_t n1, const std::size_t n2, const std::size_t n3)
{
  return n1*n2+n3;
}
 
std::size_t times_overflow_word(const std::size_t n1, const std::size_t n2);
 
std::size_t times_with_carry_overflow_word(const std::size_t n1, const std::size_t n2, std::size_t n3);
 
inline std::size_t minus_word(const std::size_t n1, const std::size_t n2)
{
  return n1-n2;
}
 
inline std::size_t monus_word(const std::size_t n1, const std::size_t n2)
{
  if (n1>n2) 
  { 
    return n1-n2;
  }
  return 0;
}
 
inline std::size_t div_word(const std::size_t n1, const std::size_t n2)
{
  return n1/n2;
}
 
inline std::size_t mod_word(const std::size_t n1, const std::size_t n2)
{
  return n1 % n2;
}
 
std::size_t div_doubleword(const std::size_t n1, const std::size_t n2, const std::size_t n3);
 
std::size_t mod_doubleword(const std::size_t n1, const std::size_t n2, const std::size_t n3);
 
std::size_t div_double_doubleword(const std::size_t n1, const std::size_t n2, const std::size_t n3, const std::size_t n4);
 
std::size_t mod_double_doubleword(const std::size_t n1, const std::size_t n2, const std::size_t n3, const std::size_t n4);
 
std::size_t div_triple_doubleword(const std::size_t n1, const std::size_t n2, const std::size_t n3, const std::size_t n4, const std::size_t n5);
 
inline std::size_t sqrt_word(const std::size_t n)
{
  return sqrt(n);
}
 
std::size_t sqrt_doubleword(const std::size_t n1, const std::size_t n2);
 
std::size_t sqrt_tripleword(const std::size_t n1, const std::size_t n2, const std::size_t n3);
 
std::size_t sqrt_tripleword_overflow(const std::size_t n1, const std::size_t n2, const std::size_t n3);
 
std::size_t sqrt_quadrupleword(const std::size_t n1, const std::size_t n2, const std::size_t n3, const std::size_t n4);
 
std::size_t sqrt_quadrupleword_overflow(const std::size_t n1, const std::size_t n2, const std::size_t n3, const std::size_t n4);
 
inline std::size_t pred_word(const std::size_t n)
{
  return n-1;
}
 
inline void rightmost_bit(data_expression& result, const std::size_t n)
{
  if ((n & 1) == 1)
  {
    result=sort_bool::true_();
    return;
  }
  result=sort_bool::false_();
}
 
inline std::size_t shift_right(const data_expression& e1, const std::size_t n)
{
  std::size_t m = n>>1;
  if (e1==sort_bool::true_())
  {
    return m | static_cast<std::size_t>(1)<<((8*sizeof(std::size_t))-1);
  }
  return m;
}
 
} // end namespace detail 
 
inline void zero_word_manual_implementation(data_expression& result)
{
  result=detail::zero_word();
}
 
inline void one_word_manual_implementation(data_expression& result)
{
  result=detail::one_word();
}
 
inline void two_word_manual_implementation(data_expression& result)
{
  result=detail::two_word();
}
 
inline void three_word_manual_implementation(data_expression& result)
{
  result=detail::three_word();
}
 
inline void four_word_manual_implementation(data_expression& result)
{
  result=detail::four_word();
}
 
inline void max_word_manual_implementation(data_expression& result)
{
  result=detail::max_word();
}
 
inline void equals_zero_word_manual_implementation(data_expression& result, const data_expression& e)
{
  assert(is_machine_number(e));
  if (detail::equals_zero_word(atermpp::down_cast<machine_number>(e).value()))
  {
    result=sort_bool::true_();
    return;
  }
  result=sort_bool::false_();
  return;
}
 
inline void not_equals_zero_word_manual_implementation(data_expression& result, const data_expression& e)
{
  assert(is_machine_number(e));
  if (detail::equals_zero_word(atermpp::down_cast<machine_number>(e).value()))
  {
    result=sort_bool::false_();
    return;
  }
  result=sort_bool::true_();
  return;
}
 
inline void equals_one_word_manual_implementation(data_expression& result, const data_expression& e)
{
  assert(is_machine_number(e));
  if (detail::equals_one_word(atermpp::down_cast<machine_number>(e).value()))
  {
    result=sort_bool::true_();
    return;
  }
  result=sort_bool::false_();
  return;
}
 
inline void equals_max_word_manual_implementation(data_expression& result, const data_expression& e)
{
  assert(is_machine_number(e));
  if (detail::equals_max_word(atermpp::down_cast<machine_number>(e).value()))
  {
    result=sort_bool::true_();
    return;
  }
  result=sort_bool::false_();
  return;
}
 
inline void succ_word_manual_implementation(data_expression& result, const data_expression& e)
{
  assert(is_machine_number(e));
  make_machine_number(result, detail::succ_word(atermpp::down_cast<machine_number>(e).value()));
}
 
inline void equal_word_manual_implementation(data_expression& result, const data_expression& e1, const data_expression& e2)
{
  assert(is_machine_number(e1) && is_machine_number(e2));
  const bool b=detail::equal_word(
                            atermpp::down_cast<machine_number>(e1).value(),
                            atermpp::down_cast<machine_number>(e2).value());
  result=(b? sort_bool::true_(): sort_bool::false_());
}
 
inline void not_equal_word_manual_implementation(data_expression& result, const data_expression& e1, const data_expression& e2)
{
  assert(is_machine_number(e1) && is_machine_number(e2));
  const bool b=detail::equal_word(
                          atermpp::down_cast<machine_number>(e1).value(),
                          atermpp::down_cast<machine_number>(e2).value());
  result=(b? sort_bool::false_(): sort_bool::true_());
}
 
inline void less_word_manual_implementation(data_expression& result, const data_expression& e1, const data_expression& e2)
{
  assert(is_machine_number(e1) && is_machine_number(e2));
  const bool b=detail::less_word(atermpp::down_cast<machine_number>(e1).value(),atermpp::down_cast<machine_number>(e2).value());
  result=(b? sort_bool::true_(): sort_bool::false_());
}
 
inline void less_equal_word_manual_implementation(data_expression& result, const data_expression& e1, const data_expression& e2)
{
  assert(is_machine_number(e1) && is_machine_number(e2));
  const bool b=detail::less_equal_word(atermpp::down_cast<machine_number>(e1).value(),atermpp::down_cast<machine_number>(e2).value());
  result=(b? sort_bool::true_(): sort_bool::false_());
}
 
inline void greater_word_manual_implementation(data_expression& result, const data_expression& e1, const data_expression& e2)
{
  assert(is_machine_number(e1) && is_machine_number(e2));
  const bool b=detail::less_word(atermpp::down_cast<machine_number>(e2).value(),atermpp::down_cast<machine_number>(e1).value());
  result=(b? sort_bool::true_(): sort_bool::false_());
}
 
inline void greater_equal_word_manual_implementation(data_expression& result, const data_expression& e1, const data_expression& e2)
{
  assert(is_machine_number(e1) && is_machine_number(e2));
  const bool b=detail::less_equal_word(atermpp::down_cast<machine_number>(e2).value(),atermpp::down_cast<machine_number>(e1).value());
  result=(b? sort_bool::true_(): sort_bool::false_());
}
 
inline void add_word_manual_implementation(data_expression& result, const data_expression& e1, const data_expression& e2)
{
  assert(is_machine_number(e1) && is_machine_number(e2));
  make_machine_number(result, detail::add_word(
                              atermpp::down_cast<machine_number>(e1).value(),
                              atermpp::down_cast<machine_number>(e2).value()));
}
 
inline void add_with_carry_word_manual_implementation(data_expression& result, const data_expression& e1, const data_expression& e2)
{
  assert(is_machine_number(e1) && is_machine_number(e2));
  make_machine_number(result, detail::add_with_carry_word(
                              atermpp::down_cast<machine_number>(e1).value(),
                              atermpp::down_cast<machine_number>(e2).value()));
}
 
inline void add_overflow_word_manual_implementation(data_expression& result, const data_expression& e1, const data_expression& e2)
{
  assert(is_machine_number(e1) && is_machine_number(e2));
  if (detail::add_overflow_word(
                              atermpp::down_cast<machine_number>(e1).value(),
                              atermpp::down_cast<machine_number>(e2).value()))
  {
    result=sort_bool::true_();
    return;
  }
  result=sort_bool::false_();
}
 
inline void add_with_carry_overflow_word_manual_implementation(data_expression& result, const data_expression& e1, const data_expression& e2)
{
  assert(is_machine_number(e1) && is_machine_number(e2));
  if (detail::add_with_carry_overflow_word(
                              atermpp::down_cast<machine_number>(e1).value(),
                              atermpp::down_cast<machine_number>(e2).value()))
  {
    result=sort_bool::true_();
    return;
  }
  result=sort_bool::false_();
}
 
inline void times_word_manual_implementation(data_expression& result, const data_expression& e1, const data_expression& e2)
{
  assert(is_machine_number(e1) && is_machine_number(e2));
  make_machine_number(result, detail::times_word(
                              atermpp::down_cast<machine_number>(e1).value(),
                              atermpp::down_cast<machine_number>(e2).value()));
}
 
inline void times_with_carry_word_manual_implementation(data_expression& result, const data_expression& e1, const data_expression& e2, const data_expression& e3)
{
  assert(is_machine_number(e1) && is_machine_number(e2) && is_machine_number(e3));
  make_machine_number(result, detail::times_with_carry_word(
                              atermpp::down_cast<machine_number>(e1).value(),
                              atermpp::down_cast<machine_number>(e2).value(),
                              atermpp::down_cast<machine_number>(e3).value()));
}
 
inline void times_overflow_word_manual_implementation(data_expression& result, const data_expression& e1, const data_expression& e2)
{
  assert(is_machine_number(e1) && is_machine_number(e2));
  make_machine_number(result, detail::times_overflow_word(
                              atermpp::down_cast<machine_number>(e1).value(),
                              atermpp::down_cast<machine_number>(e2).value()));
}
 
inline void times_with_carry_overflow_word_manual_implementation(data_expression& result, const data_expression& e1, const data_expression& e2, const data_expression& e3)
{
  assert(is_machine_number(e1) && is_machine_number(e2) && is_machine_number(e3));
  make_machine_number(result, detail::times_with_carry_overflow_word(
                              atermpp::down_cast<machine_number>(e1).value(),
                              atermpp::down_cast<machine_number>(e2).value(),
                              atermpp::down_cast<machine_number>(e3).value()));
}
 
inline void minus_word_manual_implementation(data_expression& result, const data_expression& e1, const data_expression& e2)
{
  assert(is_machine_number(e1) && is_machine_number(e2));
  make_machine_number(result, detail::minus_word(
                              atermpp::down_cast<machine_number>(e1).value(),
                              atermpp::down_cast<machine_number>(e2).value()));
}
 
inline void monus_word_manual_implementation(data_expression& result, const data_expression& e1, const data_expression& e2)
{
  assert(is_machine_number(e1) && is_machine_number(e2));
  make_machine_number(result, detail::minus_word(
                              atermpp::down_cast<machine_number>(e1).value(),
                              atermpp::down_cast<machine_number>(e2).value()));
}
 
inline void div_word_manual_implementation(data_expression& result, const data_expression& e1, const data_expression& e2)
{
  assert(is_machine_number(e1) && is_machine_number(e2));
  make_machine_number(result, detail::div_word(
                              atermpp::down_cast<machine_number>(e1).value(),
                              atermpp::down_cast<machine_number>(e2).value()));
}
 
inline void mod_word_manual_implementation(data_expression& result, const data_expression& e1, const data_expression& e2)
{
  assert(is_machine_number(e1) && is_machine_number(e2));
  make_machine_number(result, detail::mod_word(
                              atermpp::down_cast<machine_number>(e1).value(), 
                              atermpp::down_cast<machine_number>(e2).value()));
}
 
inline void sqrt_word_manual_implementation(data_expression& result, const data_expression& e)
{
  assert(is_machine_number(e));
  make_machine_number(result, detail::sqrt_word(atermpp::down_cast<machine_number>(e).value()));
}
 
inline void div_doubleword_manual_implementation(data_expression& result, const data_expression& e1, const data_expression& e2, const data_expression& e3)
{
  assert(is_machine_number(e1) && is_machine_number(e2) && is_machine_number(e3));
  make_machine_number(result, detail::div_doubleword(
                              atermpp::down_cast<machine_number>(e1).value(), 
                              atermpp::down_cast<machine_number>(e2).value(), 
                              atermpp::down_cast<machine_number>(e3).value()));
}
 
inline void div_double_doubleword_manual_implementation(data_expression& result, const data_expression& e1, const data_expression& e2, const data_expression& e3, const data_expression& e4)
{
  assert(is_machine_number(e1) && is_machine_number(e2) && is_machine_number(e3) && is_machine_number(e4));
  make_machine_number(result, detail::div_double_doubleword(
                              atermpp::down_cast<machine_number>(e1).value(), 
                              atermpp::down_cast<machine_number>(e2).value(), 
                              atermpp::down_cast<machine_number>(e3).value(), 
                              atermpp::down_cast<machine_number>(e4).value()));
}
 
inline void div_triple_doubleword_manual_implementation(
                        data_expression& result, 
                        const data_expression& e1, 
                        const data_expression& e2, 
                        const data_expression& e3, 
                        const data_expression& e4, 
                        const data_expression& e5)
{
  assert(is_machine_number(e1) && is_machine_number(e2) && is_machine_number(e3) && is_machine_number(e4) && is_machine_number(e5));
  make_machine_number(result, detail::div_triple_doubleword(
                                 atermpp::down_cast<machine_number>(e1).value(), 
                                 atermpp::down_cast<machine_number>(e2).value(), 
                                 atermpp::down_cast<machine_number>(e3).value(), 
                                 atermpp::down_cast<machine_number>(e4).value(),
                                 atermpp::down_cast<machine_number>(e5).value()));
}
 
inline void mod_double_doubleword_manual_implementation(data_expression& result, const data_expression& e1, const data_expression& e2, const data_expression& e3, const data_expression& e4)
{
  assert(is_machine_number(e1) && is_machine_number(e2) && is_machine_number(e3) && is_machine_number(e4));
  make_machine_number(result, detail::mod_double_doubleword(
                              atermpp::down_cast<machine_number>(e1).value(), 
                              atermpp::down_cast<machine_number>(e2).value(), 
                              atermpp::down_cast<machine_number>(e3).value(), 
                              atermpp::down_cast<machine_number>(e4).value()));
}
 
inline void sqrt_doubleword_manual_implementation(data_expression& result, const data_expression& e1, const data_expression& e2)
{
  assert(is_machine_number(e1) && is_machine_number(e2));
  make_machine_number(result, detail::sqrt_doubleword(
                              atermpp::down_cast<machine_number>(e1).value(),
                              atermpp::down_cast<machine_number>(e2).value()));
}
 
inline void mod_doubleword_manual_implementation(data_expression& result, const data_expression& e1, const data_expression& e2, const data_expression& e3)
{
  assert(is_machine_number(e1) && is_machine_number(e2) && is_machine_number(e3));
  make_machine_number(result, detail::mod_doubleword(
                              atermpp::down_cast<machine_number>(e1).value(), 
                              atermpp::down_cast<machine_number>(e2).value(), 
                              atermpp::down_cast<machine_number>(e3).value()));
}
 
inline void sqrt_tripleword_manual_implementation(data_expression& result, const data_expression& e1, const data_expression& e2, const data_expression& e3)
{
  assert(is_machine_number(e1) && is_machine_number(e2) && is_machine_number(e3));
  make_machine_number(result, detail::sqrt_tripleword(
                              atermpp::down_cast<machine_number>(e1).value(), 
                              atermpp::down_cast<machine_number>(e2).value(), 
                              atermpp::down_cast<machine_number>(e3).value()));
}
 
inline void sqrt_tripleword_overflow_manual_implementation(data_expression& result, const data_expression& e1, const data_expression& e2, const data_expression& e3)
{
  assert(is_machine_number(e1) && is_machine_number(e2) && is_machine_number(e3));
  make_machine_number(result, detail::sqrt_tripleword_overflow(
                              atermpp::down_cast<machine_number>(e1).value(), 
                              atermpp::down_cast<machine_number>(e2).value(), 
                              atermpp::down_cast<machine_number>(e3).value()));
}
 
inline void sqrt_quadrupleword_manual_implementation(
                                      data_expression& result, 
                                      const data_expression& e1, 
                                      const data_expression& e2, 
                                      const data_expression& e3, 
                                      const data_expression& e4)
{
  assert(is_machine_number(e1) && is_machine_number(e2) && is_machine_number(e3) && is_machine_number(e4));
  make_machine_number(result, detail::sqrt_quadrupleword(
                              atermpp::down_cast<machine_number>(e1).value(), 
                              atermpp::down_cast<machine_number>(e2).value(), 
                              atermpp::down_cast<machine_number>(e3).value(), 
                              atermpp::down_cast<machine_number>(e4).value()));
}
 
inline void sqrt_quadrupleword_overflow_manual_implementation(
                                      data_expression& result, 
                                      const data_expression& e1, 
                                      const data_expression& e2, 
                                      const data_expression& e3, 
                                      const data_expression& e4)
{
  assert(is_machine_number(e1) && is_machine_number(e2) && is_machine_number(e3) && is_machine_number(e4));
  make_machine_number(result, detail::sqrt_quadrupleword_overflow(
                              atermpp::down_cast<machine_number>(e1).value(), 
                              atermpp::down_cast<machine_number>(e2).value(), 
                              atermpp::down_cast<machine_number>(e3).value(), 
                              atermpp::down_cast<machine_number>(e4).value()));
}
 
inline void pred_word_manual_implementation(data_expression& result, const data_expression& e)
{
  make_machine_number(result, detail::pred_word(atermpp::down_cast<machine_number>(e).value())); 
}
 
inline void rightmost_bit_manual_implementation(data_expression& result, const data_expression& e)
{
  detail::rightmost_bit(result, atermpp::down_cast<machine_number>(e).value()); 
}
 
inline void shift_right_manual_implementation(data_expression& result, const data_expression& e1, const data_expression& e2)
{
  assert(e1==sort_bool::true_() || e1==sort_bool::false_());
  make_machine_number(result, detail::shift_right(e1, atermpp::down_cast<machine_number>(e2).value())); 
}
 
 
} // namespace sort_machine_word
 
} // namespace data
 
} // namespace mcrl2
 
#endif // MCRL2_DATA_MACHINE_NUMBER_H