Line data Source code
1 : // Author(s): Jeroen van der Wulp, 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 : #define BOOST_TEST_MODULE enumerator_test
10 : #include <boost/test/included/unit_test.hpp>
11 :
12 : #include "mcrl2/data/consistency.h"
13 : #include "mcrl2/data/detail/concepts.h"
14 : #include "mcrl2/data/enumerator_with_iterator.h"
15 : #include "mcrl2/data/optimized_boolean_operators.h"
16 : #include "mcrl2/data/parse.h"
17 : #include "mcrl2/data/print.h"
18 : #include "mcrl2/data/replace.h"
19 : #include "mcrl2/data/substitutions/mutable_map_substitution.h"
20 :
21 : using namespace mcrl2;
22 : using namespace mcrl2::data;
23 :
24 : // Example: parse_variable_list("x:Nat; y:Pos");
25 27 : variable_list parse_variable_list(const std::string& text, const data_specification& dataspec = detail::default_specification())
26 : {
27 27 : variable_vector result;
28 27 : parse_variables(text, std::back_inserter(result), dataspec);
29 54 : return variable_list(result.begin(), result.end());
30 27 : }
31 :
32 13 : void enumerate(const data_specification& dataspec,
33 : const variable_list& variables,
34 : const data_expression& expression,
35 : std::size_t expected_no_of_solutions,
36 : bool more_solutions_possible)
37 : {
38 : typedef enumerator_list_element_with_substitution<> enumerator_element;
39 : typedef enumerator_algorithm_with_iterator<> enumerator_type;
40 :
41 26 : data::enumerator_identifier_generator id_generator;
42 13 : rewriter rewr(dataspec);
43 13 : enumerator_type enumerator(rewr, dataspec, rewr, id_generator);
44 13 : std::size_t number_of_solutions = 0;
45 13 : mutable_indexed_substitution<> sigma;
46 13 : data::enumerator_queue<enumerator_element> enumerator_deque(enumerator_element(variables, expression));
47 13 : auto i = enumerator.begin(sigma, enumerator_deque);
48 124 : for ( ; number_of_solutions < expected_no_of_solutions && i != enumerator.end(); ++i)
49 : {
50 111 : mutable_map_substitution<> rho;
51 111 : i->add_assignments(variables, rho, rewr);
52 111 : std::cout << "solution = " << rho << std::endl;
53 111 : number_of_solutions++;
54 111 : }
55 13 : BOOST_CHECK(number_of_solutions == expected_no_of_solutions && (more_solutions_possible || i == enumerator.end()));
56 13 : }
57 :
58 13 : void enumerate(const std::string& dataspec_text,
59 : const std::string& variable_text,
60 : const std::string& expression_text,
61 : const std::string& free_variable_text,
62 : std::size_t number_of_solutions,
63 : bool more_solutions_possible)
64 : {
65 13 : data_specification dataspec = parse_data_specification(dataspec_text);
66 13 : variable_list variables = parse_variable_list(variable_text, dataspec);
67 13 : variable_list free_variables = parse_variable_list(free_variable_text, dataspec);
68 13 : data_expression expression = parse_data_expression(expression_text, free_variables, dataspec);
69 13 : enumerate(dataspec, variables, expression, number_of_solutions, more_solutions_possible);
70 13 : }
71 :
72 2 : BOOST_AUTO_TEST_CASE(empty_test)
73 : {
74 : typedef enumerator_list_element_with_substitution<> enumerator_element;
75 : typedef enumerator_algorithm_with_iterator<> enumerator_type;
76 :
77 : // test manual construction of rewr with rewriter
78 1 : data_specification dataspec;
79 1 : rewriter rewr(dataspec);
80 1 : variable_list variables;
81 :
82 1 : std::size_t count = 0;
83 2 : data::enumerator_identifier_generator id_generator;
84 :
85 : // explicit with condition rewr and condition
86 1 : enumerator_type enumerator(rewr, dataspec, rewr, id_generator);
87 :
88 1 : mutable_indexed_substitution<> sigma;
89 1 : data::enumerator_queue<enumerator_element> enumerator_deque(enumerator_element(variables, sort_bool::true_()));
90 2 : for (auto i = enumerator.begin(sigma, enumerator_deque); i != enumerator.end(); ++i)
91 : {
92 1 : count++;
93 : }
94 1 : BOOST_CHECK(count == 1);
95 :
96 : // explicit with condition but without condition rewr
97 1 : enumerator_deque.clear();
98 1 : enumerator_deque.push_back(enumerator_element(variables, sort_bool::true_()));
99 2 : for (auto i = enumerator.begin(sigma, enumerator_deque); i != enumerator.end(); ++i)
100 : {
101 1 : count++;
102 : }
103 1 : BOOST_CHECK(count == 2);
104 :
105 1 : variables = parse_variable_list("y: Nat;");
106 1 : enumerator_deque.clear();
107 1 : enumerator_deque.push_back(enumerator_element(variables, sort_bool::false_()));
108 1 : for (auto i = enumerator.begin(sigma, enumerator_deque); i != enumerator.end(); ++i)
109 : {
110 0 : BOOST_CHECK(false);
111 : }
112 1 : }
113 :
114 2 : BOOST_AUTO_TEST_CASE(list_test)
115 : {
116 : std::string dataspec_text =
117 : "sort list_of_booleans; \n"
118 : "cons empty : list_of_booleans; \n"
119 : " lcons : Bool # list_of_booleans -> list_of_booleans; \n"
120 : "map size : list_of_booleans -> Nat; \n"
121 : "var l : list_of_booleans; \n"
122 : " b : Bool; \n"
123 : "eqn size(empty) = 0; \n"
124 1 : " size(lcons(b,l)) = 1 + size(l); \n"
125 : ;
126 1 : std::string variable_text = "x: list_of_booleans; y: Nat;";
127 1 : std::string expression_text = "y == size(x) && 0 < y && y < 2";
128 1 : std::string free_variable_text = "x : list_of_booleans; y : Nat;";
129 1 : std::size_t number_of_solutions = 0;
130 1 : bool more_solutions_possible = true; // Changed!
131 1 : enumerate(dataspec_text, variable_text, expression_text, free_variable_text, number_of_solutions, more_solutions_possible);
132 1 : }
133 :
134 2 : BOOST_AUTO_TEST_CASE(structured_sort_test)
135 : {
136 : std::string dataspec_text =
137 : "sort D = struct d1(E) | d2(E); \n"
138 1 : " E = struct e1 | e2; \n"
139 : ;
140 1 : std::string variable_text = "d: D;";
141 1 : std::string expression_text = "forall d: D. d == e";
142 1 : std::string free_variable_text = "e: D;";
143 1 : std::size_t number_of_solutions = 4;
144 1 : bool more_solutions_possible = false;
145 1 : enumerate(dataspec_text, variable_text, expression_text, free_variable_text, number_of_solutions, more_solutions_possible);
146 1 : }
147 :
148 2 : BOOST_AUTO_TEST_CASE(equality_substitution_test)
149 : {
150 1 : std::string dataspec_text = "sort L = Nat;";
151 1 : std::string variable_text = "";
152 1 : std::string expression_text = "x == 17 && x != 17";
153 1 : std::string free_variable_text = "x : Pos;";
154 1 : std::size_t number_of_solutions = 0;
155 1 : bool more_solutions_possible = true; // Changed!
156 :
157 1 : std::clog << "Test1 equality\n";
158 1 : enumerate(dataspec_text, variable_text, expression_text, free_variable_text, number_of_solutions, more_solutions_possible);
159 :
160 1 : std::clog << "Test2 equality\n";
161 1 : expression_text = "x == 17 && x == x";
162 1 : number_of_solutions = 1;
163 1 : more_solutions_possible = false;
164 1 : enumerate(dataspec_text, variable_text, expression_text, free_variable_text, number_of_solutions, more_solutions_possible);
165 :
166 1 : std::clog << "Test3 equality\n";
167 1 : expression_text = "x == 17 && 2*x == 34";
168 1 : enumerate(dataspec_text, variable_text, expression_text, free_variable_text, number_of_solutions, more_solutions_possible);
169 :
170 1 : std::clog << "Test4 equality\n";
171 1 : variable_text = "";
172 1 : number_of_solutions = 1;
173 1 : enumerate(dataspec_text, variable_text, expression_text, free_variable_text, number_of_solutions, more_solutions_possible);
174 :
175 1 : std::clog << "Test4 equality: return two non exact solutions\n";
176 1 : variable_text = "b: Bool;";
177 1 : number_of_solutions = 2;
178 1 : enumerate(dataspec_text, variable_text, expression_text, free_variable_text, number_of_solutions, more_solutions_possible);
179 1 : }
180 :
181 2 : BOOST_AUTO_TEST_CASE(test_ticket_1486)
182 : {
183 1 : std::string dataspec_text = "sort L = Int;";
184 1 : std::string variable_text = "y : Nat;";
185 1 : std::string expression_text = "y + 20 == 25";
186 1 : std::string free_variable_text = "y : Nat;";
187 1 : std::size_t number_of_solutions = 1;
188 1 : bool more_solutions_possible = false;
189 1 : enumerate(dataspec_text, variable_text, expression_text, free_variable_text, number_of_solutions, more_solutions_possible);
190 1 : }
191 :
192 2 : BOOST_AUTO_TEST_CASE(tree_test)
193 : {
194 : std::string dataspec_text =
195 : "sort tree_with_booleans; \n"
196 : "cons leaf : Bool -> tree_with_booleans; \n"
197 1 : "cons node : tree_with_booleans # tree_with_booleans -> tree_with_booleans; \n"
198 : ;
199 1 : std::string variable_text = "x : tree_with_booleans;";
200 1 : std::string expression_text = "true";
201 1 : std::string free_variable_text = "";
202 1 : std::size_t number_of_solutions = 32;
203 1 : bool more_solutions_possible = true;
204 1 : enumerate(dataspec_text, variable_text, expression_text, free_variable_text, number_of_solutions, more_solutions_possible);
205 1 : }
206 :
207 2 : BOOST_AUTO_TEST_CASE(mutually_recursive_test)
208 : {
209 : std::string dataspec_text =
210 : "sort this; \n"
211 : " that; \n"
212 : "cons a : this; \n"
213 : " A : that -> this; \n"
214 : " b : that; \n"
215 : " B : this -> that; \n"
216 : "map maximum_a : Nat # this -> Bool; \n"
217 : " maximum_a : Nat # that -> Bool; \n"
218 : " maximum_b : Nat # this -> Bool; \n"
219 : " maximum_b : Nat # that -> Bool; \n"
220 : "var x : Nat; \n"
221 : " ax : this; \n"
222 : " bx : that; \n"
223 : "eqn maximum_a(x,A(bx)) = maximum_a(Int2Nat(x - 1),bx); \n"
224 : " maximum_a(0,a) = true; \n"
225 : " maximum_b(x,B(ax)) = maximum_b(Int2Nat(x - 1),ax); \n"
226 1 : " maximum_b(0,b) = true; \n"
227 : ;
228 :
229 1 : std::string variable_text = "x : this;";
230 1 : std::string expression_text = "true";
231 1 : std::string free_variable_text = "";
232 1 : std::size_t number_of_solutions = 32;
233 1 : bool more_solutions_possible = true;
234 1 : enumerate(dataspec_text, variable_text, expression_text, free_variable_text, number_of_solutions, more_solutions_possible);
235 :
236 1 : variable_text = "x : that;";
237 1 : enumerate(dataspec_text, variable_text, expression_text, free_variable_text, number_of_solutions, more_solutions_possible);
238 1 : }
239 :
240 2 : BOOST_AUTO_TEST_CASE(set_test)
241 : {
242 1 : std::string dataspec_text = "sort Dummy;\n";
243 1 : std::string variable_text = "f: Set(Bool);";
244 1 : std::string expression_text = "true in f";
245 1 : std::string free_variable_text = "f: Set(Bool);";
246 1 : std::size_t number_of_solutions = 4;
247 1 : bool more_solutions_possible = false;
248 1 : enumerate(dataspec_text, variable_text, expression_text, free_variable_text, number_of_solutions, more_solutions_possible);
249 1 : }
250 :
251 : inline
252 23 : data_expression_vector generate_values(const data_specification& dataspec, const sort_expression& s, std::size_t max_size = 1000)
253 : {
254 : typedef enumerator_list_element_with_substitution<> enumerator_element;
255 : typedef enumerator_algorithm_with_iterator<> enumerator_type;
256 :
257 23 : std::size_t max_internal_variables = 10000;
258 23 : data_expression_vector result;
259 46 : data::enumerator_identifier_generator id_generator;
260 :
261 23 : rewriter rewr(dataspec);
262 23 : enumerator_type enumerator(rewr, dataspec, rewr, id_generator, max_internal_variables);
263 46 : variable v("x", s);
264 23 : variable_list variables;
265 23 : variables.push_front(v);
266 23 : mutable_indexed_substitution<> sigma;
267 23 : data::enumerator_queue<enumerator_element> enumerator_deque(enumerator_element(variables, sort_bool::true_()));
268 133 : for (auto i = enumerator.begin(sigma, enumerator_deque); i != enumerator.end() ; ++i)
269 : {
270 116 : i->add_assignments(variables, sigma, rewr);
271 116 : result.push_back(sigma(variables.front()));
272 116 : if (result.size() >= max_size)
273 : {
274 6 : break;
275 : }
276 : }
277 46 : return result;
278 23 : }
279 :
280 23 : bool no_duplicates(const data_expression_vector& v)
281 : {
282 23 : std::set<data_expression> s;
283 23 : s.insert(v.begin(), v.end());
284 46 : return s.size() == v.size();
285 23 : }
286 :
287 2 : BOOST_AUTO_TEST_CASE(generate_values_test)
288 : {
289 : std::string DATASPEC =
290 : "sort Identifiers = struct t1 | t2 | t3 | t4 | t5 | p1 | p2 | s1 | r1 | r2 | r3 | IL; \n"
291 : " signal_Messages = struct ic_set_proceed_signal | ic_set_stop_signal; \n"
292 : " track_Messages = struct dv_free_track | dv_occupied_track; \n"
293 : " point_Messages = struct ic_move_right_point | ic_move_left_point | dv_at_right_point | dv_at_left_point; \n"
294 : " route_Messages = struct ic_cancel_route_route | ic_set_route_route; \n"
295 : " Interlocking_Messages = struct c_set_stop | c_move_left | c_set_route | c_IL_off | c_cancel_route | tc_set_proceed | c_IL_on | c_move_right; \n"
296 : " environment_Messages = struct i_signal_status_proceed_signal_environment | i_signal_status_stop_signal_environment | i_track_status_occupied_track_environment | \n"
297 : " i_track_status_free_track_environment | i_point_at_right_point_environment | i_point_locked_point_environment | i_point_ok_point_environment | \n"
298 : " i_point_broken_point_environment | i_point_at_left_point_environment | i_route_cancelled_route_environment | i_route_established_route_environment; \n"
299 : " rail_yard_Messages = struct sv_set_proceed_signal_railyard | sv_set_stop_signal_railyard | sv_move_right_point_railyard | sv_move_left_point_railyard; \n"
300 : " Enum3 = struct e2_3 | e1_3 | e0_3; \n"
301 : " track__ready_States = struct track__ready_free_substate | track__ready_occupied_substate | track__ready_startup_substate | track__ready_nop; \n"
302 : " Enum15 = struct e14_15 | e13_15 | e12_15 | e11_15 | e10_15 | e9_15 | e8_15 | e7_15 | e6_15 | e5_15 | e4_15 | e3_15 | e2_15 | e1_15 | e0_15; \n"
303 : " point_States = struct point__broken_substate | point__startup_substate | point__working_substate; \n"
304 : " point__working_States = struct point__working_right_substate | point__working_left_substate | point__working_moving_substate | point__working_nop; \n"
305 : " point__working_moving_States = struct point__working_moving_left_substate | point__working_moving_right_substate | point__working_moving_nop; \n"
306 : " Enum7 = struct e6_7 | e5_7 | e4_7 | e3_7 | e2_7 | e1_7 | e0_7; \n"
307 : " signal_States = struct signal__stop_substate | signal__proceed_substate; \n"
308 : " Enum10 = struct e9_10 | e8_10 | e7_10 | e6_10 | e5_10 | e4_10 | e3_10 | e2_10 | e1_10 | e0_10; \n"
309 : " route_States = struct route__idle_substate | route__established_substate | route__setting_up_substate; \n"
310 : " route__established_States = struct route__established_in_use_substate | route__established_active_substate | route__established_nop; \n"
311 : " Enum11 = struct e10_11 | e9_11 | e8_11 | e7_11 | e6_11 | e5_11 | e4_11 | e3_11 | e2_11 | e1_11 | e0_11; \n"
312 : " Enum13 = struct e12_13 | e11_13 | e10_13 | e9_13 | e8_13 | e7_13 | e6_13 | e5_13 | e4_13 | e3_13 | e2_13 | e1_13 | e0_13; \n"
313 : " HAL_device_States = struct HAL_device__normal_substate; \n"
314 1 : " track_States = struct track__ready_substate; \n"
315 : ;
316 1 : data_specification dataspec = parse_data_specification(DATASPEC);
317 :
318 1 : for (const sort_expression& sort: dataspec.user_defined_sorts())
319 : {
320 0 : sort_expression s = normalize_sorts(sort, dataspec);
321 0 : std::clog << "--- sort " << data::pp(s) << std::endl;
322 0 : data_expression_vector v = generate_values(dataspec, s, 10);
323 0 : std::clog << " possible values: " << core::detail::print_set(v) << std::endl;
324 0 : BOOST_CHECK(v.size() <= 10);
325 0 : BOOST_CHECK(no_duplicates(v));
326 0 : }
327 :
328 24 : for (const alias& a: dataspec.user_defined_aliases())
329 : {
330 23 : sort_expression s = normalize_sorts(a.reference(),dataspec);
331 23 : std::clog << "--- sort " << data::pp(s) << std::endl;
332 23 : data_expression_vector v = generate_values(dataspec, s, 10);
333 23 : std::clog << " possible values: " << core::detail::print_set(v) << std::endl;
334 23 : BOOST_CHECK(v.size() <= 10);
335 23 : BOOST_CHECK(no_duplicates(v));
336 23 : }
337 1 : }
338 :
339 2 : BOOST_AUTO_TEST_CASE(constructors_that_are_not_a_normal_form_test)
340 : {
341 : std::string dataspec_text =
342 : "sort FloorID = struct F1 | F2;\n"
343 : " \n"
344 : "map fSucc : FloorID -> FloorID;\n"
345 : " equal : FloorID # FloorID -> Bool;\n"
346 : "\n"
347 : "var f,g : FloorID;\n"
348 : "eqn F2 = fSucc(F1); \n"
349 : " equal(fSucc(f),fSucc(g)) = equal(f,g);\n"
350 : " equal(fSucc(f),F1) = false;\n"
351 : " equal(F1,fSucc(g)) = false;\n"
352 : " equal(F1,F1) = true;\n"
353 1 : " f==g = equal(f,g);\n"
354 : ;
355 1 : std::string variable_text = "f: FloorID;";
356 1 : std::string expression_text = "equal(f, F2)";
357 1 : const std::string& free_variable_text = variable_text;
358 1 : std::size_t number_of_solutions = 1;
359 1 : bool more_solutions_possible = false;
360 1 : enumerate(dataspec_text, variable_text, expression_text, free_variable_text, number_of_solutions, more_solutions_possible);
361 1 : }
362 :
363 2 : BOOST_AUTO_TEST_CASE(cannot_enumerate_real_default)
364 : {
365 : typedef data::enumerator_list_element<data_expression> enumerator_element;
366 :
367 1 : data_expression result = data::sort_bool::true_();
368 3 : data::variable_list v = { data::variable("r", data::sort_real::real_()) };
369 2 : data_expression phi = parse_data_expression("r == r", v);
370 1 : data::data_specification dataspec;
371 1 : dataspec.add_context_sort(data::sort_real::real_());
372 1 : data::rewriter R(dataspec);
373 2 : data::enumerator_identifier_generator id_generator("x");
374 1 : data::enumerator_algorithm<> E(R, dataspec, R, id_generator, (std::numeric_limits<std::size_t>::max)());
375 1 : data::rewriter::substitution_type sigma;
376 :
377 : try
378 : {
379 3 : E.enumerate(enumerator_element(v, phi),
380 : sigma,
381 0 : [&](const enumerator_element& p)
382 : {
383 0 : data::optimized_and(result, result, p.expression());
384 0 : return result == data::sort_bool::false_();
385 : },
386 : is_true,
387 : is_false
388 : );
389 : }
390 1 : catch (mcrl2::runtime_error& e)
391 : {
392 1 : std::cout << e.what() << std::endl;
393 1 : return;
394 1 : }
395 0 : BOOST_CHECK(false);
396 8 : }
397 :
398 2 : BOOST_AUTO_TEST_CASE(cannot_enumerate_real_with_substitution)
399 : {
400 : typedef data::enumerator_list_element_with_substitution<data_expression> enumerator_element;
401 :
402 1 : data::data_specification dataspec;
403 1 : dataspec.add_context_sort(data::sort_real::real_());
404 1 : data::rewriter R(dataspec);
405 1 : data::variable_list v;
406 1 : v.push_front(data::variable("r", data::sort_real::real_()));
407 2 : data_expression phi = parse_data_expression("r == r", v);
408 1 : data::mutable_indexed_substitution<> sigma;
409 1 : std::size_t max_count = 1000;
410 1 : bool throw_exceptions = true;
411 2 : data::enumerator_identifier_generator id_generator;
412 1 : data::enumerator_algorithm_with_iterator<rewriter, enumerator_element> E(R, dataspec, R, id_generator, max_count, throw_exceptions);
413 1 : data::enumerator_queue<enumerator_element> P(enumerator_element(v, phi));
414 : try {
415 1 : for (auto i = E.begin(sigma, P); i != E.end() ; ++i)
416 : {
417 : // skip
418 : }
419 : }
420 1 : catch (mcrl2::runtime_error& e)
421 : {
422 1 : std::cout << e.what() << std::endl;
423 1 : return;
424 1 : }
425 0 : BOOST_CHECK(false);
426 8 : }
427 :
428 2 : BOOST_AUTO_TEST_CASE(enumerate_callback)
429 : {
430 : typedef data::enumerator_list_element<data_expression> enumerator_element;
431 2 : enumerator_identifier_generator id_generator;
432 1 : data_specification dataspec;
433 1 : dataspec.add_context_sort(data::sort_int::int_());
434 1 : std::size_t max_count = 10;
435 1 : data::rewriter r(dataspec);
436 1 : data::enumerator_algorithm<rewriter> E(r, dataspec, r, id_generator, max_count);
437 :
438 2 : auto enumerate = [&](const data_expression& x)
439 : {
440 2 : data::mutable_indexed_substitution<> sigma;
441 2 : data_expression result;
442 2 : id_generator.clear();
443 2 : if (is_forall(x))
444 : {
445 1 : const auto& x_ = atermpp::down_cast<forall>(x);
446 1 : result = true_();
447 1 : E.enumerate(enumerator_element(x_.variables(), r(x_.body())),
448 : sigma,
449 1 : [&](const enumerator_element& p)
450 : {
451 1 : data::optimized_and(result, result, p.expression());
452 1 : return is_false(result);
453 : },
454 : is_true,
455 : is_false
456 : );
457 : }
458 1 : else if (is_exists(x))
459 : {
460 1 : const exists& x_ = atermpp::down_cast<exists>(x);
461 1 : result = false_();
462 1 : E.enumerate(enumerator_element(x_.variables(), r(x_.body())),
463 : sigma,
464 1 : [&](const enumerator_element& p)
465 : {
466 1 : data::optimized_or(result, result, p.expression());
467 1 : return is_true(result);
468 : },
469 : is_false,
470 : is_true
471 : );
472 : }
473 4 : return result;
474 3 : };
475 :
476 1 : BOOST_CHECK_EQUAL(enumerate(parse_data_expression("forall n: Nat. n < 2")), false_());
477 1 : BOOST_CHECK_EQUAL(enumerate(parse_data_expression("exists n: Nat. n < 2")), true_());
478 1 : }
479 :
480 2 : BOOST_AUTO_TEST_CASE(enumerate_expressions_test)
481 : {
482 : const std::string dataspec_text =
483 : "sort D = struct d1(E) | d2(E);\n"
484 1 : " E = struct e1 | e2; \n"
485 : ;
486 1 : std::string variable_text = "d:D";
487 1 : data_specification dataspec = parse_data_specification(dataspec_text);
488 1 : data::variable v = parse_variable(variable_text, dataspec);
489 1 : rewriter r(dataspec);
490 :
491 1 : data::data_expression_vector result_as_vector = enumerate_expressions(v.sort(), dataspec, r);
492 :
493 1 : std::set<data::data_expression> result(result_as_vector.begin(), result_as_vector.end());
494 : std::set<data::data_expression> expected_result = {
495 : parse_data_expression("d1(e2)", dataspec),
496 : parse_data_expression("d1(e1)", dataspec),
497 : parse_data_expression("d2(e2)", dataspec),
498 : parse_data_expression("d2(e1)", dataspec)
499 7 : };
500 :
501 1 : BOOST_CHECK_EQUAL_COLLECTIONS(result.begin(), result.end(), expected_result.begin(), expected_result.end());
502 1 : }
|