Line data Source code
1 : // Author(s): Wieger Wesselink
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 rewriter_test.cpp
10 : /// \brief Add your file description here.
11 :
12 : #define BOOST_TEST_MODULE rewriter_test
13 : #include "mcrl2/data/detail/one_point_rule_preprocessor.h"
14 : #include "mcrl2/data/detail/parse_substitution.h"
15 : #include "mcrl2/data/detail/test_rewriters.h"
16 : #include "mcrl2/data/print.h"
17 : #include "mcrl2/data/rewriter.h"
18 : #include "mcrl2/data/rewriters/simplify_rewriter.h"
19 :
20 : #include <boost/test/included/unit_test.hpp>
21 :
22 : using namespace mcrl2;
23 : using namespace mcrl2::core;
24 : using namespace mcrl2::data;
25 :
26 1 : data::rewriter make_data_rewriter(const data_specification& data_spec)
27 : {
28 1 : data::rewriter datar(data_spec);
29 1 : return datar;
30 : }
31 :
32 : struct A
33 : {
34 : data::rewriter& r_;
35 :
36 2 : A(data::rewriter& r)
37 2 : : r_(r)
38 2 : { }
39 : };
40 :
41 1 : A make_A(data::rewriter& d)
42 : {
43 1 : A result(d);
44 1 : return result;
45 : }
46 :
47 1 : void test1()
48 : {
49 : using namespace mcrl2::data::sort_nat;
50 :
51 : std::string DATA_SPEC1 =
52 1 : "sort D = struct d1(Nat)?is_d1 | d2(arg2:Nat)?is_d2;\n"
53 : ;
54 1 : data_specification data = parse_data_specification(DATA_SPEC1);
55 1 : rewriter datar(data);
56 2 : variable x("x", sort_nat::nat());
57 2 : variable y("y", sort_nat::nat());
58 2 : variable z("z", sort_nat::nat());
59 2 : data_expression t = datar(greater(minimum(x,y), z));
60 :
61 1 : BOOST_CHECK(datar(plus(parse_data_expression("1"),
62 : parse_data_expression("2"))) == datar(parse_data_expression("3")));
63 :
64 : // copy a rewriter
65 1 : data::rewriter datar1 = datar;
66 1 : t = datar1(greater(minimum(x,y), z));
67 :
68 : // rewriter as return value
69 1 : data::rewriter datar2 = make_data_rewriter(data);
70 1 : t = datar2(greater(minimum(x,y), z));
71 :
72 1 : A a(datar);
73 1 : data_expression qa = a.r_(t);
74 :
75 1 : A b = a;
76 1 : data_expression qb = b.r_(t);
77 :
78 1 : A c = make_A(datar);
79 1 : data_expression qc = c.r_(t);
80 1 : }
81 :
82 1 : void test2()
83 : {
84 : using namespace mcrl2::data::sort_nat;
85 :
86 1 : data_specification data_spec;
87 :
88 1 : data_spec.add_context_sort(nat());
89 :
90 1 : rewriter r(data_spec);
91 2 : data_expression d1 = parse_data_expression("2+7");
92 2 : data_expression d2 = parse_data_expression("4+5");
93 1 : BOOST_CHECK(r(d1) == r(d2));
94 :
95 2 : data::variable_list variables = parse_variables("m, n: Pos;");
96 1 : data::rewriter::substitution_type sigma;
97 1 : sigma[atermpp::down_cast<variable>(parse_data_expression("m", variables))] = r(parse_data_expression("3"));
98 1 : sigma[atermpp::down_cast<variable>(parse_data_expression("n", variables))] = r(parse_data_expression("4"));
99 :
100 : // Rewrite two data expressions, and check if they are the same
101 1 : d1 = parse_data_expression("m+n", variables);
102 1 : d2 = parse_data_expression("7");
103 1 : BOOST_CHECK(r(d1, sigma) == r(d2));
104 1 : }
105 :
106 : template <typename Rewriter>
107 5 : void test_expressions(Rewriter R, std::string const& expr1, std::string const& expr2, std::string const& declarations, const data_specification& data_spec, const std::string& substitution_text)
108 : {
109 5 : data::rewriter::substitution_type sigma;
110 5 : data::detail::parse_substitution(substitution_text, sigma, data_spec);
111 5 : data_expression d1 = parse_data_expression(expr1, parse_variables(declarations), data_spec);
112 5 : data_expression d2 = parse_data_expression(expr2, parse_variables(declarations), data_spec);
113 5 : data_expression rd1 = R(d1, sigma);
114 5 : data_expression rd2 = R(d2);
115 5 : if (rd1 != rd2)
116 : {
117 0 : BOOST_CHECK(rd1 == rd2);
118 0 : std::cout << "--- failed test --- " << expr1 << " -> " << expr2 << std::endl;
119 0 : std::cout << "d1 " << d1 << std::endl;
120 0 : std::cout << "d2 " << d2 << std::endl;
121 0 : std::cout << "sigma\n " << sigma << std::endl;
122 0 : std::cout << "R(d1, sigma) " << rd1 << std::endl;
123 0 : std::cout << "R(d2) " << rd2 << std::endl;
124 : }
125 5 : }
126 :
127 1 : void test4()
128 : {
129 1 : data_specification data_spec;
130 :
131 1 : data::rewriter R(data_spec);
132 :
133 1 : std::string expr1 = "exists b: Bool. if(c, c, b)";
134 1 : std::string expr2 = "exists b: Bool. if(true, true, b)";
135 1 : std::string sigma = "[c: Bool := true]";
136 1 : test_expressions(R, expr1, expr2, "c: Bool;", data_spec, sigma);
137 1 : }
138 :
139 1 : void test5() // Test set difference for finite sets.
140 : {
141 : std::string DATA_SPEC1 =
142 : "map f,g:FSet(Bool);\n"
143 : "eqn f=({false}-{true})-{false};\n"
144 1 : " g={};\n"
145 : ;
146 1 : data_specification data_spec = parse_data_specification(DATA_SPEC1);
147 1 : data::rewriter R(data_spec);
148 :
149 1 : std::string expr1 = "f";
150 1 : std::string expr2 = "g";
151 1 : std::string sigma = "[c: Bool := true]";
152 1 : test_expressions(R, expr1, expr2, "c: Bool;", data_spec, sigma);
153 1 : }
154 :
155 0 : void allocation_test()
156 : {
157 0 : data_specification data_spec;
158 0 : std::shared_ptr< data::rewriter > R_heap(new data::rewriter(data_spec));
159 0 : data::rewriter R_stack(data_spec);
160 :
161 0 : R_stack(parse_data_expression("1 == 2"));
162 0 : R_stack(parse_data_expression("1 == 2"));
163 :
164 0 : (*R_heap)(parse_data_expression("1 == 2"));
165 0 : (*R_heap)(parse_data_expression("1 == 2"));
166 0 : }
167 :
168 1 : void one_point_rule_preprocessor_test()
169 : {
170 : using namespace data::detail;
171 :
172 1 : test_rewriters(N(one_point_rule_preprocessor()), N(I), "!(true && false)", "!(true) || !(false)");
173 1 : test_rewriters(N(one_point_rule_preprocessor()), N(I), "!!b", "b");
174 1 : test_rewriters(N(one_point_rule_preprocessor()), N(I), "!!!!b", "b");
175 1 : test_rewriters(N(one_point_rule_preprocessor()), N(I), "!(b1 && b2 && b3)", "!b1 || !b2 || !b3");
176 1 : test_rewriters(N(one_point_rule_preprocessor()), N(I), "!(b1 || b2 || b3)", "!b1 && !b2 && !b3");
177 1 : test_rewriters(N(one_point_rule_preprocessor()), N(I), "!(b1 == b2)", "b1 != b2");
178 1 : test_rewriters(N(one_point_rule_preprocessor()), N(I), "!(b1 != b2)", "b1 == b2");
179 1 : test_rewriters(N(one_point_rule_preprocessor()), N(I), "!(b1 == b2 && b1 == b3)", "b1 != b2 || b1 != b3");
180 1 : test_rewriters(N(one_point_rule_preprocessor()), N(I), "!(b1 != b2 || b1 != b3)", "b1 == b2 && b1 == b3");
181 1 : test_rewriters(N(one_point_rule_preprocessor()), N(I), "!(n1 != n2 || n1 != n2 + 1)", "n1 == n2 && n1 == n2 + 1");
182 1 : }
183 :
184 1 : void simplify_rewriter_test()
185 : {
186 : using data::detail::N;
187 : using data::detail::I;
188 :
189 : data::simplify_rewriter R;
190 1 : test_rewriters(N(R), N(I), "!(true && false)", "true");
191 1 : test_rewriters(N(R), N(I), "exists n:Nat, b:Bool. b", "exists b:Bool. b");
192 1 : test_rewriters(N(R), N(I), "forall b:Bool. !!b", "forall b:Bool. b");
193 1 : }
194 :
195 : // The testcase below corresponds to ticket #1426.
196 1 : void test_lambda_expression()
197 : {
198 1 : data_specification data_spec;
199 1 : data::rewriter R(data_spec);
200 :
201 1 : std::string expr1 = "(lambda t: Real. true)(t) && (lambda s1: Pos, t: Real. 1 == s1)(2, u)";
202 1 : std::string expr2 = "false";
203 1 : std::string sigma = "[]";
204 1 : test_expressions(R, expr1, expr2, "t,u: Real;", data_spec, sigma);
205 1 : }
206 :
207 : // The testcase below corresponds to ticket #1428 which indicated
208 : // that the generated rules for equality were erroneous. Their bound variables were equal
209 : // f == g = forall x0,x0: Nat. f(x0, x0) == g(x0, x0)
210 1 : void test_equality_on_functions()
211 : {
212 : std::string DATA_SPEC1 =
213 : "map f,g:Nat#Nat->Nat;\n"
214 : "var x,y:Nat; \n"
215 : "eqn f(x,y) = x+y;\n"
216 1 : " g(x,y) = x+x;\n"
217 : ;
218 :
219 1 : data_specification data_spec = parse_data_specification(DATA_SPEC1);
220 1 : data::rewriter R(data_spec);
221 :
222 1 : std::string expr1 = "f==g";
223 1 : std::string expr2 = "false";
224 1 : std::string sigma = "[]";
225 1 : test_expressions(R, expr1, expr2, "", data_spec, sigma);
226 1 : }
227 :
228 : // The testcase below corresponds to ticket #1461 which indicated
229 : // that rewriting enumerated functions failed as the if function would be removed
230 : // from the rewriters if it does not occur explicitly in the specification.
231 1 : void test_enumeration_of_functions()
232 : {
233 : std::string DATA_SPEC1 =
234 1 : "sort Hat = struct black | white;"
235 : ;
236 :
237 1 : data_specification data_spec = parse_data_specification(DATA_SPEC1);
238 : // For this test it is essential that unnecessary equations are removed.
239 2 : data::rewriter R(data_spec,used_data_equation_selector(data_spec,std::set<function_symbol>()));
240 :
241 1 : std::string expr1 = "exists f:Hat->Hat.f(black)!=f(white)";
242 1 : std::string expr2 = "true";
243 1 : std::string sigma = "[]";
244 1 : test_expressions(R, expr1, expr2, "", data_spec, sigma);
245 1 : }
246 :
247 2 : BOOST_AUTO_TEST_CASE(test_main)
248 : {
249 1 : test1();
250 1 : test2();
251 1 : test4();
252 1 : test5();
253 1 : one_point_rule_preprocessor_test();
254 1 : simplify_rewriter_test();
255 1 : test_lambda_expression();
256 1 : test_equality_on_functions();
257 1 : test_enumeration_of_functions();
258 1 : }
|
