mCRL2
Loading...
Searching...
No Matches
machine_word.cpp
Go to the documentation of this file.
1// Author(s): 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//
13
14#include <boost/multiprecision/cpp_int.hpp>
16
17namespace mcrl2
18{
19
20namespace data
21{
22
23namespace sort_machine_word
24{
25
26namespace detail
27{
28
29/* Below standard operations on machine numbers are implemented. */
30
31std::size_t times_overflow_word(const std::size_t n1, const std::size_t n2)
32{
33 boost::multiprecision::uint128_t m1=n1;
34 boost::multiprecision::uint128_t m2=n2;
35 return static_cast<std::size_t>((m1*m2) >> std::numeric_limits<std::size_t>::digits);
36}
37
38std::size_t times_with_carry_overflow_word(const std::size_t n1, const std::size_t n2, const std::size_t n3)
39{
40 boost::multiprecision::uint128_t m1=n1;
41 boost::multiprecision::uint128_t m2=n2;
42 boost::multiprecision::uint128_t m3=n3;
43 return static_cast<std::size_t>((m1*m2+m3) >> std::numeric_limits<std::size_t>::digits);
44}
45
46std::size_t div_doubleword(const std::size_t n1, const std::size_t n2, const std::size_t n3)
47{
48 boost::multiprecision::uint128_t m1=n1;
49 m1 = (m1 << std::numeric_limits<std::size_t>::digits)+n2;
50 boost::multiprecision::uint128_t m2=n3;
51 return static_cast<std::size_t>(m1 / m2);
52}
53
54std::size_t mod_doubleword(const std::size_t n1, const std::size_t n2, const std::size_t n3)
55{
56 boost::multiprecision::uint128_t m1=n1;
57 m1 = (m1 << std::numeric_limits<std::size_t>::digits)+n2;
58 boost::multiprecision::uint128_t m2=n3;
59 return static_cast<std::size_t>(m1 % m2);
60}
61
62std::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)
63{
64 boost::multiprecision::uint128_t m1=n1;
65 m1 = (m1 << std::numeric_limits<std::size_t>::digits)+n2;
66 boost::multiprecision::uint128_t m2=n3;
67 m2 = (m2 << std::numeric_limits<std::size_t>::digits)+n4;
68 return static_cast<std::size_t>(m1 / m2);
69}
70
71std::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)
72{
73 boost::multiprecision::uint128_t m1=n1;
74 m1 = (m1 << std::numeric_limits<std::size_t>::digits)+n2;
75 boost::multiprecision::uint128_t m2=n3;
76 m2 = (m2 << std::numeric_limits<std::size_t>::digits)+n4;
77 return static_cast<std::size_t>(m1 % m2);
78}
79
80std::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)
81{
82 boost::multiprecision::uint256_t m1=n1;
83 m1 = (m1 << std::numeric_limits<std::size_t>::digits)+n2;
84 m1 = (m1 << std::numeric_limits<std::size_t>::digits)+n3;
85 boost::multiprecision::uint256_t m2=n4;
86 m2 = (m2 << std::numeric_limits<std::size_t>::digits)+n5;
87 return static_cast<std::size_t>(m1 / m2);
88}
89
90std::size_t sqrt_doubleword(const std::size_t n1, const std::size_t n2)
91{
92 boost::multiprecision::uint128_t m1=n1;
93 m1 = (m1 << std::numeric_limits<std::size_t>::digits)+n2;
94 return static_cast<std::size_t>(sqrt(m1));
95}
96
97std::size_t sqrt_tripleword(const std::size_t n1, const std::size_t n2, const std::size_t n3)
98{
99 boost::multiprecision::uint256_t m1=n1;
100 m1 = (m1 << std::numeric_limits<std::size_t>::digits)+n2;
101 m1 = (m1 << std::numeric_limits<std::size_t>::digits)+n3;
102 return static_cast<std::size_t>(sqrt(m1));
103}
104
105std::size_t sqrt_tripleword_overflow(const std::size_t n1, const std::size_t n2, const std::size_t n3)
106{
107 boost::multiprecision::uint256_t m1=n1;
108 m1 = (m1 << std::numeric_limits<std::size_t>::digits)+n2;
109 m1 = (m1 << std::numeric_limits<std::size_t>::digits)+n3;
110 return static_cast<std::size_t>(sqrt(m1)>>std::numeric_limits<std::size_t>::digits);
111}
112
113std::size_t sqrt_quadrupleword(const std::size_t n1, const std::size_t n2, const std::size_t n3, const std::size_t n4)
114{
115 boost::multiprecision::uint256_t m1=n1;
116 m1 = (m1 << std::numeric_limits<std::size_t>::digits)+n2;
117 m1 = (m1 << std::numeric_limits<std::size_t>::digits)+n3;
118 m1 = (m1 << std::numeric_limits<std::size_t>::digits)+n4;
119 return static_cast<std::size_t>(sqrt(m1));
120}
121
122std::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)
123{
124 boost::multiprecision::uint256_t m1=n1;
125 m1 = (m1 << std::numeric_limits<std::size_t>::digits)+n2;
126 m1 = (m1 << std::numeric_limits<std::size_t>::digits)+n3;
127 m1 = (m1 << std::numeric_limits<std::size_t>::digits)+n4;
128 return static_cast<std::size_t>(sqrt(m1)>>std::numeric_limits<std::size_t>::digits);
129}
130
131
132} // end namespace detail
133
134} // namespace sort_machine_word
135
136} // namespace data
137
138} // namespace mcrl2
139
140
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)
const function_symbol & div_double_doubleword()
Constructor for function symbol @div_double_doubleword.
const function_symbol & div_doubleword()
Constructor for function symbol @div_doubleword.
const function_symbol & sqrt_quadrupleword_overflow()
Constructor for function symbol @sqrt_quadrupleword_overflow.
const function_symbol & sqrt_tripleword_overflow()
Constructor for function symbol @sqrt_tripleword_overflow.
const function_symbol & sqrt_quadrupleword()
Constructor for function symbol @sqrt_quadrupleword.
const function_symbol & times_with_carry_overflow_word()
Constructor for function symbol @times_with_carry_overflow_word.
const function_symbol & div_triple_doubleword()
Constructor for function symbol @div_triple_doubleword.
const function_symbol & times_overflow_word()
Constructor for function symbol @times_overflow_word.
const function_symbol & mod_doubleword()
Constructor for function symbol @mod_doubleword.
const function_symbol & sqrt_tripleword()
Constructor for function symbol @sqrt_tripleword.
const function_symbol & sqrt_doubleword()
Constructor for function symbol @sqrt_doubleword.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72