Line data Source code
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 : //
9 : /// \file utility_test.cpp
10 : /// \brief Basic regression test for sort expressions.
11 :
12 : #define BOOST_TEST_MODULE utility_test
13 : #include <boost/test/included/unit_test.hpp>
14 :
15 : #include "mcrl2/data/parse.h"
16 : #include "mcrl2/data/rewriter.h"
17 : #include "mcrl2/data/standard_container_utility.h"
18 :
19 : using namespace mcrl2;
20 : using namespace mcrl2::data;
21 :
22 : template < typename Rewriter >
23 15 : void representation_check(Rewriter& R, data_expression const& input, data_expression const& expected, const data_specification& spec)
24 : {
25 30 : data_expression output(R(normalize_sorts(input,spec)));
26 :
27 15 : BOOST_CHECK(normalize_sorts(expected,spec) == output);
28 :
29 15 : if (output != normalize_sorts(expected,spec))
30 : {
31 0 : std::clog << "--- test failed --- " << data::pp(input) << " ->* " << data::pp(expected) << std::endl
32 0 : << "input " << data::pp(input) << std::endl
33 0 : << "expected " << data::pp(expected) << std::endl
34 0 : << "R(input) " << data::pp(output) << std::endl
35 0 : << " -- term representations -- " << std::endl
36 0 : << "input " << input << std::endl
37 0 : << "expected " << normalize_sorts(expected,spec)<< std::endl
38 0 : << "R(input) " << normalize_sorts(output,spec) << std::endl;
39 : }
40 15 : }
41 :
42 1 : void number_test()
43 : {
44 : using namespace sort_bool;
45 : using namespace sort_pos;
46 : using namespace sort_nat;
47 : using namespace sort_int;
48 : using namespace sort_real;
49 :
50 1 : BOOST_CHECK(data::detail::as_decimal_string(1) == "1");
51 1 : BOOST_CHECK(data::detail::as_decimal_string(2) == "2");
52 1 : BOOST_CHECK(data::detail::as_decimal_string(3) == "3");
53 1 : BOOST_CHECK(data::detail::as_decimal_string(4) == "4");
54 1 : BOOST_CHECK(data::detail::as_decimal_string(144) == "144");
55 :
56 : // Test character array arithmetic
57 1 : std::vector< char > numbers;
58 1 : numbers = data::detail::string_to_vector_number("1");
59 1 : BOOST_CHECK(data::detail::vector_number_to_string(numbers) == "1");
60 :
61 1 : data::detail::decimal_number_multiply_by_two(numbers);
62 1 : BOOST_CHECK(data::detail::vector_number_to_string(numbers) == "2");
63 :
64 1 : data::detail::decimal_number_increment(numbers);
65 1 : BOOST_CHECK(data::detail::vector_number_to_string(numbers) == "3");
66 :
67 1 : data::detail::decimal_number_increment(numbers);
68 1 : BOOST_CHECK(data::detail::vector_number_to_string(numbers) == "4");
69 :
70 1 : data::detail::decimal_number_multiply_by_two(numbers);
71 1 : BOOST_CHECK(data::detail::vector_number_to_string(numbers) == "8");
72 :
73 1 : data::detail::decimal_number_multiply_by_two(numbers);
74 1 : BOOST_CHECK(data::detail::vector_number_to_string(numbers) == "16");
75 :
76 1 : data::detail::decimal_number_divide_by_two(numbers);
77 1 : BOOST_CHECK(data::detail::vector_number_to_string(numbers) == "8");
78 :
79 1 : BOOST_CHECK(sort_pos::positive_constant_as_string(number(sort_pos::pos(), "1")) == "1");
80 1 : BOOST_CHECK(sort_pos::positive_constant_as_string(number(sort_pos::pos(), "10")) == "10");
81 1 : BOOST_CHECK(sort_nat::natural_constant_as_string(number(sort_nat::nat(), "0")) == "0");
82 1 : BOOST_CHECK(sort_nat::natural_constant_as_string(number(sort_nat::nat(), "1")) == "1");
83 1 : BOOST_CHECK(sort_nat::natural_constant_as_string(number(sort_nat::nat(), "10")) == "10");
84 1 : BOOST_CHECK(sort_int::integer_constant_as_string(number(sort_int::int_(), "-10")) == "-10");
85 1 : BOOST_CHECK(sort_int::integer_constant_as_string(number(sort_int::int_(), "10")) == "10");
86 :
87 2 : data_specification specification = parse_data_specification("sort A = Real;");
88 :
89 1 : mcrl2::data::rewriter R(specification);
90 :
91 1 : representation_check(R, number(sort_pos::pos(), "1"), sort_pos::c1(),specification);
92 1 : representation_check(R, number(sort_nat::nat(), "1"), R(normalize_sorts(pos2nat(sort_pos::c1()),specification)),specification);
93 1 : representation_check(R, number(sort_int::int_(), "-1"), R(cneg(sort_pos::c1())),specification);
94 1 : representation_check(R, normalize_sorts(number(sort_real::real_(), "1"),specification), R(normalize_sorts(pos2real(sort_pos::c1()),specification)),specification);
95 :
96 1 : representation_check(R, pos("11"), cdub(true_(), cdub(true_(), cdub(false_(), c1()))),specification);
97 1 : representation_check(R, pos(12), cdub(false_(), cdub(false_(), cdub(true_(), c1()))),specification);
98 1 : representation_check(R, nat("18"), R(normalize_sorts(pos2nat(cdub(false_(), cdub(true_(), cdub(false_(), cdub(false_(), c1()))))),specification)),specification);
99 1 : representation_check(R, nat(12), R(normalize_sorts(pos2nat(cdub(false_(), cdub(false_(), cdub(true_(), c1())))),specification)),specification);
100 1 : representation_check(R, int_("0"), R(nat2int(c0())),specification);
101 1 : representation_check(R, int_("-1"), cneg(c1()),specification);
102 1 : representation_check(R, int_(-2), cneg(cdub(false_(), c1())),specification);
103 1 : representation_check(R, real_("0"), R(normalize_sorts(nat2real(c0()),specification)),specification);
104 1 : representation_check(R, real_("-1"), R(normalize_sorts(int2real(cneg(c1())),specification)),specification);
105 1 : representation_check(R, real_(-2), R(normalize_sorts(int2real(cneg(cdub(false_(), c1()))),specification)),specification);
106 :
107 1 : }
108 :
109 1 : void list_construction_test()
110 : {
111 : using namespace mcrl2::data::sort_list;
112 : using namespace mcrl2::data::sort_bool;
113 :
114 1 : data_expression_vector expressions;
115 :
116 1 : expressions.push_back(true_());
117 1 : expressions.push_back(false_());
118 1 : expressions.push_back(true_());
119 1 : expressions.push_back(false_());
120 :
121 1 : data_specification specification;
122 :
123 1 : mcrl2::data::rewriter R(specification, jitty);
124 :
125 1 : representation_check(R, sort_list::list(bool_(), expressions),
126 2 : R(cons_(bool_(), expressions[0], cons_(bool_(), expressions[1],
127 2 : cons_(bool_(), expressions[2], cons_(bool_(), expressions[3], empty(bool_())))))),specification);
128 1 : }
129 :
130 1 : void convert_test()
131 : {
132 1 : std::vector< data_expression > l;
133 :
134 1 : l.push_back(sort_bool::true_());
135 :
136 1 : atermpp::aterm_list al(l.begin(),l.end());
137 :
138 1 : BOOST_CHECK(l.size() == al.size());
139 1 : }
140 :
141 2 : BOOST_AUTO_TEST_CASE(test_main)
142 : {
143 1 : number_test();
144 :
145 1 : list_construction_test();
146 :
147 1 : convert_test();
148 1 : }
149 :
|
