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 rewriting_test.cpp
10 : /// \brief Tests whether terms are correctly rewritten using various rewriters.
11 :
12 : #define BOOST_TEST_MODULE rewriting_test
13 : #include "mcrl2/data/bag.h"
14 : #include "mcrl2/data/detail/rewrite_strategies.h"
15 : #include "mcrl2/data/list.h"
16 : #include "mcrl2/data/parse.h"
17 : #include "mcrl2/data/rewriter.h"
18 :
19 : #include <boost/test/included/unit_test.hpp>
20 :
21 : using namespace mcrl2;
22 : using namespace mcrl2::core;
23 : using namespace mcrl2::data;
24 :
25 : typedef std::vector<rewrite_strategy > rewrite_strategy_vector;
26 :
27 : template <typename Rewriter>
28 274 : void data_rewrite_test(Rewriter& R, const data_expression& input, const data_expression& expected_output)
29 : {
30 274 : data_expression output = R(input);
31 :
32 274 : BOOST_CHECK(output == expected_output);
33 :
34 274 : if (output != expected_output)
35 : {
36 0 : std::cerr << "--- test failed --- " << data::pp(input) << " ->* " << data::pp(expected_output) << std::endl
37 0 : << "input " << data::pp(input) << std::endl
38 0 : << "expected " << data::pp(expected_output) << std::endl
39 0 : << "output " << data::pp(output) << std::endl
40 0 : << " -- term representations -- " << std::endl
41 0 : << "input " << atermpp::aterm(input) << std::endl
42 0 : << "expected " << atermpp::aterm(expected_output) << std::endl
43 0 : << "R(input) " << atermpp::aterm(output) << std::endl;
44 : }
45 274 : }
46 :
47 2 : BOOST_AUTO_TEST_CASE(bool_rewrite_test)
48 : {
49 : using namespace mcrl2::data::sort_bool;
50 :
51 1 : data_specification specification;
52 :
53 1 : specification.add_context_sort(bool_());
54 :
55 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
56 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
57 : {
58 1 : std::cerr << " Strategy1: " << *strat << std::endl;
59 1 : data::rewriter R(specification, *strat);
60 :
61 1 : data_rewrite_test(R, true_(), true_());
62 1 : data_rewrite_test(R, false_(), false_());
63 :
64 1 : data_rewrite_test(R, and_(true_(), false_()), false_());
65 1 : data_rewrite_test(R, and_(false_(), true_()), false_());
66 :
67 1 : data_rewrite_test(R, or_(true_(), false_()), true_());
68 1 : data_rewrite_test(R, or_(false_(), true_()), true_());
69 :
70 1 : data_rewrite_test(R, implies(true_(), false_()), false_());
71 1 : data_rewrite_test(R, implies(false_(), true_()), true_());
72 :
73 1 : data::variable_vector v;
74 1 : v.push_back(data::variable("b", bool_()));
75 1 : v.push_back(data::variable("c", bool_()));
76 2 : data::data_expression e(parse_data_expression("b&&(b&&c)", v));
77 1 : data_rewrite_test(R, e, e);
78 1 : }
79 :
80 1 : }
81 :
82 2 : BOOST_AUTO_TEST_CASE(pos_rewrite_test)
83 : {
84 : using namespace mcrl2::data::sort_pos;
85 1 : std::cerr << "pos_rewrite_test\n";
86 :
87 1 : data_specification specification;
88 :
89 1 : specification.add_context_sort(pos());
90 :
91 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
92 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
93 : {
94 1 : std::cerr << " Strategy2: " << *strat << std::endl;
95 1 : data::rewriter R(specification, *strat);
96 :
97 2 : data_expression p1(pos("1"));
98 2 : data_expression p2(pos("2"));
99 2 : data_expression p3(pos("3"));
100 2 : data_expression p4(pos("4"));
101 :
102 1 : data_rewrite_test(R, sort_pos::plus(p1, p2), p3);
103 1 : data_rewrite_test(R, sort_pos::plus(p2, p1), p3);
104 :
105 1 : data_rewrite_test(R, sort_pos::times(p1, p1), p1);
106 1 : data_rewrite_test(R, sort_pos::times(p1, p2), p2);
107 :
108 1 : data_rewrite_test(R, (sort_pos::minimum)(p1, p1), p1);
109 1 : data_rewrite_test(R, (sort_pos::minimum)(p1, p2), p1);
110 :
111 1 : data_rewrite_test(R, (sort_pos::maximum)(p1, p1), p1);
112 1 : data_rewrite_test(R, (sort_pos::maximum)(p1, p2), p2);
113 :
114 1 : data_rewrite_test(R, sort_pos::succ(p1), p2);
115 1 : }
116 1 : }
117 :
118 2 : BOOST_AUTO_TEST_CASE(nat_rewrite_test)
119 : {
120 : using namespace mcrl2::data::sort_nat;
121 1 : std::cerr << "nat_rewrite_test\n";
122 :
123 1 : data_specification specification;
124 :
125 1 : specification.add_context_sort(nat());
126 :
127 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
128 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
129 : {
130 1 : std::cerr << " Strategy3: " << *strat << std::endl;
131 1 : data::rewriter R(specification, *strat);
132 :
133 1 : data_expression p0(nat(0));
134 1 : data_expression p1(nat(1));
135 1 : data_expression p2(nat(2));
136 1 : data_expression p3(nat(3));
137 1 : data_expression p4(nat(4));
138 :
139 1 : data_rewrite_test(R, plus(p0, p2), p2);
140 1 : data_rewrite_test(R, plus(p2, p0), p2);
141 1 : data_rewrite_test(R, plus(p1, p2), p3);
142 1 : data_rewrite_test(R, plus(p2, p1), p3);
143 :
144 1 : data_rewrite_test(R, times(p1, p1), p1);
145 1 : data_rewrite_test(R, times(p0, p2), p0);
146 1 : data_rewrite_test(R, times(p2, p0), p0);
147 1 : data_rewrite_test(R, times(p1, p2), p2);
148 :
149 1 : data_rewrite_test(R, (minimum)(p1, p1), p1);
150 1 : data_rewrite_test(R, (minimum)(p0, p2), p0);
151 1 : data_rewrite_test(R, (minimum)(p2, p0), p0);
152 1 : data_rewrite_test(R, (minimum)(p1, p2), p1);
153 :
154 1 : data_rewrite_test(R, (maximum)(p1, p1), p1);
155 1 : data_rewrite_test(R, (maximum)(p0, p2), p2);
156 1 : data_rewrite_test(R, (maximum)(p2, p0), p2);
157 1 : data_rewrite_test(R, (maximum)(p1, p2), p2);
158 :
159 1 : data_rewrite_test(R, succ(p0), R(nat2pos(p1)));
160 1 : data_rewrite_test(R, succ(p1), R(nat2pos(p2)));
161 :
162 1 : data_rewrite_test(R, pred(nat2pos(p1)), p0);
163 1 : data_rewrite_test(R, pred(nat2pos(p2)), p1);
164 :
165 1 : data_rewrite_test(R, div(p0, sort_pos::pos(2)), p0);
166 1 : data_rewrite_test(R, div(p2, sort_pos::pos(1)), p2);
167 1 : data_rewrite_test(R, div(p4, sort_pos::pos(2)), p2);
168 :
169 1 : data_rewrite_test(R, mod(p1, nat2pos(p1)), p0);
170 1 : data_rewrite_test(R, mod(p0, nat2pos(p2)), p0);
171 1 : data_rewrite_test(R, mod(p2, nat2pos(p1)), p0);
172 1 : data_rewrite_test(R, mod(p4, nat2pos(p3)), p1);
173 :
174 1 : data_rewrite_test(R, exp(p2, p2), p4);
175 :
176 : // Added a few additional checks (Wieger)
177 1 : data::rewriter datar(specification);
178 2 : data::data_expression x = data::parse_data_expression("n >= 0", parse_variables("n:Nat;"));
179 :
180 1 : BOOST_CHECK(datar(x) == sort_bool::true_());
181 1 : data_rewrite_test(R, greater_equal(variable("n", nat()), p0), sort_bool::true_());
182 1 : }
183 1 : }
184 :
185 2 : BOOST_AUTO_TEST_CASE(int_rewrite_test)
186 : {
187 : using namespace mcrl2::data::sort_int;
188 1 : std::cerr << "int_rewrite_test\n";
189 :
190 1 : data_specification specification;
191 :
192 1 : specification.add_context_sort(int_());
193 :
194 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
195 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
196 : {
197 1 : std::cerr << " Strategy4: " << *strat << std::endl;
198 1 : data::rewriter R(specification, *strat);
199 :
200 1 : data_expression p0(int_(0));
201 1 : data_expression p1(int_(1));
202 1 : data_expression p2(int_(2));
203 1 : data_expression p3(int_(3));
204 1 : data_expression p4(int_(4));
205 :
206 1 : data_rewrite_test(R, plus(p0, p2), p2);
207 1 : data_rewrite_test(R, plus(p2, p0), p2);
208 1 : data_rewrite_test(R, plus(p1, p2), p3);
209 1 : data_rewrite_test(R, plus(p2, p1), p3);
210 1 : data_rewrite_test(R, plus(negate(p4), p4), p0);
211 1 : data_rewrite_test(R, minus(p4, p4), p0);
212 :
213 1 : data_rewrite_test(R, times(p1, p1), p1);
214 1 : data_rewrite_test(R, times(p0, p2), p0);
215 1 : data_rewrite_test(R, times(p2, p0), p0);
216 1 : data_rewrite_test(R, times(p1, p2), p2);
217 :
218 1 : data_rewrite_test(R, (minimum)(p1, p1), p1);
219 1 : data_rewrite_test(R, (minimum)(p0, p2), p0);
220 1 : data_rewrite_test(R, (minimum)(p2, p0), p0);
221 1 : data_rewrite_test(R, (minimum)(p1, p2), p1);
222 :
223 1 : data_rewrite_test(R, (maximum)(p1, p1), p1);
224 1 : data_rewrite_test(R, (maximum)(p0, p2), p2);
225 1 : data_rewrite_test(R, (maximum)(p2, p0), p2);
226 1 : data_rewrite_test(R, (maximum)(p1, p2), p2);
227 :
228 1 : data_rewrite_test(R, succ(p0), p1);
229 1 : data_rewrite_test(R, succ(p1), p2);
230 :
231 1 : data_rewrite_test(R, pred(p1), p0);
232 1 : data_rewrite_test(R, pred(p2), p1);
233 :
234 1 : data_rewrite_test(R, nat2int(abs(p1)), p1);
235 :
236 1 : data_rewrite_test(R, div(p1, int2pos(p1)), p1);
237 1 : data_rewrite_test(R, div(p0, int2pos(p2)), p0);
238 1 : data_rewrite_test(R, div(p2, int2pos(p1)), p2);
239 1 : data_rewrite_test(R, div(p4, int2pos(p2)), p2);
240 :
241 1 : data_rewrite_test(R, mod(p1, int2pos(p1)), R(int2nat(p0)));
242 1 : data_rewrite_test(R, mod(p0, int2pos(p2)), R(int2nat(p0)));
243 1 : data_rewrite_test(R, mod(p2, int2pos(p1)), R(int2nat(p0)));
244 1 : data_rewrite_test(R, mod(p4, int2pos(p3)), R(int2nat(p1)));
245 :
246 1 : data_rewrite_test(R, exp(p2, int2nat(p2)), p4);
247 1 : }
248 1 : }
249 :
250 2 : BOOST_AUTO_TEST_CASE(real_rewrite_test)
251 : {
252 : using namespace mcrl2::data::sort_real;
253 1 : std::cerr << "real_rewrite_test\n";
254 :
255 1 : data_specification specification;
256 1 : specification.add_context_sort(real_());
257 :
258 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
259 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
260 : {
261 1 : std::cerr << " Strategy5: " << *strat << std::endl;
262 1 : data::rewriter R(specification, *strat);
263 :
264 1 : data_expression p0(real_(0));
265 1 : data_expression p1(real_(1));
266 1 : data_expression p2(real_(2));
267 1 : data_expression p3(real_(3));
268 1 : data_expression p4(real_(4));
269 :
270 1 : data_rewrite_test(R, plus(p0, p2), p2);
271 1 : data_rewrite_test(R, plus(p2, p0), p2);
272 1 : data_rewrite_test(R, plus(p1, p2), p3);
273 1 : data_rewrite_test(R, plus(p2, p1), p3);
274 1 : data_rewrite_test(R, plus(negate(p4), p4), p0);
275 1 : data_rewrite_test(R, minus(p4, p4), p0);
276 :
277 1 : data_rewrite_test(R, times(p1, p1), p1);
278 1 : data_rewrite_test(R, times(p0, p2), p0);
279 1 : data_rewrite_test(R, times(p2, p0), p0);
280 1 : data_rewrite_test(R, times(p1, p2), p2);
281 :
282 1 : data_rewrite_test(R, (minimum)(p1, p1), p1);
283 1 : data_rewrite_test(R, (minimum)(p0, p2), p0);
284 1 : data_rewrite_test(R, (minimum)(p2, p0), p0);
285 1 : data_rewrite_test(R, (minimum)(p1, p2), p1);
286 :
287 1 : data_rewrite_test(R, (maximum)(p1, p1), p1);
288 1 : data_rewrite_test(R, (maximum)(p0, p2), p2);
289 1 : data_rewrite_test(R, (maximum)(p2, p0), p2);
290 1 : data_rewrite_test(R, (maximum)(p1, p2), p2);
291 :
292 1 : data_rewrite_test(R, succ(p0), p1);
293 1 : data_rewrite_test(R, succ(p1), p2);
294 :
295 1 : data_rewrite_test(R, pred(p1), p0);
296 1 : data_rewrite_test(R, pred(p2), p1);
297 :
298 1 : data_rewrite_test(R, abs(p1), p1);
299 :
300 1 : data_rewrite_test(R, divides(p1, p1), p1);
301 1 : data_rewrite_test(R, divides(p0, p2), p0);
302 1 : data_rewrite_test(R, divides(p2, p1), p2);
303 1 : data_rewrite_test(R, divides(p4, p2), p2);
304 :
305 1 : data_rewrite_test(R, exp(p2, real2int(p2)), p4);
306 :
307 1 : data_rewrite_test(R, int2real(floor(real_(29, 10))), p2);
308 :
309 1 : data_rewrite_test(R, int2real(ceil(real_(12, 10))), p2);
310 :
311 1 : data_rewrite_test(R, int2real(round(real_(16, 10))), p2);
312 1 : data_rewrite_test(R, int2real(round(real_(24, 10))), p2);
313 1 : }
314 1 : }
315 :
316 2 : BOOST_AUTO_TEST_CASE(list_rewrite_test)
317 : {
318 : using namespace mcrl2::data::sort_bool;
319 : using namespace mcrl2::data::sort_list;
320 1 : std::cerr << "list_rewrite_test\n";
321 1 : data_specification specification;
322 :
323 1 : specification.add_context_sort(list(bool_()));
324 :
325 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
326 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
327 : {
328 1 : std::cerr << " Strategy6: " << *strat << std::endl;
329 1 : data::rewriter R(specification, *strat);
330 :
331 1 : data_expression empty_(R(empty(bool_())));
332 1 : data_expression head_true(cons_(bool_(), true_(), empty_));
333 :
334 1 : data_rewrite_test(R, in(bool_(), true_(), head_true), true_());
335 1 : data_rewrite_test(R, in(bool_(), false_(), head_true), false_());
336 1 : data_rewrite_test(R, count(bool_(), head_true), sort_nat::nat(1));
337 1 : data_rewrite_test(R, in(bool_(), false_(), snoc(bool_(), head_true, true_())), false_());
338 1 : data_rewrite_test(R, concat(bool_(), head_true, head_true), R(cons_(bool_(), true_(), head_true)));
339 1 : data_rewrite_test(R, element_at(bool_(), head_true, sort_nat::nat(0)), true_());
340 1 : data_rewrite_test(R, head(bool_(), head_true), true_());
341 1 : data_rewrite_test(R, rhead(bool_(), head_true), true_());
342 1 : data_rewrite_test(R, rtail(bool_(), head_true), empty_);
343 1 : data_rewrite_test(R, tail(bool_(), head_true), empty_);
344 1 : }
345 1 : }
346 :
347 2 : BOOST_AUTO_TEST_CASE(struct_list_rewrite_test)
348 : {
349 : using namespace mcrl2::data::sort_bool;
350 : using namespace mcrl2::data::sort_list;
351 1 : std::cerr << "struct_list_rewrite_test\n";
352 : data_specification specification=parse_data_specification("sort L = struct l( R: List(Bool) );"
353 2 : "map f:Set(L);"); // Map is added to guarantee that rewrite rules for sets
354 : // are present.
355 :
356 :
357 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
358 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
359 : {
360 1 : std::cerr << " Strategy7: " << *strat << std::endl;
361 1 : data::rewriter R(specification, *strat);
362 :
363 2 : const data_expression e1=parse_data_expression("l( [true]) in {l( [])}",specification);
364 2 : const data_expression e2=parse_data_expression("l( [true]) in {l( [true])}",specification);
365 2 : const data_expression e3=parse_data_expression("l( [true]) in {l( [true]),l([false])}",specification);
366 2 : const data_expression e4=parse_data_expression("l( [true]) in {l([false])}",specification);
367 :
368 1 : data_rewrite_test(R, e1, false_());
369 1 : data_rewrite_test(R, e2, true_());
370 1 : data_rewrite_test(R, e3, true_());
371 1 : data_rewrite_test(R, e4, false_());
372 1 : }
373 1 : }
374 :
375 :
376 2 : BOOST_AUTO_TEST_CASE(set_rewrite_test)
377 : {
378 1 : std::cerr << "set_rewrite_test" << std::endl;
379 : // data_specification specification = parse_data_specification(
380 : // "sort A = Set(Nat);"
381 : // );
382 :
383 1 : data_specification specification;
384 1 : specification.add_context_sort(sort_set::set_(sort_nat::nat()));
385 1 : specification.add_context_sort(sort_set::set_(sort_bool::bool_()));
386 :
387 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
388 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
389 : {
390 1 : std::cerr << " Strategy8: " << *strat << std::endl;
391 1 : data::rewriter R(specification, *strat);
392 :
393 1 : sort_expression set_nat(sort_set::set_(sort_nat::nat()));
394 :
395 2 : data_expression empty_fset(R(normalize_sorts(sort_fset::empty(sort_nat::nat()),specification)));
396 2 : data_expression empty_set(R(normalize_sorts(sort_set::constructor(sort_nat::nat(),sort_set::false_function(sort_nat::nat()),
397 2 : sort_fset::empty(sort_nat::nat())),specification)));
398 :
399 1 : data_expression p0(sort_nat::nat(0));
400 1 : data_expression p1(sort_nat::nat(1));
401 1 : data_expression p2(sort_nat::nat(2));
402 :
403 1 : data_rewrite_test(R, normalize_sorts(equal_to(sort_set::true_function(sort_nat::nat()), sort_set::true_function(sort_nat::nat())),specification), sort_bool::true_());
404 1 : data_rewrite_test(R, normalize_sorts(equal_to(sort_set::false_function(sort_nat::nat()), sort_set::false_function(sort_nat::nat())),specification), sort_bool::true_());
405 1 : data_rewrite_test(R, normalize_sorts(equal_to(sort_set::true_function(sort_nat::nat()), sort_set::false_function(sort_nat::nat())),specification), sort_bool::false_());
406 1 : data_rewrite_test(R, normalize_sorts(equal_to(sort_set::false_function(sort_nat::nat()), sort_set::true_function(sort_nat::nat())),specification), sort_bool::false_());
407 :
408 2 : data_expression s1(R(normalize_sorts(sort_set::set_fset(sort_nat::nat(), sort_fset::insert(sort_nat::nat(), p1, sort_fset::empty(sort_nat::nat()))),specification)));
409 2 : data_expression s2(R(normalize_sorts(sort_set::set_fset(sort_nat::nat(), sort_fset::insert(sort_nat::nat(), p2, sort_fset::empty(sort_nat::nat()))),specification)));
410 2 : data_expression s(R(normalize_sorts(sort_set::set_fset(sort_nat::nat(), sort_fset::insert(sort_nat::nat(), p1, sort_fset::insert(sort_nat::nat(), p2, sort_fset::empty(sort_nat::nat())))),specification)));
411 :
412 2 : data_expression empty_complement(normalize_sorts(sort_set::complement(sort_nat::nat(),
413 3 : sort_set::constructor(sort_nat::nat(),sort_set::false_function(sort_nat::nat()),sort_fset::empty(sort_nat::nat()))),specification));
414 2 : data_expression intersection(normalize_sorts(sort_set::intersection(sort_nat::nat(),sort_set::complement(sort_nat::nat(),
415 2 : sort_set::constructor(sort_nat::nat(),sort_set::false_function(sort_nat::nat()), sort_fset::empty(sort_nat::nat()))),
416 3 : sort_set::constructor(sort_nat::nat(),sort_set::false_function(sort_nat::nat()),sort_fset::empty(sort_nat::nat()))),specification));
417 : //data_rewrite_test(R, normalize_sorts(less_equal(empty_complement,empty),specification), false_());
418 1 : data_rewrite_test(R, normalize_sorts(less_equal(empty_set,empty_complement),specification), sort_bool::true_());
419 : //data_rewrite_test(R, normalize_sorts(equal_to(intersection, empty_complement),specification), true_());
420 : //data_rewrite_test(R, normalize_sorts(equal_to(empty_complement, intersection),specification), true_());
421 :
422 1 : data_rewrite_test(R, normalize_sorts(sort_set::in(sort_nat::nat(), p0, s),specification), sort_bool::false_());
423 1 : data_rewrite_test(R, normalize_sorts(sort_set::in(sort_nat::nat(), p1, s),specification), sort_bool::true_());
424 1 : data_rewrite_test(R, normalize_sorts(sort_set::in(sort_nat::nat(), p2, s),specification), sort_bool::true_());
425 :
426 1 : data_rewrite_test(R, normalize_sorts(sort_set::union_(sort_nat::nat(), s, empty_set),specification), s);
427 1 : data_rewrite_test(R, normalize_sorts(sort_set::union_(sort_nat::nat(), s1, s2),specification), s);
428 :
429 1 : data_rewrite_test(R, normalize_sorts(sort_set::intersection(sort_nat::nat(), s, empty_set),specification), empty_set);
430 1 : data_rewrite_test(R, normalize_sorts(sort_set::intersection(sort_nat::nat(), s, s1),specification), s1);
431 1 : data_rewrite_test(R, normalize_sorts(sort_set::intersection(sort_nat::nat(), s, s2),specification), s2);
432 :
433 1 : data_rewrite_test(R, normalize_sorts(sort_set::difference(sort_nat::nat(), s, empty_set),specification), s);
434 1 : data_rewrite_test(R, normalize_sorts(sort_set::difference(sort_nat::nat(), s, s1),specification), s2);
435 1 : data_rewrite_test(R, normalize_sorts(sort_set::difference(sort_nat::nat(), s, s2),specification), s1);
436 :
437 1 : data_rewrite_test(R, normalize_sorts(sort_set::in(sort_nat::nat(), p0, sort_set::complement(sort_nat::nat(), s)),specification), sort_bool::true_());
438 : // extra tests by Jan Friso
439 2 : data::data_expression x = data::parse_data_expression("1 in {n:Nat|n<5}",specification);
440 1 : data_rewrite_test(R, x, sort_bool::true_());
441 1 : x = data::parse_data_expression("7 in {n:Nat|n<5}",specification);
442 1 : data_rewrite_test(R, x, sort_bool::false_());
443 1 : x = data::parse_data_expression("true in {n:Bool|n || !n}",specification);
444 1 : data_rewrite_test(R, x, sort_bool::true_());
445 1 : x = data::parse_data_expression("false in {n:Bool|n && !n}",specification);
446 1 : data_rewrite_test(R, x, sort_bool::false_());
447 :
448 : // test for a variation on bug #721,
449 : // see also set_bool_rewrite_test()
450 1 : x = sort_bool::not_(sort_fset::in(sort_nat::nat(), sort_nat::c0(), sort_fset::insert(sort_nat::nat(), sort_nat::cnat(sort_pos::c1()), sort_fset::cons_(sort_nat::nat(), sort_nat::c0(), sort_fset::empty(sort_nat::nat())))));
451 1 : x = normalize_sorts(x,specification);
452 1 : data_rewrite_test(R, x, sort_bool::false_());
453 1 : }
454 1 : }
455 :
456 2 : BOOST_AUTO_TEST_CASE(bag_rewrite_test)
457 : {
458 : using namespace mcrl2::data::sort_nat;
459 : using namespace mcrl2::data::sort_pos;
460 : using namespace mcrl2::data::sort_bool;
461 :
462 : data_specification specification = parse_data_specification(
463 : "sort A = Bag(Nat);"
464 2 : );
465 :
466 1 : specification.add_context_sort(sort_bag::bag(nat()));
467 1 : specification.add_context_sort(sort_bag::bag(pos()));
468 :
469 1 : std::cerr << "bag rewrite test\n";
470 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
471 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
472 : {
473 1 : std::cerr << " Strategy9: " << *strat << std::endl;
474 1 : data::rewriter R(specification, *strat);
475 :
476 1 : sort_expression bag_nat(sort_bag::bag(nat()));
477 :
478 2 : data_expression empty_fbag(R(normalize_sorts(sort_fbag::empty(nat()),specification)));
479 2 : data_expression empty_bag(R(normalize_sorts(
480 3 : sort_bag::constructor(nat(),sort_bag::zero_function(nat()),sort_fbag::empty(nat())),specification)));
481 :
482 1 : data_expression p0(nat(0));
483 1 : data_expression p1(nat(1));
484 1 : data_expression p2(nat(2));
485 :
486 2 : data_expression s1(R(normalize_sorts(sort_bag::bag_fbag(nat(), sort_fbag::insert(nat(), p1, pos(1), sort_fbag::empty(nat()))),specification)));
487 2 : data_expression s2(R(normalize_sorts(sort_bag::bag_fbag(nat(), sort_fbag::insert(nat(), p2, pos(2), sort_fbag::empty(nat()))),specification)));
488 2 : data_expression s(R(normalize_sorts(sort_bag::bag_fbag(nat(), sort_fbag::insert(nat(), p1, pos(1), sort_fbag::insert(nat(), p2, pos(2), sort_fbag::empty(nat())))),specification)));
489 :
490 1 : data_rewrite_test(R, normalize_sorts(sort_bag::in(nat(), p0, s),specification), false_());
491 1 : data_rewrite_test(R, normalize_sorts(sort_bag::in(nat(), p1, s),specification), true_());
492 1 : data_rewrite_test(R, normalize_sorts(sort_bag::in(nat(), p2, s),specification), true_());
493 :
494 1 : data_rewrite_test(R, normalize_sorts(sort_bag::count(nat(), p0, s),specification), p0);
495 1 : data_rewrite_test(R, normalize_sorts(sort_bag::count(nat(), p1, s),specification), p1);
496 1 : data_rewrite_test(R, normalize_sorts(sort_bag::count(nat(), p2, s),specification), p2);
497 :
498 1 : data_rewrite_test(R, normalize_sorts(sort_bag::union_(nat(), s, empty_bag),specification), s);
499 1 : data_rewrite_test(R, normalize_sorts(sort_bag::union_(nat(), s1, s2),specification), s);
500 :
501 1 : data_rewrite_test(R, normalize_sorts(sort_bag::intersection(nat(), s, empty_bag),specification), empty_bag);
502 1 : data_rewrite_test(R, normalize_sorts(sort_bag::intersection(nat(), s, s1),specification), s1);
503 1 : data_rewrite_test(R, normalize_sorts(sort_bag::intersection(nat(), s, s2),specification), s2);
504 :
505 1 : data_rewrite_test(R, normalize_sorts(sort_bag::difference(nat(), s, empty_bag),specification), s);
506 1 : data_rewrite_test(R, normalize_sorts(sort_bag::difference(nat(), s, s1),specification), s2);
507 1 : data_rewrite_test(R, normalize_sorts(sort_bag::difference(nat(), s, s2),specification), s1);
508 :
509 : // extra tests by Jan Friso
510 2 : data::data_expression x = data::parse_data_expression("count(1,{ 1:1,2:2})==1",specification);
511 1 : data_rewrite_test(R, x, true_());
512 1 : x = data::parse_data_expression("count(2,{ 1:1,2:2})==2",specification);
513 1 : data_rewrite_test(R, x, true_());
514 1 : x = data::parse_data_expression("count(2,{ 1:1,2:2})==1",specification);
515 1 : data_rewrite_test(R, x, false_());
516 1 : }
517 1 : }
518 :
519 2 : BOOST_AUTO_TEST_CASE(structured_sort_rewrite_test)
520 : {
521 : using namespace sort_bool;
522 : using namespace sort_nat;
523 :
524 :
525 : //data_specification specification;
526 :
527 1 : std::vector< structured_sort_constructor_argument > arguments;
528 :
529 1 : arguments.push_back(structured_sort_constructor_argument("a0", bool_()));
530 1 : arguments.push_back(structured_sort_constructor_argument(static_cast<sort_expression const&>(bool_())));
531 1 : arguments.push_back(structured_sort_constructor_argument("n0", sort_nat::nat()));
532 1 : arguments.push_back(structured_sort_constructor_argument("n1", sort_nat::nat()));
533 :
534 1 : std::vector< structured_sort_constructor > constructors;
535 : // without arguments or recogniser
536 : // c0
537 1 : constructors.push_back(structured_sort_constructor("c0"));
538 : // without arguments, with recogniser
539 : // c1?is_one
540 1 : constructors.push_back(structured_sort_constructor("c1", std::string("is_one")));
541 : // with arguments, without recogniser
542 : // a(a0 : A)
543 1 : constructors.push_back(structured_sort_constructor("a",
544 2 : structured_sort_constructor_argument_list(arguments.begin(), arguments.begin() + 1)));
545 : // two arguments, with recogniser
546 : // b(B)?is_b
547 1 : constructors.push_back(structured_sort_constructor("b",
548 2 : structured_sort_constructor_argument_list(arguments.begin() + 1, arguments.begin() + 2), "is_b"));
549 : // c(n0 : Nat, n1 : Nat)?is_c
550 1 : constructors.push_back(structured_sort_constructor("c",
551 2 : structured_sort_constructor_argument_list(arguments.begin() + 2, arguments.end()), "is_c"));
552 :
553 1 : data::structured_sort ls(constructors);
554 :
555 : // specification.add_alias(alias(basic_sort("D"), ls));
556 : // specification.normalize_sorts();
557 :
558 2 : data_specification specification = data::parse_data_specification("sort D = struct c0 | c1?is_one | a(a0: Bool) | b(Bool)?is_b | c(n0: Nat, n1: Nat)?is_c; ");
559 :
560 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
561 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
562 : {
563 1 : std::cerr << " Strategy10: " << *strat << std::endl;
564 1 : data::rewriter R(specification, *strat);
565 :
566 1 : data_expression c0(constructors[0].constructor_function(ls));
567 1 : data_expression c1(constructors[1].constructor_function(ls));
568 2 : data_expression a(constructors[2].constructor_function(ls)(true_()));
569 2 : data_expression b(constructors[3].constructor_function(ls)(false_()));
570 2 : data_expression n0(nat("0"));
571 2 : data_expression n1(nat("1"));
572 2 : data_expression c(constructors[4].constructor_function(ls)(n0, n1));
573 2 : data_expression c_(constructors[4].constructor_function(ls)(n1, n0));
574 :
575 : // equality, less, less_equal test
576 1 : data_rewrite_test(R, normalize_sorts(equal_to(c0, c0),specification), true_());
577 1 : data_rewrite_test(R, normalize_sorts(equal_to(c0, c1),specification), false_());
578 1 : data_rewrite_test(R, normalize_sorts(equal_to(c0, c),specification), false_());
579 1 : data_rewrite_test(R, normalize_sorts(equal_to(c, c),specification), true_());
580 1 : data_rewrite_test(R, normalize_sorts(equal_to(c, c_),specification), false_());
581 1 : data_rewrite_test(R, normalize_sorts(less(c0, c0),specification), false_());
582 1 : data_rewrite_test(R, normalize_sorts(less(c0, c1),specification), true_());
583 1 : data_rewrite_test(R, normalize_sorts(less(c1, c0),specification), false_());
584 1 : data_rewrite_test(R, normalize_sorts(less(c0, c),specification), true_());
585 1 : data_rewrite_test(R, normalize_sorts(less(c, c),specification), false_());
586 1 : data_rewrite_test(R, normalize_sorts(less(c, c_),specification), true_());
587 1 : data_rewrite_test(R, normalize_sorts(less(c_, c),specification), false_());
588 1 : data_rewrite_test(R, normalize_sorts(less_equal(c0, c0),specification), true_());
589 1 : data_rewrite_test(R, normalize_sorts(less_equal(c0, c1),specification), true_());
590 1 : data_rewrite_test(R, normalize_sorts(less_equal(c1, c0),specification), false_());
591 1 : data_rewrite_test(R, normalize_sorts(less_equal(c0, c),specification), true_());
592 1 : data_rewrite_test(R, normalize_sorts(less_equal(c, c),specification), true_());
593 1 : data_rewrite_test(R, normalize_sorts(less_equal(c, c_),specification), true_());
594 1 : data_rewrite_test(R, normalize_sorts(less_equal(c_, c),specification), false_());
595 :
596 : // recogniser tests
597 1 : data_rewrite_test(R, normalize_sorts(application(constructors[1].recogniser_function(ls), c0),specification), false_());
598 1 : data_rewrite_test(R, normalize_sorts(application(constructors[3].recogniser_function(ls), c0),specification), false_());
599 1 : data_rewrite_test(R, normalize_sorts(application(constructors[4].recogniser_function(ls), c0),specification), false_());
600 1 : data_rewrite_test(R, normalize_sorts(application(constructors[1].recogniser_function(ls), c1),specification), true_());
601 1 : data_rewrite_test(R, normalize_sorts(application(constructors[3].recogniser_function(ls), c1),specification), false_());
602 1 : data_rewrite_test(R, normalize_sorts(application(constructors[4].recogniser_function(ls), c1),specification), false_());
603 1 : data_rewrite_test(R, normalize_sorts(application(constructors[1].recogniser_function(ls), a),specification), false_());
604 1 : data_rewrite_test(R, normalize_sorts(application(constructors[3].recogniser_function(ls), a),specification), false_());
605 1 : data_rewrite_test(R, normalize_sorts(application(constructors[4].recogniser_function(ls), a),specification), false_());
606 1 : data_rewrite_test(R, normalize_sorts(application(constructors[1].recogniser_function(ls), b),specification), false_());
607 1 : data_rewrite_test(R, normalize_sorts(application(constructors[3].recogniser_function(ls), b),specification), true_());
608 1 : data_rewrite_test(R, normalize_sorts(application(constructors[4].recogniser_function(ls), b),specification), false_());
609 1 : data_rewrite_test(R, normalize_sorts(application(constructors[1].recogniser_function(ls), c),specification), false_());
610 1 : data_rewrite_test(R, normalize_sorts(application(constructors[3].recogniser_function(ls), c),specification), false_());
611 1 : data_rewrite_test(R, normalize_sorts(application(constructors[4].recogniser_function(ls), c),specification), true_());
612 :
613 : // projection tests
614 1 : data_rewrite_test(R, normalize_sorts(application(constructors[2].projection_functions(ls)[0], a),specification), true_());
615 1 : data_rewrite_test(R, normalize_sorts(application(constructors[4].projection_functions(ls)[0], c),specification), R(n0));
616 1 : data_rewrite_test(R, normalize_sorts(application(constructors[4].projection_functions(ls)[1], c),specification), R(n1));
617 1 : }
618 1 : }
619 :
620 : // Test for bug #721
621 2 : BOOST_AUTO_TEST_CASE(set_bool_rewrite_test)
622 : {
623 : using namespace sort_bool;
624 : using namespace sort_nat;
625 :
626 1 : data_specification specification;
627 :
628 : // Rewrite without sort alias
629 1 : specification.add_context_sort(sort_set::set_(bool_()));
630 1 : specification.add_context_sort(sort_fset::fset(bool_()));
631 :
632 1 : std::cerr << "set bool rewrite test\n";
633 2 : data_expression e(not_(sort_fset::in(bool_(), true_(), sort_fset::insert(bool_(), false_(), sort_fset::cons_(bool_(), true_(), sort_fset::empty(bool_()))))));
634 1 : e = normalize_sorts(e,specification);
635 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
636 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
637 : {
638 1 : std::cerr << " Strategy11: " << *strat << std::endl;
639 1 : data::rewriter R(specification, *strat);
640 1 : data_rewrite_test(R, e, false_());
641 1 : }
642 :
643 : // Rewrite with sort alias
644 1 : specification = parse_data_specification("sort S = Set(Bool);\n");
645 1 : specification.add_context_sort(sort_set::set_(bool_()));
646 1 : specification.add_context_sort(sort_fset::fset(bool_()));
647 :
648 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
649 : {
650 1 : std::cerr << " Strategy12: " << *strat << std::endl;
651 1 : data::rewriter R(specification, *strat);
652 :
653 1 : e = not_(sort_fset::in(bool_(), true_(), sort_fset::insert(bool_(), false_(), sort_fset::cons_(bool_(), true_(), sort_fset::empty(bool_())))));
654 1 : e = normalize_sorts(e,specification);
655 1 : data_rewrite_test(R, e, false_());
656 :
657 : // Rewrite with parsing
658 1 : e = parse_data_expression("true in {true, false}", specification);
659 1 : data_rewrite_test(R, e, true_());
660 1 : }
661 :
662 :
663 1 : specification = data_specification();
664 1 : specification.add_context_sort(sort_set::set_(nat()));
665 :
666 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
667 : {
668 1 : std::cerr << " Strategy13: " << *strat << std::endl;
669 1 : data::rewriter R(specification, *strat);
670 :
671 : // test for a variation on bug #721
672 1 : e = not_(sort_fset::in(nat(), c0(), sort_fset::insert(nat(), cnat(sort_pos::c1()), sort_fset::cons_(nat(), c0(), sort_fset::empty(nat())))));
673 1 : e = normalize_sorts(e,specification);
674 1 : data_rewrite_test(R, e, false_());
675 1 : }
676 1 : }
677 :
678 2 : BOOST_AUTO_TEST_CASE(finite_set_nat_rewrite_test)
679 : {
680 : using namespace mcrl2::data::sort_set;
681 : using namespace mcrl2::data::sort_fset;
682 : using namespace mcrl2::data::sort_nat;
683 : using namespace mcrl2::data::sort_bool;
684 1 : std::cerr << "finite_set_nat_rewrite_test\n";
685 : data_specification specification = parse_data_specification(
686 : "sort A = Set(Nat);"
687 2 : );
688 :
689 1 : specification.add_context_sort(set_(nat()));
690 1 : specification.add_context_sort(set_(bool_()));
691 :
692 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
693 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
694 : {
695 1 : std::cerr << " Strategy14: " << *strat << std::endl;
696 1 : data::rewriter R(specification, *strat);
697 :
698 2 : data::data_expression x = not_(sort_fset::in(nat(), c0(), sort_fset::insert(nat(), cnat(sort_pos::c1()), sort_fset::cons_(nat(), c0(), sort_fset::empty(nat())))));
699 1 : x = normalize_sorts(x,specification);
700 1 : data_rewrite_test(R, x, false_());
701 1 : }
702 1 : }
703 :
704 2 : BOOST_AUTO_TEST_CASE(finite_set_equals_test)
705 : {
706 : using namespace mcrl2::data::sort_set;
707 : using namespace mcrl2::data::sort_fset;
708 : using namespace mcrl2::data::sort_nat;
709 : using namespace mcrl2::data::sort_bool;
710 1 : std::cerr << "finite_set_equals_test\n";
711 : data_specification specification = parse_data_specification(
712 : "sort R = struct r2 | r1 ;\n"
713 : "map All: Set(R);\n"
714 2 : "eqn All = { r: R | true };\n");
715 :
716 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
717 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
718 : {
719 1 : std::cerr << " Strategy14a: " << *strat << std::endl;
720 1 : data::rewriter R(specification, *strat);
721 :
722 2 : data::data_expression x = data::parse_data_expression("{r1, r2} == All", specification);
723 1 : x = normalize_sorts(x,specification);
724 1 : data_rewrite_test(R, x, true_());
725 1 : x = data::parse_data_expression("r1 == r1", specification);
726 1 : x = normalize_sorts(x,specification);
727 1 : data_rewrite_test(R, x, true_());
728 1 : x = data::parse_data_expression("r1 == r2", specification);
729 1 : x = normalize_sorts(x,specification);
730 1 : data_rewrite_test(R, x, false_());
731 1 : }
732 1 : }
733 :
734 2 : BOOST_AUTO_TEST_CASE(finite_set_nat_rewrite_test_without_alias)
735 : {
736 : using namespace mcrl2::data::sort_nat;
737 : using namespace mcrl2::data::sort_bool;
738 1 : std::cerr << "finite_set_nat_rewrite_test_without_alias\n";
739 1 : data_specification specification;
740 :
741 1 : specification.add_context_sort(sort_set::set_(nat()));
742 :
743 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
744 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
745 : {
746 1 : std::cerr << " Strategy15: " << *strat << std::endl;
747 1 : data::rewriter R(specification, *strat);
748 :
749 1 : data::data_expression x;
750 :
751 1 : x = less(cnat(sort_pos::c1()), c0());
752 1 : x = normalize_sorts(x,specification);
753 1 : data_rewrite_test(R, x, false_());
754 :
755 1 : x = less(c0(), cnat(sort_pos::c1()));
756 1 : x = normalize_sorts(x,specification);
757 1 : data_rewrite_test(R, x, true_());
758 :
759 1 : x = sort_fset::in(nat(), c0(), sort_fset::cons_(nat(), c0(), sort_fset::empty(nat())));
760 1 : x = normalize_sorts(x,specification);
761 1 : data_rewrite_test(R, x, true_());
762 :
763 1 : x = sort_fset::insert(nat(), cnat(sort_pos::c1()), sort_fset::cons_(nat(), c0(), sort_fset::empty(nat())));
764 1 : x = normalize_sorts(x,specification);
765 1 : data_rewrite_test(R, x, sort_fset::cons_(nat(), c0(), sort_fset::cons_(nat(), cnat(sort_pos::c1()), sort_fset::empty(nat()))));
766 :
767 1 : x = sort_fset::in(nat(), c0(), sort_fset::insert(nat(), cnat(sort_pos::c1()), sort_fset::cons_(nat(), c0(), sort_fset::empty(nat()))));
768 1 : x = normalize_sorts(x,specification);
769 1 : data_rewrite_test(R, x, true_());
770 :
771 1 : x = not_(sort_fset::in(nat(), c0(), sort_fset::insert(nat(), cnat(sort_pos::c1()), sort_fset::cons_(nat(), c0(), sort_fset::empty(nat())))));
772 1 : x = normalize_sorts(x,specification);
773 1 : data_rewrite_test(R, x, false_());
774 1 : }
775 1 : }
776 :
777 2 : BOOST_AUTO_TEST_CASE(regression_test_bug_723)
778 : {
779 : std::string s(
780 : "sort BL = List(Bool);\n"
781 : "map initial: Nat -> BL;\n"
782 : " all_false: BL -> Bool;\n"
783 : "var b0: Bool;\n"
784 : " bl: BL;\n"
785 : " n: Nat;\n"
786 : "eqn initial (1) = [];\n"
787 : " n > 1 -> initial (n) = false |> initial(Int2Nat(n-1));\n"
788 : " all_false ([]) = true;\n"
789 : " all_false (b0 |> bl) = !b0 && all_false(bl);\n"
790 1 : );
791 :
792 1 : std::cerr << "List of booleans test, using initial" << std::endl;
793 1 : data_specification specification(parse_data_specification(s));
794 :
795 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
796 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
797 : {
798 1 : std::cerr << " Strategy16: " << *strat << std::endl;
799 1 : data::rewriter R(specification, *strat);
800 :
801 2 : const data::data_expression e(parse_data_expression("all_false(initial(1))", specification));
802 1 : data_rewrite_test(R, e, sort_bool::true_());
803 :
804 2 : const data::data_expression e1(parse_data_expression("all_false(initial(2))", specification));
805 1 : data_rewrite_test(R, e1, sort_bool::true_());
806 :
807 2 : const data::data_expression e2(parse_data_expression("all_false(initial(4))", specification));
808 1 : data_rewrite_test(R, e2, sort_bool::true_());
809 1 : }
810 1 : }
811 :
812 2 : BOOST_AUTO_TEST_CASE(test_othello_condition)
813 : {
814 : std::string s(
815 : "sort Piece = struct Red | White | None;\n"
816 : " Row = List(Piece);\n"
817 : " Board = List(Row);\n"
818 : "map At:Nat#Nat#Board->Piece;\n"
819 : " At:Nat#Row->Piece;\n"
820 : " Put:Piece#Pos#Pos#Board->Board;\n"
821 : " Put:Piece#Pos#Row->Row;\n"
822 : " N,M: Pos;\n"
823 : "var b,b':Board;\n"
824 : " r:Row;\n"
825 : " p,p':Piece;\n"
826 : " x,y:Nat;\n"
827 : " c:Bool;\n"
828 : " z:Pos;\n"
829 : "eqn N = 4;\n"
830 : " M = 4;\n"
831 : " y==1 -> At(x,y,r|>b)=At(x,r);\n"
832 : " 1<y && y<=M -> At(x,y,r|>b)=At(x,Int2Nat(y-1),b);\n"
833 : " y==0 || y>M || x==0 || x>N -> At(x,y,b)=None;\n"
834 : " At(x,y,if(c,b,b'))=if(c,At(x,y,b),At(x,y,b'));\n"
835 : " x==1 -> At(x,p|>r)=p;\n"
836 : " 1<x && x<=N -> At(x,p|>r)=At(Int2Nat(x-1),r);\n"
837 : " x==0 || x>N -> At(x,p|>r)=None;\n"
838 : " At(x,Put(p,z,r))=if(x==z,p,At(x,r));\n"
839 : "var b,b':Board;\n"
840 : " r:Row;\n"
841 : " p,p':Piece;\n"
842 : " x,y:Pos;\n"
843 : " c:Bool;\n"
844 : "eqn y==1 -> Put(p,x,y,r|>b)=Put(p,x,r)|>b;\n"
845 : " y>1 && y<=M -> Put(p,x,y,r|>b)=r|>Put(p,x,Int2Pos(y-1),b);\n"
846 : " Put(p,x,y,if(c,b,b'))=if(c,Put(p,x,y,b),Put(p,x,y,b'));\n"
847 : " x==1 -> Put(p,x,p'|>r)=p|>r;\n"
848 : " x>1 && x<=N -> Put(p,x,p'|>r)=p'|>Put(p,Int2Pos(x-1),r);\n"
849 1 : );
850 :
851 1 : data_specification specification(parse_data_specification(s));
852 :
853 1 : std::cerr << "othello test\n";
854 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
855 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
856 : {
857 1 : std::cerr << " Strategy17: " << *strat << std::endl;
858 1 : data::rewriter R(specification, *strat);
859 :
860 2 : data::data_expression e(parse_data_expression("At(1, 2, [[None, None, None, None], [None, Red, White, None], [None, White, Red, None], [None, None, None, None]]) == None", specification));
861 1 : data_rewrite_test(R, e, sort_bool::true_());
862 1 : }
863 1 : }
864 :
865 2 : BOOST_AUTO_TEST_CASE(test_lambda_expression)
866 : {
867 : std::string s(
868 : "map n: Pos;\n"
869 : "eqn n=2;\n"
870 : "sort D = struct d1 | d2;\n"
871 : " Buf = Nat -> struct data(getdata:D) | empty;\n"
872 : "map emptyBuf: Buf;\n"
873 : " insert: D#Nat#Buf -> Buf;\n"
874 : " remove: Nat#Buf -> Buf;\n"
875 : " release: Nat#Nat#Buf -> Buf;\n"
876 : " nextempty: Nat#Buf -> Nat;\n"
877 : " nextempty_rec: Nat#Buf#Nat -> Nat;\n"
878 : " inWindow: Nat#Nat#Nat -> Bool;\n"
879 : " nat_const:Nat;\n"
880 : "var i,j,k: Nat; d: D; q: Buf;\n"
881 : "eqn emptyBuf = lambda j:Nat.empty;\n"
882 : " insert(d,i,q) = lambda j:Nat.if(i==j,data(d),q(j));\n"
883 : " remove(i,q) = lambda j:Nat.if(i==j,empty,q(j));\n"
884 : " i mod 2*n==j mod 2*n -> release(i,j,q) = q;\n"
885 : " i mod 2*n!=j mod 2*n ->\n"
886 : " release(i,j,q) = release((i+1) mod 2*n,j,remove(i,q));\n"
887 : " k<n -> nextempty_rec(i,q,k) =\n"
888 : " if(q(i)==empty,i,nextempty_rec((i+1) mod n,q,k+1));\n"
889 : " k==n -> nextempty_rec(i,q,k)=i;\n"
890 : " nextempty(i,q) = nextempty_rec(i,q,0);\n"
891 : " inWindow(i,j,k) = (i<=j && j<k) || (k<i && i<=j) || (j<k && k<i);\n"
892 1 : );
893 :
894 1 : data_specification specification(parse_data_specification(s));
895 :
896 1 : std::cerr << "lambda rewrite test\n";
897 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
898 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
899 : {
900 1 : std::cerr << " Strategy18: " << *strat << std::endl;
901 1 : data::rewriter R(specification, *strat);
902 :
903 2 : data::data_expression e(parse_data_expression("(insert(d2,2,insert(d1,1,emptyBuf)))(nat_const)", specification));
904 1 : data_rewrite_test(R, e, R(e));
905 1 : e=parse_data_expression("insert(d1,1,emptyBuf)(1)==data(d1)", specification);
906 1 : data_rewrite_test(R, e, sort_bool::true_());
907 1 : e=parse_data_expression("insert(d1,1,emptyBuf)(1)==empty", specification);
908 1 : data_rewrite_test(R, e, sort_bool::false_());
909 1 : e=parse_data_expression("remove(1,emptyBuf)(1)==data(d1)", specification);
910 1 : data_rewrite_test(R, e, sort_bool::false_());
911 1 : e=parse_data_expression("remove(1,emptyBuf)(1)==empty", specification);
912 1 : data_rewrite_test(R, e, sort_bool::true_());
913 1 : e=parse_data_expression("remove(1,insert(d1,1,emptyBuf))(1)==insert(d1,1,emptyBuf)(1)", specification);
914 1 : data_rewrite_test(R, e, sort_bool::false_());
915 1 : }
916 1 : }
917 :
918 2 : BOOST_AUTO_TEST_CASE(test_whether_lists_can_be_put_in_sets)
919 : {
920 : std::string s(
921 : "sort T = struct s( List(T) ) | c;\n"
922 : "map func: Bool;\n"
923 : "eqn func = s( [c] ) in { s( [] ) };\n"
924 1 : );
925 :
926 1 : data_specification specification(parse_data_specification(s));
927 :
928 1 : std::cerr << "list in set teste\n";
929 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
930 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
931 : {
932 1 : std::cerr << " Strategy19: " << *strat << std::endl;
933 1 : data::rewriter R(specification, *strat);
934 :
935 2 : data::data_expression e(parse_data_expression("func", specification));
936 1 : data_rewrite_test(R, e, sort_bool::false_());
937 1 : }
938 :
939 1 : }
940 :
941 2 : BOOST_AUTO_TEST_CASE(lambda_predicate_matching)
942 : {
943 : // Taken from the specification:
944 : // ================================
945 : // map match :(Nat -> Bool)#List(Nat) -> List(Nat) ;
946 : // pre: Nat -> Bool;
947 : // emptyList: List(Nat);
948 : // eqn match (pre, []) = [];
949 : // emptyList = [];
950 : //
951 : // init ( match( lambda i:Nat. true, [] ) == emptyList ) -> tau;
952 : // ================================
953 :
954 :
955 : std::string s(
956 : "map match : (Nat -> Bool)#List(Nat) -> List(Nat);\n"
957 : " emptyList: List(Nat);\n"
958 : "var v : Nat -> Bool;\n"
959 : "eqn match(v, []) = emptyList;"
960 1 : );
961 :
962 1 : data_specification specification(parse_data_specification(s));
963 :
964 1 : std::cerr << "lambda_predicate_matching\n";
965 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
966 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
967 : {
968 1 : std::cerr << " Strategy20: " << *strat << std::endl;
969 1 : data::rewriter R(specification, *strat);
970 :
971 2 : data::data_expression e(parse_data_expression("match( lambda i:Nat. true, [] )", specification));
972 2 : data::data_expression f(parse_data_expression("emptyList", specification));
973 1 : data_rewrite_test(R, e, f);
974 1 : }
975 :
976 1 : }
977 :
978 2 : BOOST_AUTO_TEST_CASE(difficult_empty_list_in_set)
979 : {
980 : // Taken from the specification:
981 : // ================================
982 : // map F1: List(Bool)#Bool#List(Bool)#Bag(Bool) -> List(Bool);
983 : // F2: List(Bool) -> Bag(Bool);
984 : // ELM: List(Bool)#Bool#List(Bool) -> List(Bool);
985 : // var ca: Bool;
986 : // cal: List(Bool);
987 : // b: Bool;
988 : // bs: List(Bool);
989 : // m: Bag(Bool);
990 : // a: Bool;
991 : // eqn
992 : // F1( cal, b, [] , m ) = [];
993 : // F1( cal, b, a |> bs, m ) = if( m <= {}, ELM( cal, b, a |> bs ) , [] );
994 : // ELM( [] , b, bs ) = F1( [] , b, bs, { false:1 } );
995 : // ELM( ca |> cal, b, bs ) = ELM( cal, b , bs );
996 : //
997 : // act a: List(Bool);
998 : //
999 : // proc X = sum r: List(Bool). ( r in { a: List(Bool) | exists ac': List(Bool). a == F1( [false], false, ac', { false:1 })} )-> a(r) . X;
1000 : //
1001 : // init X;
1002 : // ================================
1003 :
1004 : std::string s(
1005 : "map F1: List(Bool)#Bool#List(Bool)#Bag(Bool) -> List(Bool);"
1006 : " F2: Set(List(Bool)); %declared to add the rewrite rules for Set(List(Bool)).\n"
1007 : " ELM: List(Bool)#Bool#List(Bool) -> List(Bool);"
1008 : "var ca: Bool;"
1009 : " cal: List(Bool);"
1010 : " b: Bool;"
1011 : " bs: List(Bool);"
1012 : " m: Bag(Bool);"
1013 : " a: Bool;"
1014 : "eqn "
1015 : " F1( cal, b, [] , m ) = [];"
1016 : " F1( cal, b, a |> bs, m ) = if( m <= {:}, ELM( cal, b, a |> bs ) , [] );"
1017 : " ELM( [] , b, bs ) = F1( [] , b, bs, { false:1 } );"
1018 : " ELM( ca |> cal, b, bs ) = ELM( cal, b , bs );"
1019 1 : );
1020 :
1021 1 : data_specification specification(parse_data_specification(s));
1022 :
1023 1 : std::cerr << "difficult_empty_list_in_set\n";
1024 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
1025 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
1026 : {
1027 1 : std::cerr << " Strategy21: " << *strat << std::endl;
1028 1 : data::rewriter R(specification, *strat);
1029 :
1030 2 : data::data_expression e(parse_data_expression("[] in { a: List(Bool) | exists ac': List(Bool). a == F1( [false], false, ac', { false:1 }) }", specification));
1031 2 : data::data_expression f(parse_data_expression("true", specification));
1032 1 : data_rewrite_test(R, e, f);
1033 1 : }
1034 :
1035 1 : }
1036 :
1037 2 : BOOST_AUTO_TEST_CASE(bound_existential_quantifiers_with_same_name)
1038 : {
1039 : // Taken from a pbes provided by Tim Willemse, showing a conflict of variable name x0
1040 : // that are bound by different existential quantifiers of different type.
1041 : // =====================================================================================
1042 : // sort AbsNum = struct e0 | e1 | e2 | e3 | e4 ;
1043 : //
1044 : // map
1045 : // absplus: AbsNum # AbsNum -> Set(AbsNum);
1046 : // absle: AbsNum # AbsNum -> Set(Bool);
1047 : // Lifted_and: Set(Bool) # Set(Bool) -> Set(Bool);
1048 : // Lifted_absle: Set(AbsNum) # Set(AbsNum) -> Set(Bool);
1049 : // Lifted_absplus: Set(AbsNum) # Set(AbsNum) -> Set(AbsNum);
1050 : //
1051 : // var
1052 : // n,m: AbsNum;
1053 : // eqn
1054 : // absplus(e0, n) = {n};
1055 : // absplus(e2, e2) = {e3};
1056 : // absle(n,m) = {false};
1057 : //
1058 : // var X0,X1: Set(Bool);
1059 : // eqn
1060 : // Lifted_and(X0, X1) = { y: Bool | exists x0,x1: Bool. (x0 in X0) && (x1 in X1) && (y in {x0 && x1}) } ;
1061 : //
1062 : // var X0,X1: Set(AbsNum);
1063 : // eqn Lifted_absle(X0, X1) = { y: Bool | exists x0,x1: AbsNum. (x0 in X0) && (x1 in X1) && (y in absle(x0, x1)) };
1064 : // Lifted_absplus(X0, X1) = { y: AbsNum | exists x0,x1: AbsNum. (x0 in X0) && (x1 in X1) && (y in absplus(x0, x1)) };
1065 : //
1066 : //
1067 : // pbes
1068 : // mu X(t_P: AbsNum) = val(false in (Lifted_and( Lifted_absle({e2}, Lifted_absplus({t_P}, {e2})) , {true}))) ;
1069 : //
1070 : // init X(e0);
1071 :
1072 : std::string s(
1073 : "sort AbsNum = struct e0 | e1 | e2 | e3 | e4 ;\n"
1074 :
1075 : "map\n"
1076 : " absplus: AbsNum # AbsNum -> Set(AbsNum);\n"
1077 : " absle: AbsNum # AbsNum -> Set(Bool);\n"
1078 : " Lifted_and: Set(Bool) # Set(Bool) -> Set(Bool);\n"
1079 : " Lifted_absle: Set(AbsNum) # Set(AbsNum) -> Set(Bool);\n"
1080 : " Lifted_absplus: Set(AbsNum) # Set(AbsNum) -> Set(AbsNum);\n"
1081 : "\n"
1082 : "var\n"
1083 : " n,m: AbsNum;\n"
1084 : "eqn\n"
1085 : " absplus(e0, n) = {n};\n"
1086 : " absplus(e2, e2) = {e3};\n"
1087 : " absle(n,m) = {false};\n"
1088 : "\n"
1089 : "var X0,X1: Set(Bool);\n"
1090 : "eqn\n"
1091 : " Lifted_and(X0, X1) = { y: Bool | exists x0,x1: Bool. (x0 in X0) && (x1 in X1) && (y in {x0 && x1}) } ;\n"
1092 : "\n"
1093 : "var X0,X1: Set(AbsNum);\n"
1094 : "eqn Lifted_absle(X0, X1) = { y: Bool | exists x0,x1: AbsNum. (x0 in X0) && (x1 in X1) && (y in absle(x0, x1)) };\n"
1095 : " Lifted_absplus(X0, X1) = { y: AbsNum | exists x0,x1: AbsNum. (x0 in X0) && (x1 in X1) && (y in absplus(x0, x1)) };\n"
1096 1 : );
1097 :
1098 1 : data_specification specification(parse_data_specification(s));
1099 :
1100 1 : std::cerr << "existentially bound variable x0 of different types\n";
1101 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
1102 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
1103 : {
1104 1 : std::cerr << " Strategy22: " << *strat << std::endl;
1105 1 : data::rewriter R(specification, *strat);
1106 :
1107 2 : data::data_expression e(parse_data_expression("false in (Lifted_and( Lifted_absle({e2}, Lifted_absplus({e0}, {e2})) , {true}))", specification));
1108 2 : data::data_expression f(parse_data_expression("true", specification));
1109 1 : data_rewrite_test(R, e, f);
1110 1 : }
1111 1 : }
1112 :
1113 2 : BOOST_AUTO_TEST_CASE(constructors_that_are_not_a_normal_form)
1114 : {
1115 : // The example below was made by Rolf van Leusden. It shows that if
1116 : // constructors are not normalforms, then the generated normalform must
1117 : // be rewritten. This was not the case with revision 10008 (December 2012)
1118 : std::string s(
1119 : "sort FloorID = struct F1 | F2;\n"
1120 : " \n"
1121 : "map fSucc : FloorID -> FloorID;\n"
1122 : " equal : FloorID # FloorID -> Bool;\n"
1123 : "\n"
1124 : "var f,g : FloorID;\n"
1125 : "eqn F2 = fSucc(F1); \n"
1126 : " equal(fSucc(f),fSucc(g)) = equal(f,g);\n"
1127 : " equal(fSucc(f),F1) = false;\n"
1128 : " equal(F1,fSucc(g)) = false;\n"
1129 : " equal(F1,F1) = true;\n"
1130 : " f==g = equal(f,g);\n"
1131 1 : );
1132 :
1133 1 : data_specification specification(parse_data_specification(s));
1134 :
1135 1 : std::cerr << "constructors_that_are_not_a_normal_form\n";
1136 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
1137 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
1138 : {
1139 1 : std::cerr << " Strategy23: " << *strat << std::endl;
1140 1 : data::rewriter R(specification, *strat);
1141 :
1142 2 : data::data_expression e(parse_data_expression("exists f:FloorID.equal(f,F2)", specification));
1143 2 : data::data_expression f(parse_data_expression("true", specification));
1144 1 : data_rewrite_test(R, e, f);
1145 1 : }
1146 1 : }
1147 :
1148 2 : BOOST_AUTO_TEST_CASE(rewrite_using_the_where_construct)
1149 : {
1150 : std::string s(
1151 : "map f: Nat;\n"
1152 : "eqn f = n whr n = 3 end;\n"
1153 1 : );
1154 :
1155 1 : data_specification specification(parse_data_specification(s));
1156 :
1157 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
1158 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
1159 : {
1160 1 : data::rewriter R(specification, *strat);
1161 :
1162 2 : data::data_expression e(parse_data_expression("Nat2Pos(f)", specification));
1163 2 : data::data_expression f(parse_data_expression("3", specification));
1164 1 : data_rewrite_test(R, e, f);
1165 1 : }
1166 1 : }
1167 :
1168 2 : BOOST_AUTO_TEST_CASE(rewrite_rule_for_higher_order_functions)
1169 : {
1170 : std::string s(
1171 : "map f:Nat->Nat->Bool;\n"
1172 : " c:Nat->Bool;\n"
1173 : "var x:Nat;\n"
1174 : "eqn c(x) = f(x)(0);\n"
1175 1 : );
1176 :
1177 1 : data_specification specification(parse_data_specification(s));
1178 :
1179 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
1180 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
1181 : {
1182 1 : std::cerr << " Strategy24: " << *strat << std::endl;
1183 1 : data::rewriter R(specification, *strat);
1184 :
1185 2 : data::data_expression e(parse_data_expression("c(0)", specification));
1186 2 : data::data_expression f(parse_data_expression("f(0)(0)", specification));
1187 1 : data_rewrite_test(R, e, f);
1188 1 : }
1189 1 : }
1190 :
1191 2 : BOOST_AUTO_TEST_CASE(check_whether_counting_of_elements_in_an_FBag_works_properly)
1192 : {
1193 : std::string s(
1194 : "map f:FBag(Bool);\n"
1195 : " g:FBag(Nat);\n"
1196 1 : );
1197 :
1198 1 : data_specification specification(parse_data_specification(s));
1199 :
1200 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
1201 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
1202 : {
1203 1 : std::cerr << " Strategy25: " << *strat << std::endl;
1204 1 : data::rewriter R(specification, *strat);
1205 :
1206 2 : data::data_expression e(parse_data_expression("{true:7,false:8}-{true:4,false:4}", specification));
1207 2 : data::data_expression f(parse_data_expression("{false:4,true:3}", specification));
1208 1 : data_rewrite_test(R, e, R(f));
1209 :
1210 1 : e=parse_data_expression("{false:14,true:8}-{true:29,false:4}", specification);
1211 1 : f=parse_data_expression("{false:10}", specification);
1212 1 : data_rewrite_test(R, e, R(f));
1213 :
1214 1 : e=parse_data_expression("{0:14,7:8}-{0:29,7:4}", specification);
1215 1 : f=parse_data_expression("{Pos2Nat(7):4}", specification);
1216 1 : data_rewrite_test(R, e, R(f));
1217 1 : }
1218 1 : }
1219 :
1220 :
1221 2 : BOOST_AUTO_TEST_CASE(square_root_test)
1222 : {
1223 : std::string s(
1224 : "map f:Nat;\n"
1225 : "eqn f=sqrt(1);\n"
1226 1 : );
1227 :
1228 1 : data_specification specification(parse_data_specification(s));
1229 :
1230 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
1231 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
1232 : {
1233 1 : std::cerr << " Strategy26: " << *strat << std::endl;
1234 1 : data::rewriter R(specification, *strat);
1235 :
1236 2 : data::data_expression e(parse_data_expression("Nat2Pos(sqrt(2578))", specification));
1237 2 : data::data_expression f(parse_data_expression("50", specification));
1238 1 : data_rewrite_test(R, e, R(f));
1239 :
1240 1 : e=parse_data_expression("sqrt(0)", specification);
1241 1 : f=parse_data_expression("0", specification);
1242 1 : data_rewrite_test(R, e, f);
1243 :
1244 1 : e=parse_data_expression("sqrt(1)", specification);
1245 1 : f=parse_data_expression("Pos2Nat(1)", specification);
1246 1 : data_rewrite_test(R, e, R(f));
1247 :
1248 1 : e=parse_data_expression("sqrt(2)", specification);
1249 1 : f=parse_data_expression("Pos2Nat(1)", specification);
1250 1 : data_rewrite_test(R, e, R(f));
1251 :
1252 1 : e=parse_data_expression("sqrt(3)", specification);
1253 1 : f=parse_data_expression("Pos2Nat(1)", specification);
1254 1 : data_rewrite_test(R, e, R(f));
1255 :
1256 1 : e=parse_data_expression("sqrt(4)", specification);
1257 1 : f=parse_data_expression("Pos2Nat(2)", specification);
1258 1 : data_rewrite_test(R, e, R(f));
1259 :
1260 1 : e=parse_data_expression("sqrt(5)", specification);
1261 1 : f=parse_data_expression("Pos2Nat(2)", specification);
1262 1 : data_rewrite_test(R, e, R(f));
1263 :
1264 1 : e=parse_data_expression("sqrt(6)", specification);
1265 1 : f=parse_data_expression("Pos2Nat(2)", specification);
1266 1 : data_rewrite_test(R, e, R(f));
1267 :
1268 1 : e=parse_data_expression("sqrt(7)", specification);
1269 1 : f=parse_data_expression("Pos2Nat(2)", specification);
1270 1 : data_rewrite_test(R, e, R(f));
1271 :
1272 1 : e=parse_data_expression("sqrt(8)", specification);
1273 1 : f=parse_data_expression("Pos2Nat(2)", specification);
1274 1 : data_rewrite_test(R, e, R(f));
1275 :
1276 1 : e=parse_data_expression("sqrt(9)", specification);
1277 1 : f=parse_data_expression("Pos2Nat(3)", specification);
1278 1 : data_rewrite_test(R, e, R(f));
1279 :
1280 1 : e=parse_data_expression("sqrt(10)", specification);
1281 1 : f=parse_data_expression("Pos2Nat(3)", specification);
1282 1 : data_rewrite_test(R, e, R(f));
1283 :
1284 1 : e=parse_data_expression("sqrt(11)", specification);
1285 1 : f=parse_data_expression("Pos2Nat(3)", specification);
1286 1 : data_rewrite_test(R, e, R(f));
1287 :
1288 1 : e=parse_data_expression("sqrt(12)", specification);
1289 1 : f=parse_data_expression("Pos2Nat(3)", specification);
1290 1 : data_rewrite_test(R, e, R(f));
1291 :
1292 1 : e=parse_data_expression("sqrt(13)", specification);
1293 1 : f=parse_data_expression("Pos2Nat(3)", specification);
1294 1 : data_rewrite_test(R, e, R(f));
1295 :
1296 1 : e=parse_data_expression("sqrt(14)", specification);
1297 1 : f=parse_data_expression("Pos2Nat(3)", specification);
1298 1 : data_rewrite_test(R, e, R(f));
1299 :
1300 1 : e=parse_data_expression("sqrt(15)", specification);
1301 1 : f=parse_data_expression("Pos2Nat(3)", specification);
1302 1 : data_rewrite_test(R, e, R(f));
1303 :
1304 1 : e=parse_data_expression("sqrt(16)", specification);
1305 1 : f=parse_data_expression("Pos2Nat(4)", specification);
1306 1 : data_rewrite_test(R, e, R(f));
1307 :
1308 1 : e=parse_data_expression("sqrt(17)", specification);
1309 1 : f=parse_data_expression("Pos2Nat(4)", specification);
1310 1 : data_rewrite_test(R, e, R(f));
1311 :
1312 1 : e=parse_data_expression("sqrt(18)", specification);
1313 1 : f=parse_data_expression("Pos2Nat(4)", specification);
1314 1 : data_rewrite_test(R, e, R(f));
1315 :
1316 1 : e=parse_data_expression("sqrt(19)", specification);
1317 1 : f=parse_data_expression("Pos2Nat(4)", specification);
1318 1 : data_rewrite_test(R, e, R(f));
1319 :
1320 1 : e=parse_data_expression("sqrt(20)", specification);
1321 1 : f=parse_data_expression("Pos2Nat(4)", specification);
1322 1 : data_rewrite_test(R, e, R(f));
1323 1 : }
1324 1 : }
1325 :
1326 2 : BOOST_AUTO_TEST_CASE(check_whether_higher_order_function_are_dealt_with_appropriately)
1327 : {
1328 : std::string s(
1329 : "map f:Pos->Pos->Pos->Pos->Pos->Pos;\n"
1330 : " g:Pos->Pos->Pos->Pos->Pos->Pos;\n"
1331 : " h:Pos->Pos->Pos->Pos->Pos->Pos;\n"
1332 : " k:Pos->Pos->Pos->Pos->Pos->Pos;\n"
1333 : "var x,y,z,u,v:Pos;\n"
1334 : "eqn f(x)(2)(z)(u)(v)=1;\n"
1335 : " g(3)(y)(z)(u)(v)=1;\n"
1336 : " h(x)(y)(z)(u)(v)=x;\n"
1337 : " k(x)(x)(z)(u)(v)=x;\n"
1338 1 : );
1339 :
1340 1 : data_specification specification(parse_data_specification(s));
1341 :
1342 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
1343 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
1344 : {
1345 1 : std::cerr << " Strategy27: " << *strat << std::endl;
1346 1 : data::rewriter R(specification, *strat);
1347 :
1348 2 : data::data_expression e(parse_data_expression("f(1)(2)(1)(1)(1)", specification));
1349 2 : data::data_expression f(parse_data_expression("1", specification));
1350 1 : data_rewrite_test(R, e, f);
1351 :
1352 1 : e=parse_data_expression("f(1)(1)(1)(1)(1)", specification);
1353 1 : f=parse_data_expression("f(1)(1)(1)(1)(1)", specification);
1354 1 : data_rewrite_test(R, e, f);
1355 :
1356 1 : e=parse_data_expression("g(3)(1)(1)(1)(1)", specification);
1357 1 : f=parse_data_expression("1", specification);
1358 1 : data_rewrite_test(R, e, f);
1359 :
1360 1 : e=parse_data_expression("g(1)(1)(1)(1)(1)", specification);
1361 1 : f=parse_data_expression("g(1)(1)(1)(1)(1)", specification);
1362 1 : data_rewrite_test(R, e, f);
1363 :
1364 1 : e=parse_data_expression("h(1)(1)(1)(1)(1)", specification);
1365 1 : f=parse_data_expression("1", specification);
1366 1 : data_rewrite_test(R, e, f);
1367 :
1368 1 : e=parse_data_expression("h(10)(1)(1)(1)(1)", specification);
1369 1 : f=parse_data_expression("10", specification);
1370 1 : data_rewrite_test(R, e, f);
1371 :
1372 1 : e=parse_data_expression("k(1)(1)(1)(1)(1)", specification);
1373 1 : f=parse_data_expression("1", specification);
1374 1 : data_rewrite_test(R, e, f);
1375 :
1376 1 : e=parse_data_expression("k(10)(1)(1)(1)(1)", specification);
1377 1 : f=parse_data_expression("k(10)(1)(1)(1)(1)", specification);
1378 1 : data_rewrite_test(R, e, f);
1379 :
1380 1 : }
1381 1 : }
1382 :
1383 2 : BOOST_AUTO_TEST_CASE(check_whether_higher_order_function_are_dealt_with_appropriately_in_rhs_of_rewrite_rules)
1384 : {
1385 : std::string s(
1386 : "map f:Pos->Pos->Pos->Pos->Pos->Bool;\n"
1387 : " g:Pos->Pos->Pos->Pos->Pos->Bool;\n"
1388 : "var x,y,z,u,v:Pos;\n"
1389 : "eqn f(x)(2)(z)(u)(v)=(u==2);\n"
1390 : " g(3)(y)(z)(u)(v)=f(3)(y)(z)(u)(v) || f(2)(y)(z)(u)(u);\n"
1391 1 : );
1392 :
1393 1 : data_specification specification(parse_data_specification(s));
1394 :
1395 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
1396 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
1397 : {
1398 1 : std::cerr << " Strategy28: " << *strat << std::endl;
1399 1 : data::rewriter R(specification, *strat);
1400 :
1401 2 : data::data_expression e(parse_data_expression("g(1)(2)(1)(1)(1)", specification));
1402 2 : data::data_expression f(parse_data_expression("g(1)(2)(1)(1)(1)", specification));
1403 1 : data_rewrite_test(R, e, f);
1404 :
1405 1 : e(parse_data_expression("g(3)(2)(1)(1)(1)", specification));
1406 1 : f(parse_data_expression("false", specification));
1407 1 : data_rewrite_test(R, e, f);
1408 :
1409 1 : }
1410 1 : }
1411 :
1412 2 : BOOST_AUTO_TEST_CASE(check_higher_order_functions_with_multiple_arguments)
1413 : {
1414 : std::string s(
1415 : "map f:Pos->(Pos#Pos)->Pos->Pos->Pos;\n"
1416 : " g:Pos->(Pos#Pos)->Pos->Pos->Pos;\n"
1417 : "var x,y,z,u,v:Pos;\n"
1418 : "eqn f(x)(2,z)(u)(v)= g(x)(3,z)(u)(v)+g(x)(4,z)(v)(u);\n"
1419 : " g(3)(y,z)(u)(v)=1;\n"
1420 1 : );
1421 :
1422 1 : data_specification specification(parse_data_specification(s));
1423 :
1424 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
1425 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
1426 : {
1427 1 : std::cerr << " Strategy29: " << *strat << std::endl;
1428 1 : data::rewriter R(specification, *strat);
1429 :
1430 2 : data::data_expression e(parse_data_expression("g(3)(2,1)(1)(1)", specification));
1431 2 : data::data_expression f(parse_data_expression("1", specification));
1432 1 : data_rewrite_test(R, e, f);
1433 :
1434 1 : e(parse_data_expression("g(4)(2,1)(1)(1)", specification));
1435 1 : f(parse_data_expression("g(4)(2,1)(1)(1)", specification));
1436 1 : data_rewrite_test(R, e, f);
1437 :
1438 1 : e(parse_data_expression("f(3)(2,1)(1)(1)", specification));
1439 1 : f(parse_data_expression("2", specification));
1440 1 : data_rewrite_test(R, e, f);
1441 :
1442 1 : }
1443 1 : }
1444 :
1445 2 : BOOST_AUTO_TEST_CASE(Check_function_equality)
1446 : {
1447 : std::string s(
1448 : "map f:Pos#Pos->Pos;\n"
1449 : " g:(Pos#Pos)->Pos;\n"
1450 : " h:(Pos#Pos)->Pos;\n"
1451 : "var x,y,z,u,v:Pos;\n"
1452 : "eqn f(x,y)=x+y;\n"
1453 : " g(x,y)=x+y;\n"
1454 : " h(x,y)=x+x;\n"
1455 1 : );
1456 :
1457 1 : data_specification specification(parse_data_specification(s));
1458 :
1459 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
1460 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
1461 : {
1462 1 : std::cerr << " Strategy30: " << *strat << std::endl;
1463 1 : data::rewriter R(specification, *strat);
1464 :
1465 2 : data::data_expression e(parse_data_expression("f==g", specification));
1466 2 : data::data_expression f(parse_data_expression("true", specification));
1467 1 : data_rewrite_test(R, e, f);
1468 :
1469 1 : e(parse_data_expression("f==h", specification));
1470 1 : f(parse_data_expression("false", specification));
1471 1 : data_rewrite_test(R, e, f);
1472 1 : }
1473 1 : }
1474 :
1475 2 : BOOST_AUTO_TEST_CASE(Check_normal_forms_in_function_update) // In the jitty rewriter the internally used annotation Rewritten@@term
1476 : // was not always properly removed.
1477 : {
1478 : std::string s(
1479 : "sort F = Nat->Nat->Nat;\n"
1480 : "map a:F;\n"
1481 : " update:F#Nat#Nat#Nat->F;\n"
1482 : "var c:F;\n"
1483 : " i,j,x:Nat;\n"
1484 : "eqn update(c,i,j,x)=c[i->c(i)[j->x]];\n"
1485 1 : );
1486 :
1487 1 : data_specification specification(parse_data_specification(s));
1488 :
1489 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
1490 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
1491 : {
1492 1 : std::cerr << " Strategy31: " << *strat << std::endl;
1493 1 : data::rewriter R(specification, *strat);
1494 :
1495 2 : data::data_expression e(parse_data_expression("update(a,0,0,0)", specification));
1496 2 : data::data_expression f(R(parse_data_expression("a[0 -> a(0)[0 -> 0]]", specification)));
1497 1 : data_rewrite_test(R, e, f);
1498 1 : }
1499 1 : }
1500 :
1501 2 : BOOST_AUTO_TEST_CASE(Problem_with_recursive_templates_in_jittyc) // This rewrite system cannot stand the compiling rewriter
1502 : // if it uses templates freely. The templates will be
1503 : // used recursively, causing infinite template nesting, which
1504 : // the compiler cannot handle.
1505 : {
1506 : std::string s(
1507 : "map f:Nat#Nat->Nat;\n"
1508 : "var n,m:Nat;\n"
1509 : "eqn n>0 -> f(n,m)=f(Int2Nat(n-1),m+1);\n"
1510 1 : );
1511 :
1512 1 : data_specification specification(parse_data_specification(s));
1513 :
1514 1 : rewrite_strategy_vector strategies(data::detail::get_test_rewrite_strategies(false));
1515 2 : for (rewrite_strategy_vector::const_iterator strat = strategies.begin(); strat != strategies.end(); ++strat)
1516 : {
1517 1 : std::cerr << " Strategy32: " << *strat << std::endl;
1518 1 : data::rewriter R(specification, *strat);
1519 :
1520 2 : data::data_expression e(parse_data_expression("f(3,3)", specification));
1521 2 : data::data_expression f(parse_data_expression("f(0,6)", specification));
1522 1 : data_rewrite_test(R, e, f);
1523 1 : }
1524 1 : }
|
