mCRL2
Loading...
Searching...
No Matches
standard_numbers_utility.h
Go to the documentation of this file.
1// Author(s): Jeroen van der Wulp
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//
11
12#ifndef MCRL2_DATA_STANDARD_NUMBERS_UTILITY_H
13#define MCRL2_DATA_STANDARD_NUMBERS_UTILITY_H
14
16
17namespace mcrl2
18{
19
20namespace data
21{
22
24namespace detail
25{
26// Convert to number represented as character array where each character
27// represents a decimal digit
28inline std::vector< char > string_to_vector_number(const std::string& s)
29{
30 assert(s.size() > 0);
31 std::vector< char > result;
32
33 result.reserve(s.size());
34
35 for (char i: s)
36 {
37 assert('0' <= i && i <= '9');
38
39 result.push_back(i - '0');
40 }
41
42 return result;
43}
44
45// Convert from number represented as character array where each character
46// represents a decimal digit
47inline std::string vector_number_to_string(const std::vector< char >& v)
48{
49 assert(v.size() > 0);
50 std::string result;
51
52 result.reserve(v.size());
53
54 for (char i: v)
55 {
56 result.push_back(i + '0');
57 }
58
59 return result;
60}
61
65inline void decimal_number_multiply_by_two(std::vector< char >& number)
66{
67 assert(0 < number.size());
68
69 std::vector< char > result(number.size() + 2, 0);
70 std::vector< char >::iterator j(result.begin());
71
72 if (5 <= number[0])
73 {
74 *(j++) = number[0] / 5;
75 }
76
77 for (std::vector< char >::const_iterator i = number.begin(); i < number.end(); ++i, ++j)
78 {
79 // result[a] = 2*(number[b] mod 5) + number[b+1] div 5 where result[a] = *j and number[b] = *(i)
80 if (i == number.end() - 1)
81 {
82 *j = 2 * (*i % 5);
83 }
84 else
85 {
86 *j = 2 * (*i % 5) + *(i+1) / 5;
87 }
88 }
89
90 result.resize(j - result.begin());
91
92 number.swap(result);
93}
94
95
99inline void decimal_number_increment(std::vector< char >& number)
100{
101 assert(0 < number.size());
102
103 for (std::vector< char >::reverse_iterator i = number.rbegin(); i != number.rend(); ++i)
104 {
105 if (*i < 9)
106 {
107 ++(*i);
108
109 return;
110 }
111 else
112 {
113 *i = 0;
114 }
115 }
116
117 number.insert(number.begin(), 1);
118}
119
120
122template< typename T >
123inline std::string as_decimal_string(T t)
124{
125 if (t != 0)
126 {
127 std::string result;
128
129 while (0 < t)
130 {
131 result.append(1, '0' + static_cast< char >(t % 10));
132
133 t /= 10;
134 }
135
136 return std::string(result.rbegin(), result.rend());
137 }
138
139 return "0";
140}
141
145inline void decimal_number_divide_by_two(std::vector< char >& number)
146{
147 assert(0 < number.size());
148
149 std::vector< char > result(number.size(), 0);
150 std::vector< char >::iterator j(result.begin());
151
152 if (2 <= number[0])
153 {
154 *(j++) = number[0] / 2;
155 }
156
157 for (std::vector< char >::const_iterator i = number.begin() + 1; i != number.end(); ++i, ++j)
158 {
159 // result[a] = 5*(number[b - 1] mod 2) + number[b] div 2 where result[a] = *j, number[b - 1] = *(i - 1)
160 *j = 5 * (*(i - 1) % 2) + *i / 2;
161 }
162
163 result.resize(j - result.begin());
164
165 number.swap(result);
166}
167
168#ifdef MCRL2_ENABLE_MACHINENUMBERS
169// Check whether a number vector is equal to zero.
170inline bool is_zero_number_vector(const std::vector< std::size_t >& v)
171{
172 for(const std::size_t n: v)
173 {
174 if (n>0)
175 {
176 return false;
177 }
178 }
179 // All digits are zero. Thus the number is zero.
180 assert(v.size()<2); // Zero can only occur as a vector of length 0 or 1.
181 return true;
182}
183
184
185// Add the two number vectors. The least significant digit is at position 0.
186inline std::vector<std::size_t> add_number_vectors(const std::vector< std::size_t >& v1,
187 const std::vector< std::size_t >& v2)
188{
189 std::vector<std::size_t> result;
190 std::size_t carry=0;
191 for(std::size_t i=0; i<std::max(v1.size(),v2.size()); i++)
192 {
193 std::size_t n1 = (i<v1.size()? v1[i]: 0);
194 std::size_t n2 = (i<v2.size()? v2[i]: 0);
195
196 std::size_t sum = n1+n2+carry;
197 if (sum<n1) // There is a carry overflow.
198 {
199 assert(sum<n2);
200 carry=1;
201 }
202 else
203 {
204 carry=0;
205 }
206 result.push_back(sum);
207 }
208 if (carry==1)
209 {
210 result.push_back(1);
211 }
212 assert(result.size()<=1 || result.back()!=0);
213 return result;
214}
215
216
217inline std::vector<size_t> multiply_by10_and_add(const std::vector< size_t >& v, size_t val)
218{
219 std::vector<size_t> val_vector(1,val);
220 assert(val_vector.size()==1);
221 std::vector<size_t> result=add_number_vectors(v,v); // result is 2 v.
222 result = add_number_vectors(result, result); // result is 4 v.
223 result = add_number_vectors(result, v); // result is 5 v.
224 result = add_number_vectors(result, result); // result is 10 v.
225 result = add_number_vectors(result, val_vector); // result is 10 v + val.
226 return result;
227}
228
229// Transform a number vector to a string representation of the same number.
230inline std::string number_vector_as_string(const std::vector< std::size_t >& v)
231{
232 assert(!detail::is_zero_number_vector(v));
233
234 std::vector< char > result = detail::string_to_vector_number("0");
235 bool is_zero=true; // Avoid doing many multiplications for small numbers.
236
237 for(size_t i=v.size(); i>0 ; --i)
238 {
239 std::size_t n= v.at(i-1);
240 for(std::size_t mask = std::size_t(1)<<(8*sizeof(std::size_t)-1); mask>0; mask=mask>>1)
241 {
242 if (!is_zero)
243 {
244 detail::decimal_number_multiply_by_two(result);
245 }
246 if ((n & mask) >0)
247 {
248 detail::decimal_number_increment(result);
249 is_zero=false;
250 }
251 }
252 }
253
254 return detail::vector_number_to_string(result);
255}
256
257
258// Multiply a vector consisting of size_t's with 10 and add the extra value.
259// Convert to number represented as character array where each character
260// represents a decimal digit
261inline std::vector< size_t > number_string_to_vector_number(const std::string& s)
262{
263 assert(s.size() > 0);
264 std::vector< size_t > result;
265
266 result.reserve(s.size()/18); // approximately 18 digits fit in one size_t.
267
268 for (char i: s)
269 {
270 if ('0' <= i && i <= '9')
271 {
272 result = multiply_by10_and_add(result, i - '0');
273 }
274 else
275 {
276 throw mcrl2::runtime_error("The string " + s + " is expected to only consist of digits. ");
277 }
278 }
279
280 return result;
281}
282#endif
283
284} // namespace detail
286
287namespace sort_pos
288{
291template < typename T >
292inline typename std::enable_if<std::is_integral< T >::value, data_expression>::type
293pos(const T t)
294{
295 assert(t>0);
296
297#ifdef MCRL2_ENABLE_MACHINENUMBERS
298 static_assert(sizeof(T)<=sizeof(std::size_t),"Can only convert numbers up till a size_t.");
300#else
301 std::vector< bool > bits;
302 bits.reserve(8 * sizeof(T));
303
304 for (T u = t; 1 < u; u /= 2)
305 {
306 bits.push_back(u % 2 != 0);
307 }
308
310
311 for (std::vector< bool >::reverse_iterator i = bits.rbegin(); i != bits.rend(); ++i)
312 {
313 result = sort_pos::cdub(sort_bool::bool_(*i), result);
314 }
315
316 return result;
317#endif
318}
319
322inline data_expression pos(const std::string& n)
323{
324#ifdef MCRL2_ENABLE_MACHINENUMBERS
325 std::vector<std::size_t> number_vector= detail::number_string_to_vector_number(n);
326
327 assert(!detail::is_zero_number_vector(number_vector));
328
329 data_expression result=most_significant_digit(machine_number(number_vector.back()));
330 for(std::size_t i=number_vector.size()-1; i>0; --i)
331 {
332 result = sort_pos::concat_digit(result,machine_number(number_vector.at(i-1)));
333 }
334 return result;
335
336#else
337 std::vector< char > number_as_vector(detail::string_to_vector_number(n));
338
339 std::vector< bool > bits;
340
341 while (0 < number_as_vector.size() && !((number_as_vector.size() == 1) && number_as_vector[0] == 1)) // number != 1
342 {
343 bits.push_back((static_cast< int >(*number_as_vector.rbegin()) % 2 != 0));
344
345 detail::decimal_number_divide_by_two(number_as_vector);
346 }
348
349 for (std::vector< bool >::reverse_iterator i = bits.rbegin(); i != bits.rend(); ++i)
350 {
351 result = sort_pos::cdub(sort_bool::bool_(*i), result);
352 }
353
354 return result;
355#endif
356}
357
361{
362#ifdef MCRL2_ENABLE_MACHINENUMBERS
367 );
368#else
373 );
374#endif
375}
376
383inline
385{
386#ifdef MCRL2_ENABLE_MACHINENUMBERS
387 std::vector<std::size_t> number_vector;
388 data_expression n=n_in;
389
391 {
392 number_vector.push_back(atermpp::down_cast<machine_number>(sort_pos::arg2(n)).value());
393 n = sort_pos::arg1(n);
394 }
395
397 number_vector.push_back(atermpp::down_cast<machine_number>(sort_pos::arg(n)).value());
398
399 return detail::number_vector_as_string(number_vector);
400#else
401 std::vector<bool> bits;
402 data_expression n=n_in;
403
405 {
407 n = sort_pos::right(n);
408 }
409
411
412 std::vector< char > result = detail::string_to_vector_number("1");
413
414 for (std::vector<bool>::reverse_iterator i = bits.rbegin(); i != bits.rend(); ++i)
415 {
416 detail::decimal_number_multiply_by_two(result);
417 if (*i)
418 {
419 detail::decimal_number_increment(result);
420 }
421 }
422
423 return detail::vector_number_to_string(result);
424#endif
425}
426
433template <class NUMERIC_TYPE>
434inline
436{
437#ifdef MCRL2_ENABLE_MACHINENUMBERS
438 if constexpr (std::is_integral<NUMERIC_TYPE>::value)
439 {
441 {
442 mcrl2::runtime_error("Number " + pp(n) + " is too large to transform to a machine number.");
443 }
445 assert(atermpp::down_cast<machine_number>(sort_pos::arg(n)).value()>0);
446 return atermpp::down_cast<machine_number>(sort_pos::arg(n)).value();
447 }
448 else
449 {
451 {
452 return positive_constant_to_value<NUMERIC_TYPE>(sort_pos::arg1(n))*pow(2.0,64) +
453 atermpp::down_cast<machine_number>(sort_pos::arg2(n)).value();
454 }
456 return atermpp::down_cast<machine_number>(sort_pos::arg(n)).value();
457 }
458#else
460 {
461 NUMERIC_TYPE result = 2*positive_constant_to_value<NUMERIC_TYPE>(sort_pos::right(n));
463 {
464 result=result+1;
465 }
466 return result;
467 }
468
470
471 return static_cast<NUMERIC_TYPE>(1);
472#endif
473}
474
475} // namespace sort_pos
476
477namespace sort_nat
478{
479
481template < typename T >
482inline typename std::enable_if< std::is_integral< T >::value, data_expression >::type
483nat(T t)
484{
485#ifdef MCRL2_ENABLE_MACHINENUMBERS
486 static_assert(sizeof(T)<=sizeof(std::size_t),"Can only convert numbers up till a size_t.");
488#else
489 if (t == 0)
490 {
491 return sort_nat::c0();
492 }
493 return sort_nat::cnat(sort_pos::pos(t));
494#endif
495}
496
499inline data_expression nat(const std::string& n)
500{
501#ifdef MCRL2_ENABLE_MACHINENUMBERS
502 std::vector<std::size_t> number_vector= detail::number_string_to_vector_number(n);
503
504 if (number_vector.empty())
505 {
507 }
508 data_expression result=most_significant_digit_nat(machine_number(number_vector.back()));
509 for(std::size_t i=number_vector.size()-1; i>0; --i)
510 {
511 result = sort_nat::concat_digit(result,machine_number(number_vector.at(i-1)));
512 }
513 return result;
514#else
515 std::vector< char > number_as_vector(detail::string_to_vector_number(n));
516
517 std::vector< bool > bits;
518
519 while (0 < number_as_vector.size() && !((number_as_vector.size() == 1) && number_as_vector[0] == 1)) // number != 1
520 {
521 bits.push_back((static_cast< int >(*number_as_vector.rbegin()) % 2 != 0));
522
523 detail::decimal_number_divide_by_two(number_as_vector);
524 }
525 return (n == "0") ? sort_nat::c0() : static_cast< data_expression const& >(sort_nat::cnat(sort_pos::pos(n)));
526#endif
527}
528
532{
533#ifdef MCRL2_ENABLE_MACHINENUMBERS
536 ||
539 );
540#else
544 );
545#endif
546}
547
552inline std::string natural_constant_as_string(const data_expression& n_in)
553{
554#ifdef MCRL2_ENABLE_MACHINENUMBERS
555 std::vector<std::size_t> number_vector;
556 data_expression n=n_in;
557
559 {
560 number_vector.push_back(atermpp::down_cast<machine_number>(sort_nat::arg2(n)).value());
561 n = sort_nat::arg1(n);
562 }
563
565 number_vector.push_back(atermpp::down_cast<machine_number>(sort_nat::arg(n)).value());
566
567 if (detail::is_zero_number_vector(number_vector))
568 {
569 return "0";
570 }
571
572 return detail::number_vector_as_string(number_vector);
573#else
574 assert(is_natural_constant(n_in));
576 {
577 return "0";
578 }
579 else
580 {
582 }
583#endif
584}
585
590template <class NUMERIC_TYPE>
591inline NUMERIC_TYPE natural_constant_to_value(const data_expression& n)
592{
593#ifdef MCRL2_ENABLE_MACHINENUMBERS
594 if constexpr (std::is_integral<NUMERIC_TYPE>::value)
595 {
597 {
598 mcrl2::runtime_error("Number " + pp(n) + " is too large to transform to a machine number.");
599 }
601 return atermpp::down_cast<machine_number>(sort_nat::arg(n)).value();
602 }
603 else
604 {
606 {
607 return natural_constant_to_value<NUMERIC_TYPE>(sort_nat::arg1(n))*pow(2.0,64) +
608 atermpp::down_cast<machine_number>(sort_nat::arg2(n)).value();
609 }
611 return atermpp::down_cast<machine_number>(sort_nat::arg(n)).value();
612 }
613#else
614 assert(is_natural_constant(n));
616 {
617 return static_cast<NUMERIC_TYPE>(0);
618 }
619 else
620 {
621 return sort_pos::positive_constant_to_value<NUMERIC_TYPE>(sort_nat::arg(n));
622 }
623#endif
624}
625
626#ifdef MCRL2_ENABLE_MACHINENUMBERS
629inline data_expression transform_positive_constant_to_nat(const data_expression& n)
630{
631 assert(n.sort()==sort_pos::pos());
633 {
634 return sort_nat::concat_digit(transform_positive_constant_to_nat(sort_pos::arg1(n)),sort_nat::arg2(n));
635 }
636
639}
640
643inline data_expression transform_positive_number_to_nat(const data_expression& n)
644{
646 {
647 return transform_positive_constant_to_nat(n);
648 }
649 if (is_function_symbol(n))
650 {
651 const function_symbol& f=atermpp::down_cast<function_symbol>(n);
652 const std::string& name(f.name());
653 if (name.find_first_not_of("-/0123456789") == std::string::npos) // crude but efficient
654 {
655 return sort_nat::nat(name);
656 }
657 }
658 return application(sort_nat::pos2nat(),n);
659}
660#endif
661
662} // namespace sort_nat
663
664namespace sort_int
665{
666
668template < typename T >
669inline typename std::enable_if< std::is_integral< T >::value && std::is_unsigned< T >::value, data_expression >::type
671{
672 return sort_int::cint(sort_nat::nat(t));
673}
674
676template < typename T >
677inline typename std::enable_if< std::is_integral< T >::value && std::is_signed< T >::value, data_expression >::type
679{
680 if (t<0)
681 {
682 return sort_int::cneg(sort_pos::pos(typename std::make_unsigned<T>::type(-t)));
683 }
684 return sort_int::cint(sort_nat::nat(typename std::make_unsigned<T>::type(t)));
685}
686
690inline data_expression int_(const std::string& n)
691{
692 if (n[0] == '-')
693 {
694 return sort_int::cneg(sort_pos::pos(n.substr(1)));
695 }
696 return sort_int::cint(sort_nat::nat(n));
697}
698
702{
707 );
708}
709
714inline std::string integer_constant_as_string(const data_expression& n)
715{
716 assert(is_integer_constant(n));
718 {
720 }
721 else
722 {
724 }
725}
726
731template <class NUMERIC_VALUE>
732inline NUMERIC_VALUE integer_constant_to_value(const data_expression& n)
733{
734 assert(is_integer_constant(n));
736 {
737 return sort_nat::natural_constant_to_value<NUMERIC_VALUE>(sort_int::arg(n));
738 }
739 else
740 {
741 return -sort_pos::positive_constant_to_value<NUMERIC_VALUE>(sort_int::arg(n));
742 }
743}
744} // namespace sort_int
745
746namespace sort_real
747{
750template < typename T >
751inline typename std::enable_if< std::is_integral< T >::value, data_expression >::type
753{
754#ifdef MCRL2_ENABLE_MACHINENUMBERS
756#else
758#endif
759}
760
764template < typename T >
765inline typename std::enable_if< std::is_integral< T >::value, data_expression >::type
766real_(T numerator, T denominator)
767{
768 return sort_real::creal(sort_int::int_(numerator), sort_pos::pos(denominator));
769}
770
775inline data_expression real_(const std::string& numerator, const std::string& denominator)
776{
777 return sort_real::creal(sort_int::int_(numerator), sort_pos::pos(denominator));
778}
779
783inline data_expression real_(const std::string& n)
784{
785#ifdef MCRL2_ENABLE_MACHINENUMBERS
787#else
789#endif
790}
791
794template <class NUMERIC_TYPE>
795inline NUMERIC_TYPE value(const data_expression& r, typename std::enable_if<std::is_floating_point<NUMERIC_TYPE>::value>::type* = nullptr)
796{
798 {
799 const application& a = atermpp::down_cast<application>(r);
800 return sort_int::integer_constant_to_value<NUMERIC_TYPE>(a[0]) /
801 sort_pos::positive_constant_to_value<NUMERIC_TYPE>(a[1]);
802 }
803 throw runtime_error("Expected a closed term of type real " + pp(r) + ".");
804}
805
806} // namespace sort_real
807
812inline data_expression number(const sort_expression& s, const std::string& n)
813{
814 if (s == sort_pos::pos())
815 {
816 return sort_pos::pos(n);
817 }
818 else if (s == sort_nat::nat())
819 {
820 return sort_nat::nat(n);
821 }
822 else if (s == sort_int::int_())
823 {
824 return sort_int::int_(n);
825 }
826
827 return sort_real::real_(n);
828}
829
834inline bool is_convertible(const sort_expression& s1, const sort_expression& s2)
835{
836 if (s1 != s2)
837 {
838 if (s2 == sort_real::real_())
839 {
840 return s1 == sort_int::int_() || s1 == sort_nat::nat() || s1 == sort_pos::pos();
841 }
842 else if (s2 == sort_int::int_())
843 {
844 return s1 == sort_nat::nat() || s1 == sort_pos::pos();
845 }
846 else if (s2 == sort_nat::nat())
847 {
848 return s1 == sort_pos::pos();
849 }
850
851 return false;
852 }
853
854 return true;
855}
856
857} // namespace data
858
859} // namespace mcrl2
860
861#endif
862
size_type size() const
Returns the number of arguments of this term.
Definition aterm.h:151
void swap(unprotected_aterm_core &t) noexcept
Swaps this term with its argument.
Definition aterm_core.h:152
An application of a data expression to a number of arguments.
sort_expression sort() const
Returns the sort of the data expression.
Definition data.cpp:108
const_iterator end() const
const_iterator begin() const
\brief A machine number
\brief A sort expression
Standard exception class for reporting runtime errors.
Definition exception.h:27
const basic_sort & bool_()
Constructor for sort expression Bool.
Definition bool.h:44
bool is_boolean_constant(data_expression const &b)
Determines whether b is a Boolean constant.
bool is_true_function_symbol(const atermpp::aterm &e)
Recogniser for function true.
Definition bool.h:87
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition int1.h:1492
bool is_cneg_application(const atermpp::aterm &e)
Recogniser for application of @cNeg.
Definition int1.h:186
const function_symbol & cneg()
Constructor for function symbol @cNeg.
Definition int1.h:142
bool is_cint_application(const atermpp::aterm &e)
Recogniser for application of @cInt.
Definition int1.h:124
bool is_integer_constant(const data_expression &n)
Determines whether n is an integer constant.
std::string integer_constant_as_string(const data_expression &n)
Return the string representation of an integer number.
const function_symbol & cint()
Constructor for function symbol @cInt.
Definition int1.h:80
NUMERIC_VALUE integer_constant_to_value(const data_expression &n)
Return the NUMERIC_VALUE representation of an integer number.
const basic_sort & int_()
Constructor for sort expression Int.
Definition int1.h:47
const function_symbol & c0()
Constructor for function symbol @c0.
Definition nat1.h:108
bool is_cnat_application(const atermpp::aterm &e)
Recogniser for application of @cNat.
Definition nat1.h:184
function_symbol concat_digit(const sort_expression &s0, const sort_expression &s1)
Definition nat64.h:361
const function_symbol & cnat()
Constructor for function symbol @cNat.
Definition nat1.h:140
const basic_sort & nat()
Constructor for sort expression Nat.
Definition nat1.h:46
std::string natural_constant_as_string(const data_expression &n_in)
Return the string representation of a natural number.
bool is_c0_function_symbol(const atermpp::aterm &e)
Recogniser for function @c0.
Definition nat1.h:118
const function_symbol & most_significant_digit_nat()
Constructor for function symbol @most_significant_digitNat.
Definition nat64.h:301
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition nat1.h:2233
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition nat1.h:2221
bool is_concat_digit_application(const atermpp::aterm &e)
Recogniser for application of @concat_digit.
Definition nat64.h:422
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition nat1.h:2209
NUMERIC_TYPE natural_constant_to_value(const data_expression &n)
Return the NUMERIC_VALUE representation of a natural number.
const function_symbol & pos2nat()
Constructor for function symbol Pos2Nat.
Definition nat1.h:300
bool is_natural_constant(const data_expression &n)
Determines whether n is a natural constant.
bool is_most_significant_digit_nat_application(const atermpp::aterm &e)
Recogniser for application of @most_significant_digitNat.
Definition nat64.h:345
std::string positive_constant_as_string(const data_expression &n_in)
Return the string representation of a positive number.
const data_expression & arg(const data_expression &e)
Function for projecting out argument. arg from an application.
Definition pos1.h:788
bool is_positive_constant(const data_expression &n)
Determines whether n is a positive constant.
const function_symbol & c1()
Constructor for function symbol @c1.
Definition pos1.h:78
const data_expression & arg1(const data_expression &e)
Function for projecting out argument. arg1 from an application.
Definition pos1.h:800
bool is_cdub_application(const atermpp::aterm &e)
Recogniser for application of @cDub.
Definition pos1.h:156
bool is_c1_function_symbol(const atermpp::aterm &e)
Recogniser for function @c1.
Definition pos1.h:88
const data_expression & arg2(const data_expression &e)
Function for projecting out argument. arg2 from an application.
Definition pos1.h:812
const function_symbol & cdub()
Constructor for function symbol @cDub.
Definition pos1.h:110
const data_expression & right(const data_expression &e)
Function for projecting out argument. right from an application.
Definition pos1.h:776
const function_symbol & concat_digit()
Constructor for function symbol @concat_digit.
Definition pos64.h:267
bool is_most_significant_digit_application(const atermpp::aterm &e)
Recogniser for application of @most_significant_digit.
Definition pos64.h:249
bool is_concat_digit_application(const atermpp::aterm &e)
Recogniser for application of @concat_digit.
Definition pos64.h:313
const function_symbol & most_significant_digit()
Constructor for function symbol @most_significant_digit.
Definition pos64.h:205
const basic_sort & pos()
Constructor for sort expression Pos.
Definition pos1.h:45
NUMERIC_TYPE positive_constant_to_value(const data_expression &n)
Returns the NUMERIC_TYPE representation of a positive number.
const data_expression & left(const data_expression &e)
Function for projecting out argument. left from an application.
Definition pos1.h:764
const function_symbol & creal()
Constructor for function symbol @cReal.
Definition real1.h:107
bool is_creal_application(const atermpp::aterm &e)
Recogniser for application of @cReal.
Definition real1.h:153
NUMERIC_TYPE value(const data_expression &r, typename std::enable_if< std::is_floating_point< NUMERIC_TYPE >::value >::type *=nullptr)
Yields the real value of a data expression.
const basic_sort & real_()
Constructor for sort expression Real.
Definition real1.h:48
bool is_convertible(const sort_expression &s1, const sort_expression &s2)
Returns true if and only if s1 == s2, or if s1 is a less specific numeric type than s2.
data_expression number(const sort_expression &s, const std::string &n)
Construct numeric expression from a string representing a number in decimal notation.
std::string pp(const abstraction &x)
Definition data.cpp:39
bool is_zero(const data_expression &e)
bool is_function_symbol(const atermpp::aterm &x)
Returns true if the term t is a function symbol.
bool is_machine_number(const atermpp::aterm &x)
Returns true if the term t is a machine_number.
const core::identifier_string & name(const pbes_expression &t)
Returns the name of a propositional variable expression.
A class that takes a linear process specification and checks all tau-summands of that LPS for conflue...
Definition indexed_set.h:72
Provides utilities for working with data expressions of standard sorts.