1 /* Header file for test programs.
2 Copyright (C) 2001-2010 Roberto Bagnara <bagnara@cs.unipr.it>
3 Copyright (C) 2010-2016 BUGSENG srl (http://bugseng.com)
4
5 This file is part of the Parma Polyhedra Library (PPL).
6
7 The PPL is free software; you can redistribute it and/or modify it
8 under the terms of the GNU General Public License as published by the
9 Free Software Foundation; either version 3 of the License, or (at your
10 option) any later version.
11
12 The PPL is distributed in the hope that it will be useful, but WITHOUT
13 ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
14 FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License
15 for more details.
16
17 You should have received a copy of the GNU General Public License
18 along with this program; if not, write to the Free Software Foundation,
19 Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02111-1307, USA.
20
21 For the most up-to-date information see the Parma Polyhedra Library
22 site: http://bugseng.com/products/ppl/ . */
23
24 #ifndef PPL_ppl_test_hh
25 #define PPL_ppl_test_hh 1
26
27 #include "ppl_header.hh"
28 #include "Random_Number_Generator_defs.hh"
29 #include <stdexcept>
30 #include <sstream>
31 #include <list>
32 #include <map>
33 #include <iterator>
34 #include <string>
35 #include <iostream>
36 #include <algorithm>
37 #include <typeinfo>
38 #include <cstdlib>
39
40 #ifndef NOISY
41 #define NOISY 0
42 #endif
43
44 #ifndef VERY_NOISY
45 #define VERY_NOISY 0
46 #endif
47
48 #define TRY try
49
50 #define CATCH \
51 catch (const std::overflow_error& e) { \
52 std::cerr << "arithmetic overflow (" << e.what() << ")" \
53 << std::endl; \
54 exit(1); \
55 } \
56 catch (const std::exception& e) { \
57 std::cerr << "std::exception caught: " \
58 << e.what() << " (type == " << typeid(e).name() << ")" \
59 << std::endl; \
60 exit(1); \
61 }
62
63 #define BEGIN_MAIN \
64 int \
65 main() try { \
66 set_handlers(); \
67 bool succeeded = false; \
68 bool overflow = false; \
69 (void) overflow; \
70 std::list<std::string> failed_tests; \
71 std::list<std::string> unexpectedly_succeeded_tests;
72
73 #define END_MAIN \
74 if (!failed_tests.empty()) { \
75 std::cerr << "tests failed: "; \
76 std::copy(failed_tests.begin(), \
77 failed_tests.end(), \
78 std::ostream_iterator<std::string>(std::cerr, " ")); \
79 std::cerr << std::endl; \
80 return 1; \
81 } \
82 if (!unexpectedly_succeeded_tests.empty()) { \
83 std::cerr << "tests unexpectedly succeeded: "; \
84 std::copy(unexpectedly_succeeded_tests.begin(), \
85 unexpectedly_succeeded_tests.end(), \
86 std::ostream_iterator<std::string>(std::cerr, " ")); \
87 std::cerr << std::endl; \
88 return 1; \
89 } \
90 return 0; \
91 } \
92 catch (const std::overflow_error& e) { \
93 std::cerr << "arithmetic overflow (" << e.what() << ")" \
94 << std::endl; \
95 exit(1); \
96 } \
97 catch (const std::exception& e) { \
98 std::cerr << "std::exception caught: " \
99 << e.what() << " (type == " << typeid(e).name() << ")" \
100 << std::endl; \
101 exit(1); \
102 }
103
104 #define ANNOUNCE_TEST(test) \
105 nout << "\n=== " #test " ===" << std::endl
106
107 #define RUN_TEST(test) \
108 try { \
109 overflow = false; \
110 succeeded = test(); \
111 } \
112 catch (const std::overflow_error& e) { \
113 nout << "arithmetic overflow (" << e.what() << ")" \
114 << std::endl; \
115 overflow = true; \
116 succeeded = false; \
117 } \
118 catch (const std::exception& e) { \
119 nout << "std::exception caught: " \
120 << e.what() << " (type == " << typeid(e).name() << ")" \
121 << std::endl; \
122 succeeded = false; \
123 } \
124 catch (...) { \
125 nout << "unknown exception caught" \
126 << std::endl; \
127 succeeded = false; \
128 }
129
130 #define DO_TEST(test) \
131 ANNOUNCE_TEST(test); \
132 RUN_TEST(test); \
133 if (!succeeded) \
134 failed_tests.push_back(#test);
135
136 #define DO_TEST_F(test) \
137 ANNOUNCE_TEST(test); \
138 RUN_TEST(test); \
139 if (succeeded) \
140 unexpectedly_succeeded_tests.push_back(#test);
141
142 #define DO_TEST_OVERFLOW(test) \
143 ANNOUNCE_TEST(test); \
144 RUN_TEST(test); \
145 if (succeeded) \
146 unexpectedly_succeeded_tests.push_back(#test); \
147 else if (!overflow) \
148 failed_tests.push_back(#test);
149
150 #define DO_TEST_MAY_OVERFLOW_IF_INEXACT(test, shape) \
151 ANNOUNCE_TEST(test); \
152 RUN_TEST(test); \
153 if (!succeeded) \
154 if (!overflow || has_exact_coefficient_type(shape(0, EMPTY))) \
155 failed_tests.push_back(#test);
156
157
158 // Macros for arbitrary combination of preprocessor conditions.
159
160 #define PPL_CPP_AND_false_false false
161 #define PPL_CPP_AND_false_true false
162 #define PPL_CPP_AND_true_false false
163 #define PPL_CPP_AND_true_true true
164 #define PPL_CPP_AND_(x,y) PPL_CPP_AND_ ## x ## _ ## y
165 #define PPL_CPP_AND(x,y) PPL_CPP_AND_(x, y)
166
167 #define PPL_CPP_OR_false_false false
168 #define PPL_CPP_OR_false_true true
169 #define PPL_CPP_OR_true_false true
170 #define PPL_CPP_OR_true_true true
171 #define PPL_CPP_OR_(x,y) PPL_CPP_OR_ ## x ## _ ## y
172 #define PPL_CPP_OR(x,y) PPL_CPP_OR_(x, y)
173
174 #define PPL_CPP_NOT_false true
175 #define PPL_CPP_NOT_true false
176 #define PPL_CPP_NOT_(x) PPL_CPP_NOT_ ## x
177 #define PPL_CPP_NOT(x) PPL_CPP_NOT_(x)
178
179 #define PPL_CPP_VAL_true_ true
180 #define PPL_CPP_VAL_false_ false
181 #define PPL_CPP_VAL_false(v) PPL_CPP_VAL_true
182 #define PPL_CPP_VAL_b(v) PPL_CPP_VAL_false
183 #define PPL_CPP_VAL_a(v) PPL_CPP_VAL_b(v)
184
185 #define PPL_CPP_IS_NEGx_arg_neg 0)(0
186 #define PPL_CPP_IS_NEGx(v) PPL_CPP_VAL_a(PPL_CPP_IS_NEGx_arg_##v)
187
188 #define PPL_CPP_IS_NEG__(v) v ## _
189 #define PPL_CPP_IS_NEG_(v) PPL_CPP_IS_NEG__(v)
190 #define PPL_CPP_IS_NEG(v) PPL_CPP_IS_NEG_(PPL_CPP_IS_NEGx(v))
191
192 #define PPL_CPP_IS_ZEROx_arg_0 0)(0
193 #define PPL_CPP_IS_ZEROx(v) PPL_CPP_VAL_a(PPL_CPP_IS_ZEROx_arg_##v)
194
195 #define PPL_CPP_IS_ZERO__(v) v ## _
196 #define PPL_CPP_IS_ZERO_(v) PPL_CPP_IS_ZERO__(v)
197 #define PPL_CPP_IS_ZERO(v) PPL_CPP_IS_ZERO_(PPL_CPP_IS_ZEROx(v))
198
199 #define PPL_CPP_DECR_neg neg
200 #define PPL_CPP_DECR_0 neg
201 #define PPL_CPP_DECR_1 0
202 #define PPL_CPP_DECR_2 1
203 #define PPL_CPP_DECR_3 2
204 #define PPL_CPP_DECR_4 3
205 #define PPL_CPP_DECR_5 4
206 #define PPL_CPP_DECR_6 5
207 #define PPL_CPP_DECR_7 6
208 #define PPL_CPP_DECR_8 7
209 #define PPL_CPP_DECR_9 8
210
211 #define PPL_CPP_DECR_(x) PPL_CPP_DECR_ ## x
212 #define PPL_CPP_DECR(x) PPL_CPP_DECR_(x)
213
214 #define PPL_CPP_SUB_0(x) x
215 #define PPL_CPP_SUB_1(x) PPL_CPP_DECR(x)
216 #define PPL_CPP_SUB_2(x) PPL_CPP_DECR(PPL_CPP_SUB_1(x))
217 #define PPL_CPP_SUB_3(x) PPL_CPP_DECR(PPL_CPP_SUB_2(x))
218 #define PPL_CPP_SUB_4(x) PPL_CPP_DECR(PPL_CPP_SUB_3(x))
219 #define PPL_CPP_SUB_5(x) PPL_CPP_DECR(PPL_CPP_SUB_4(x))
220 #define PPL_CPP_SUB_6(x) PPL_CPP_DECR(PPL_CPP_SUB_5(x))
221 #define PPL_CPP_SUB_7(x) PPL_CPP_DECR(PPL_CPP_SUB_6(x))
222 #define PPL_CPP_SUB_8(x) PPL_CPP_DECR(PPL_CPP_SUB_7(x))
223 #define PPL_CPP_SUB_9(x) PPL_CPP_DECR(PPL_CPP_SUB_8(x))
224
225 #define PPL_CPP_SUB_(x, y) PPL_CPP_SUB_ ## y (x)
226 #define PPL_CPP_SUB(x, y) PPL_CPP_SUB_(x, y)
227
228 #define PPL_CPP_LT(x, y) PPL_CPP_IS_NEG(PPL_CPP_SUB(x, y))
229 #define PPL_CPP_GT(x, y) PPL_CPP_LT(y, x)
230 #define PPL_CPP_LE(x, y) PPL_CPP_NOT(PPL_CPP_LT(y, x))
231 #define PPL_CPP_GE(x, y) PPL_CPP_NOT(PPL_CPP_LT(x, y))
232 #define PPL_CPP_EQ(x, y) PPL_CPP_IS_ZERO(PPL_CPP_SUB(x, y))
233 #define PPL_CPP_NE(x, y) PPL_CPP_NOT(PPL_CPP_EQ(x,y))
234
235 #define PPL_CPP_LOG2_64 6
236 #define PPL_CPP_LOG2_32 5
237 #define PPL_CPP_LOG2_16 4
238 #define PPL_CPP_LOG2_8 3
239 #define PPL_CPP_LOG2_0 neg
240
241 #define PPL_CPP_LOG2_(x) PPL_CPP_LOG2_ ## x
242 #define PPL_CPP_LOG2(x) PPL_CPP_LOG2_(x)
243
244 #define COND_MACRO_2(prefix, v) prefix ## _ ## v
245 #define COND_MACRO_1(prefix, v) COND_MACRO_2(prefix, v)
246 #define COND_MACRO(prefix, expr) COND_MACRO_1(prefix, expr)
247
248
249 #define PPL_CPP_LOGBITS PPL_CPP_LOG2(PPL_COEFFICIENT_BITS)
250
251 #define COND_F64 PPL_CPP_LT(PPL_CPP_LOGBITS, 0)
252 #define COND_F32 PPL_CPP_OR(PPL_CPP_GT(PPL_CPP_LOGBITS, 5), \
253 PPL_CPP_LT(PPL_CPP_LOGBITS, 0))
254 #define COND_F16 PPL_CPP_OR(PPL_CPP_GT(PPL_CPP_LOGBITS, 4), \
255 PPL_CPP_LT(PPL_CPP_LOGBITS, 0))
256 #define COND_F8 PPL_CPP_OR(PPL_CPP_GT(PPL_CPP_LOGBITS, 3), \
257 PPL_CPP_LT(PPL_CPP_LOGBITS, 0))
258
259 #ifndef NDEBUG
260 # define COND_ASSERT_OFF false
261 #else
262 # define COND_ASSERT_OFF true
263 #endif
264
265 #define COND_SUCC_64_ONLY \
266 PPL_CPP_AND(PPL_CPP_EQ(PPL_CPP_LOGBITS, 6), COND_ASSERT_OFF)
267 #define COND_SUCC_32_ONLY \
268 PPL_CPP_AND(PPL_CPP_EQ(PPL_CPP_LOGBITS, 5), COND_ASSERT_OFF)
269 #define COND_SUCC_16_ONLY \
270 PPL_CPP_AND(PPL_CPP_EQ(PPL_CPP_LOGBITS, 4), COND_ASSERT_OFF)
271 #define COND_SUCC_8_ONLY \
272 PPL_CPP_AND(PPL_CPP_EQ(PPL_CPP_LOGBITS, 3), COND_ASSERT_OFF)
273
274 #define COND_F64A PPL_CPP_OR(COND_F64, COND_SUCC_64_ONLY)
275 #define COND_F32A PPL_CPP_OR(COND_F32, COND_SUCC_32_ONLY)
276 #define COND_F16A PPL_CPP_OR(COND_F16, COND_SUCC_16_ONLY)
277 #define COND_F8A PPL_CPP_OR(COND_F8, COND_SUCC_8_ONLY)
278
279
280 #define COND_DO_TEST_false(test) DO_TEST_OVERFLOW(test)
281 #define COND_DO_TEST_true(test) DO_TEST(test)
282 #define COND_DO_TEST(cond, test) COND_MACRO(COND_DO_TEST, cond)(test)
283
284 #define DO_TEST_F64(test) COND_DO_TEST(COND_F64, test)
285 #define DO_TEST_F64A(test) COND_DO_TEST(COND_F64A, test)
286 #define DO_TEST_F32(test) COND_DO_TEST(COND_F32, test)
287 #define DO_TEST_F32A(test) COND_DO_TEST(COND_F32A, test)
288 #define DO_TEST_F16(test) COND_DO_TEST(COND_F16, test)
289 #define DO_TEST_F16A(test) COND_DO_TEST(COND_F16A, test)
290 #define DO_TEST_F8(test) COND_DO_TEST(COND_F8, test)
291 #define DO_TEST_F8A(test) COND_DO_TEST(COND_F8A, test)
292
293
294 #define COND_DO_TEST_MAY_OVERFLOW_IF_INEXACT_false(test, shape) \
295 DO_TEST_OVERFLOW(test)
296 #define COND_DO_TEST_MAY_OVERFLOW_IF_INEXACT_true(test, shape) \
297 DO_TEST_MAY_OVERFLOW_IF_INEXACT(test, shape)
298 #define COND_DO_TEST_MAY_OVERFLOW_IF_INEXACT(cond, test, shape) \
299 COND_MACRO(COND_DO_TEST_MAY_OVERFLOW_IF_INEXACT, cond)(test, shape)
300
301 #define DO_TEST_F64_MAY_OVERFLOW_IF_INEXACT(test, shape) \
302 COND_DO_TEST_MAY_OVERFLOW_IF_INEXACT(COND_F64, test, shape)
303 #define DO_TEST_F64A_MAY_OVERFLOW_IF_INEXACT(test, shape) \
304 COND_DO_TEST_MAY_OVERFLOW_IF_INEXACT(COND_F64A, test, shape)
305 #define DO_TEST_F32_MAY_OVERFLOW_IF_INEXACT(test, shape) \
306 COND_DO_TEST_MAY_OVERFLOW_IF_INEXACT(COND_F32, test, shape)
307 #define DO_TEST_F32A_MAY_OVERFLOW_IF_INEXACT(test, shape) \
308 COND_DO_TEST_MAY_OVERFLOW_IF_INEXACT(COND_F32A, test, shape)
309 #define DO_TEST_F16_MAY_OVERFLOW_IF_INEXACT(test, shape) \
310 COND_DO_TEST_MAY_OVERFLOW_IF_INEXACT(COND_F16, test, shape)
311 #define DO_TEST_F16A_MAY_OVERFLOW_IF_INEXACT(test, shape) \
312 COND_DO_TEST_MAY_OVERFLOW_IF_INEXACT(COND_F16A, test, shape)
313 #define DO_TEST_F8_MAY_OVERFLOW_IF_INEXACT(test, shape) \
314 COND_DO_TEST_MAY_OVERFLOW_IF_INEXACT(COND_F8, test, shape)
315 #define DO_TEST_F8A_MAY_OVERFLOW_IF_INEXACT(test, shape) \
316 COND_DO_TEST_MAY_OVERFLOW_IF_INEXACT(COND_F8A, test, shape)
317
318 // Encoding floating point formats.
319 #define PPL_CPP_FP_FORMAT_float 1
320 #define PPL_CPP_FP_FORMAT_double 2
321 #define PPL_CPP_FP_FORMAT_long_double 3
322 #define PPL_CPP_FP_FORMAT_float_ieee754_single 4
323 #define PPL_CPP_FP_FORMAT_float_ieee754_double 5
324 #define PPL_CPP_FP_FORMAT_float_ieee754_quad 6
325 #define PPL_CPP_FP_FORMAT_(format) PPL_CPP_FP_FORMAT_ ## format
326 #define PPL_CPP_FP_FORMAT(format) PPL_CPP_FP_FORMAT_(format)
327
328
329 // Turn s into a string: PPL_TEST_STR(x + y) => "x + y".
330 #define PPL_TEST_STR(s) #s
331
332 // Turn the expansion of s into a string: PPL_TEST_XSTR(x) => "s expanded".
333 #define PPL_TEST_XSTR(s) PPL_TEST_STR(s)
334
335
336 #ifdef DERIVED_TEST
337 #define C_Polyhedron NNC_Polyhedron
338 #endif
339
340 #ifndef BOX_INSTANCE
341 #define BOX_INSTANCE rt_r_oc
342 #endif
343
344 #ifndef BD_SHAPE_INSTANCE
345 #define BD_SHAPE_INSTANCE mpq_class
346 #endif
347
348 #ifndef OCTAGONAL_SHAPE_INSTANCE
349 #define OCTAGONAL_SHAPE_INSTANCE mpq_class
350 #endif
351
352 namespace Parma_Polyhedra_Library {
353
354 namespace Test {
355
356 static bool
check_noisy(const char * environment_variable)357 check_noisy(const char*
358 #if PPL_HAVE_DECL_GETENV || NOISY || VERY_NOISY
359 environment_variable
360 #endif
361 ) {
362 #if PPL_HAVE_DECL_GETENV
363 return getenv(environment_variable) != 0;
364 #else
365 #if NOISY
366 if (strcmp(environment_variable, "PPL_NOISY_TESTS") == 0)
367 return true;
368 #endif
369 #if VERY_NOISY
370 if (strcmp(environment_variable, "PPL_VERY_NOISY_TESTS") == 0)
371 return true;
372 #endif
373 return false;
374 #endif // !PPL_HAVE_DECL_GETENV
375 }
376
377 template<typename CharT, typename Traits = std::char_traits<CharT> >
378 class nullbuf : public std::basic_streambuf<CharT, Traits> {
379 protected:
overflow(typename Traits::int_type c)380 virtual typename Traits::int_type overflow(typename Traits::int_type c) {
381 return Traits::not_eof(c);
382 }
383 };
384
385 template <class CharT, class Traits = std::char_traits<CharT> >
386 class noisy_ostream : public std::basic_ostream<CharT, Traits> {
387 private:
388 nullbuf<CharT, Traits> black_hole;
389
390 public:
noisy_ostream(const std::basic_ostream<CharT,Traits> & os,const char * environment_variable)391 noisy_ostream(const std::basic_ostream<CharT, Traits>& os,
392 const char* environment_variable)
393 : std::basic_ostream<CharT, Traits>(check_noisy(environment_variable)
394 ? os.rdbuf()
395 : &black_hole) {
396 }
397 };
398
399 static noisy_ostream<char> nout(std::cout, "PPL_NOISY_TESTS");
400 static noisy_ostream<char> vnout(std::cout, "PPL_VERY_NOISY_TESTS");
401
402 void
403 set_handlers();
404
405 //! Utility typedef to allow a macro argument to denote the long double type.
406 typedef long double long_double;
407
408 struct Floating_Real_Open_Interval_Info_Policy {
409 const_bool_nodef(store_special, false);
410 const_bool_nodef(store_open, true);
411 const_bool_nodef(cache_empty, true);
412 const_bool_nodef(cache_singleton, true);
413 const_bool_nodef(cache_normalized, false);
414 const_int_nodef(next_bit, 0);
415 const_bool_nodef(may_be_empty, true);
416 const_bool_nodef(may_contain_infinity, false);
417 const_bool_nodef(check_empty_result, false);
418 const_bool_nodef(check_inexact, false);
419 };
420
421 struct Floating_Real_Closed_Interval_Info_Policy {
422 const_bool_nodef(store_special, false);
423 const_bool_nodef(store_open, false);
424 const_bool_nodef(cache_empty, false);
425 const_bool_nodef(cache_singleton, true);
426 const_bool_nodef(cache_normalized, false);
427 const_int_nodef(next_bit, 0);
428 const_bool_nodef(may_be_empty, false);
429 const_bool_nodef(may_contain_infinity, false);
430 const_bool_nodef(check_empty_result, false);
431 const_bool_nodef(check_inexact, false);
432 };
433
434 typedef Interval_Info_Bitset<unsigned int,
435 Floating_Real_Open_Interval_Info_Policy> Floating_Real_Open_Interval_Info;
436
437 typedef Interval<float, Floating_Real_Open_Interval_Info> fl_r_oc;
438 typedef Interval<double, Floating_Real_Open_Interval_Info> db_r_oc;
439 typedef Interval<long double, Floating_Real_Open_Interval_Info> ld_r_oc;
440
441 struct Rational_Real_Open_Interval_Info_Policy {
442 const_bool_nodef(store_special, true);
443 const_bool_nodef(store_open, true);
444 const_bool_nodef(cache_empty, true);
445 const_bool_nodef(cache_singleton, true);
446 const_bool_nodef(cache_normalized, false);
447 const_int_nodef(next_bit, 0);
448 const_bool_nodef(may_be_empty, true);
449 const_bool_nodef(may_contain_infinity, false);
450 const_bool_nodef(check_empty_result, false);
451 const_bool_nodef(check_inexact, false);
452 };
453
454 typedef Interval_Info_Bitset<unsigned int,
455 Rational_Real_Open_Interval_Info_Policy> Rational_Real_Open_Interval_Info;
456
457 typedef Interval<mpq_class, Rational_Real_Open_Interval_Info> rt_r_oc;
458
459 //! The incarnation of Box under test.
460 typedef Box<BOX_INSTANCE> TBox;
461
462 //! The incarnation of BD_Shape under test.
463 typedef BD_Shape<BD_SHAPE_INSTANCE> TBD_Shape;
464
465 //! The incarnation of Octagonal_Shape under test.
466 typedef Octagonal_Shape<OCTAGONAL_SHAPE_INSTANCE> TOctagonal_Shape;
467
468 // For floating point analysis.
469 #ifdef ANALYZER_FP_FORMAT
470 #ifdef ANALYZED_FP_FORMAT
471 //! The type of an interval with floating point boundaries.
472 typedef Interval<ANALYZER_FP_FORMAT,
473 Floating_Real_Open_Interval_Info> FP_Interval;
474
475 //! The type of an interval linear form.
476 typedef Linear_Form<FP_Interval> FP_Linear_Form;
477
478 //! The type of an interval abstract store.
479 typedef Box<FP_Interval> FP_Interval_Abstract_Store;
480
481 //! The type of a linear form abstract store.
482 typedef std::map<dimension_type, FP_Linear_Form>
483 FP_Linear_Form_Abstract_Store;
484
485 /*! \brief
486 The incarnation of BD_Shape under test for analyzing
487 floating point computations.
488 */
489 typedef BD_Shape<ANALYZER_FP_FORMAT> FP_BD_Shape;
490
491 /*! \brief
492 The incarnation of Octagonal_Shape under test for analyzing
493 floating point computations.
494 */
495 typedef Octagonal_Shape<ANALYZER_FP_FORMAT> FP_Octagonal_Shape;
496 #endif // ANALYZED_FP_FORMAT
497 #endif // ANALYZER_FP_FORMAT
498
499 template <typename Shape>
500 inline bool
has_exact_coefficient_type(const Shape &)501 has_exact_coefficient_type(const Shape&) {
502 return std::numeric_limits<typename Shape::coefficient_type>::is_exact;
503 }
504
505 template <typename Interval>
506 inline bool
has_exact_coefficient_type(const Box<Interval> &)507 has_exact_coefficient_type(const Box<Interval>&) {
508 return std::numeric_limits<typename Interval::boundary_type>::is_exact;
509 }
510
511 bool
512 check_distance(const Checked_Number<mpq_class, Extended_Number_Policy>& d,
513 const char* max_d_s, const char* d_name);
514
515 template <typename T>
516 bool
check_result_i(const BD_Shape<T> & computed_result,const BD_Shape<mpq_class> & known_result,const char * max_r_d_s,const char * max_e_d_s,const char * max_l_d_s)517 check_result_i(const BD_Shape<T>& computed_result,
518 const BD_Shape<mpq_class>& known_result,
519 const char* max_r_d_s,
520 const char* max_e_d_s,
521 const char* max_l_d_s) {
522 BD_Shape<mpq_class> q_computed_result(computed_result);
523 // Handle in a more efficient way the case where equality is expected.
524 if (max_r_d_s == 0 && max_e_d_s == 0 && max_l_d_s == 0) {
525 if (q_computed_result != known_result) {
526 using IO_Operators::operator<<;
527 nout << "Equality does not hold:"
528 << "\ncomputed result is\n"
529 << q_computed_result
530 << "\nknown result is\n"
531 << known_result
532 << std::endl;
533 return false;
534 }
535 else
536 return true;
537 }
538
539 if (!q_computed_result.contains(known_result)) {
540 using IO_Operators::operator<<;
541 nout << "Containment does not hold:"
542 << "\ncomputed result is\n"
543 << q_computed_result
544 << "\nknown result is\n"
545 << known_result
546 << std::endl;
547 return false;
548 }
549
550 Checked_Number<mpq_class, Extended_Number_Policy> r_d;
551 rectilinear_distance_assign(r_d, known_result, q_computed_result, ROUND_UP);
552 Checked_Number<mpq_class, Extended_Number_Policy> e_d;
553 euclidean_distance_assign(e_d, known_result, q_computed_result, ROUND_UP);
554 Checked_Number<mpq_class, Extended_Number_Policy> l_d;
555 l_infinity_distance_assign(l_d, known_result, q_computed_result, ROUND_UP);
556 bool ok_r = check_distance(r_d, max_r_d_s, "rectilinear");
557 bool ok_e = check_distance(e_d, max_e_d_s, "euclidean");
558 bool ok_l = check_distance(l_d, max_l_d_s, "l_infinity");
559 bool ok = ok_r && ok_e && ok_l;
560 if (!ok) {
561 using IO_Operators::operator<<;
562 nout << "Computed result is\n"
563 << q_computed_result
564 << "\nknown result is\n"
565 << known_result
566 << std::endl;
567 }
568 return ok;
569 }
570
571 template <typename T>
572 bool
check_result(const BD_Shape<T> & computed_result,const BD_Shape<mpq_class> & known_result,const char * max_r_d_s,const char * max_e_d_s,const char * max_l_d_s)573 check_result(const BD_Shape<T>& computed_result,
574 const BD_Shape<mpq_class>& known_result,
575 const char* max_r_d_s,
576 const char* max_e_d_s,
577 const char* max_l_d_s) {
578 return std::numeric_limits<T>::is_integer
579 ? check_result_i(computed_result, known_result,
580 "+inf", "+inf", "+inf")
581 : check_result_i(computed_result, known_result,
582 max_r_d_s, max_e_d_s, max_l_d_s);
583 }
584
585 template <typename T>
586 bool
check_result(const BD_Shape<T> & computed_result,const BD_Shape<T> & known_result)587 check_result(const BD_Shape<T>& computed_result,
588 const BD_Shape<T>& known_result) {
589 if (computed_result == known_result)
590 return true;
591 else {
592 using IO_Operators::operator<<;
593 nout << "Equality does not hold:"
594 << "\ncomputed result is\n"
595 << computed_result
596 << "\nknown result is\n"
597 << known_result
598 << std::endl;
599 return false;
600 }
601 }
602
603 template <typename T>
604 bool
check_result(const BD_Shape<T> & computed_result,const BD_Shape<mpq_class> & known_result)605 check_result(const BD_Shape<T>& computed_result,
606 const BD_Shape<mpq_class>& known_result) {
607 return std::numeric_limits<T>::is_integer
608 ? check_result_i(computed_result, known_result, "+inf", "+inf", "+inf")
609 : check_result_i(computed_result, known_result, 0, 0, 0);
610 }
611
612 bool
613 check_result(const BD_Shape<mpq_class>& computed_result,
614 const BD_Shape<mpq_class>& known_result);
615
616 template <typename T>
617 bool
check_result_i(const Octagonal_Shape<T> & computed_result,const Octagonal_Shape<mpq_class> & known_result,const char * max_r_d_s,const char * max_e_d_s,const char * max_l_d_s)618 check_result_i(const Octagonal_Shape<T>& computed_result,
619 const Octagonal_Shape<mpq_class>& known_result,
620 const char* max_r_d_s,
621 const char* max_e_d_s,
622 const char* max_l_d_s) {
623 Octagonal_Shape<mpq_class> q_computed_result(computed_result);
624 // Handle in a more efficient way the case where equality is expected.
625 if (max_r_d_s == 0 && max_e_d_s == 0 && max_l_d_s == 0) {
626 if (q_computed_result != known_result) {
627 using IO_Operators::operator<<;
628 nout << "Equality does not hold:"
629 << "\ncomputed result is\n"
630 << q_computed_result
631 << "\nknown result is\n"
632 << known_result
633 << std::endl;
634 return false;
635 }
636 else
637 return true;
638 }
639
640 if (!q_computed_result.contains(known_result)) {
641 using IO_Operators::operator<<;
642 nout << "Containment does not hold:"
643 << "\ncomputed result is\n"
644 << q_computed_result
645 << "\nknown result is\n"
646 << known_result
647 << std::endl;
648 return false;
649 }
650
651 Checked_Number<mpq_class, Extended_Number_Policy> r_d;
652 rectilinear_distance_assign(r_d, known_result, q_computed_result, ROUND_UP);
653 Checked_Number<mpq_class, Extended_Number_Policy> e_d;
654 euclidean_distance_assign(e_d, known_result, q_computed_result, ROUND_UP);
655 Checked_Number<mpq_class, Extended_Number_Policy> l_d;
656 l_infinity_distance_assign(l_d, known_result, q_computed_result, ROUND_UP);
657 bool ok_r = check_distance(r_d, max_r_d_s, "rectilinear");
658 bool ok_e = check_distance(e_d, max_e_d_s, "euclidean");
659 bool ok_l = check_distance(l_d, max_l_d_s, "l_infinity");
660 bool ok = ok_r && ok_e && ok_l;
661 if (!ok) {
662 using IO_Operators::operator<<;
663 nout << "Computed result is\n"
664 << q_computed_result
665 << "\nknown result is\n"
666 << known_result
667 << std::endl;
668 }
669 return ok;
670 }
671
672 template <typename T>
673 bool
check_result(const Octagonal_Shape<T> & computed_result,const Octagonal_Shape<mpq_class> & known_result,const char * max_r_d_s,const char * max_e_d_s,const char * max_l_d_s)674 check_result(const Octagonal_Shape<T>& computed_result,
675 const Octagonal_Shape<mpq_class>& known_result,
676 const char* max_r_d_s,
677 const char* max_e_d_s,
678 const char* max_l_d_s) {
679 return std::numeric_limits<T>::is_integer
680 ? check_result_i(computed_result, known_result,
681 "+inf", "+inf", "+inf")
682 : check_result_i(computed_result, known_result,
683 max_r_d_s, max_e_d_s, max_l_d_s);
684 }
685
686 template <>
687 inline bool
check_result(const Octagonal_Shape<mpq_class> & computed_result,const Octagonal_Shape<mpq_class> & known_result,const char *,const char *,const char *)688 check_result(const Octagonal_Shape<mpq_class>& computed_result,
689 const Octagonal_Shape<mpq_class>& known_result,
690 const char*,
691 const char*,
692 const char*) {
693 return check_result_i(computed_result, known_result,
694 0, 0, 0);
695 }
696
697 template <typename T>
698 bool
check_result(const Octagonal_Shape<T> & computed_result,const Octagonal_Shape<mpq_class> & known_result)699 check_result(const Octagonal_Shape<T>& computed_result,
700 const Octagonal_Shape<mpq_class>& known_result) {
701 return std::numeric_limits<T>::is_integer
702 ? check_result_i(computed_result, known_result, "+inf", "+inf", "+inf")
703 : check_result_i(computed_result, known_result, 0, 0, 0);
704 }
705
706
707 template <typename Interval>
708 bool
check_result_i(const Box<Interval> & computed_result,const Rational_Box & known_result,const char * max_r_d_s,const char * max_e_d_s,const char * max_l_d_s)709 check_result_i(const Box<Interval>& computed_result,
710 const Rational_Box& known_result,
711 const char* max_r_d_s,
712 const char* max_e_d_s,
713 const char* max_l_d_s) {
714 Rational_Box q_computed_result(computed_result);
715 // Handle in a more efficient way the case where equality is expected.
716 if (max_r_d_s == 0 && max_e_d_s == 0 && max_l_d_s == 0) {
717 if (q_computed_result != known_result) {
718 using IO_Operators::operator<<;
719 nout << "Equality does not hold:"
720 << "\ncomputed result is\n"
721 << q_computed_result
722 << "\nknown result is\n"
723 << known_result
724 << std::endl;
725 return false;
726 }
727 else
728 return true;
729 }
730
731 if (!q_computed_result.contains(known_result)) {
732 using IO_Operators::operator<<;
733 nout << "Containment does not hold:"
734 << "\ncomputed result is\n"
735 << q_computed_result
736 << "\nknown result is\n"
737 << known_result
738 << std::endl;
739 nout << "Individual dimensions where containment does not hold"
740 << "\n(Variable: computed-result known-result):\n";
741 for (dimension_type i = 0; i < computed_result.space_dimension(); ++i) {
742 if (!q_computed_result.get_interval(Variable(i))
743 .contains(known_result.get_interval(Variable(i)))) {
744 using IO_Operators::operator<<;
745 nout << Variable(i) << ": "
746 << q_computed_result.get_interval(Variable(i))
747 << ' '
748 << known_result.get_interval(Variable(i))
749 << std::endl;
750 }
751 }
752 return false;
753 }
754
755 Checked_Number<mpq_class, Extended_Number_Policy> r_d;
756 rectilinear_distance_assign(r_d, known_result, q_computed_result, ROUND_UP);
757 Checked_Number<mpq_class, Extended_Number_Policy> e_d;
758 euclidean_distance_assign(e_d, known_result, q_computed_result, ROUND_UP);
759 Checked_Number<mpq_class, Extended_Number_Policy> l_d;
760 l_infinity_distance_assign(l_d, known_result, q_computed_result, ROUND_UP);
761 bool ok_r = check_distance(r_d, max_r_d_s, "rectilinear");
762 bool ok_e = check_distance(e_d, max_e_d_s, "euclidean");
763 bool ok_l = check_distance(l_d, max_l_d_s, "l_infinity");
764 bool ok = ok_r && ok_e && ok_l;
765 if (!ok) {
766 using IO_Operators::operator<<;
767 nout << "Computed result is\n"
768 << q_computed_result
769 << "\nknown result is\n"
770 << known_result
771 << std::endl;
772 }
773 return ok;
774 }
775
776 template <typename Interval>
777 bool
check_result(const Box<Interval> & computed_result,const Rational_Box & known_result,const char * max_r_d_s,const char * max_e_d_s,const char * max_l_d_s)778 check_result(const Box<Interval>& computed_result,
779 const Rational_Box& known_result,
780 const char* max_r_d_s,
781 const char* max_e_d_s,
782 const char* max_l_d_s) {
783 return std::numeric_limits<typename Interval::boundary_type>::is_integer
784 ? check_result_i(computed_result, known_result,
785 "+inf", "+inf", "+inf")
786 : check_result_i(computed_result, known_result,
787 max_r_d_s, max_e_d_s, max_l_d_s);
788 }
789
790 template <typename Interval>
791 bool
check_result(const Box<Interval> & computed_result,const Box<Interval> & known_result)792 check_result(const Box<Interval>& computed_result,
793 const Box<Interval>& known_result) {
794 if (computed_result == known_result)
795 return true;
796 else {
797 using IO_Operators::operator<<;
798 nout << "Equality does not hold:"
799 << "\ncomputed result is\n"
800 << computed_result
801 << "\nknown result is\n"
802 << known_result
803 << std::endl;
804 return false;
805 }
806 }
807
808 template <typename Interval>
809 bool
check_result(const Box<Interval> & computed_result,const Rational_Box & known_result)810 check_result(const Box<Interval>& computed_result,
811 const Rational_Box& known_result) {
812 return std::numeric_limits<typename Interval::boundary_type>::is_integer
813 ? check_result_i(computed_result, known_result, "+inf", "+inf", "+inf")
814 : check_result_i(computed_result, known_result, 0, 0, 0);
815 }
816
817 bool
818 check_result(const Rational_Box& computed_result,
819 const Rational_Box& known_result);
820
821 bool
822 check_result(const Generator& computed_result,
823 const Generator& known_result,
824 const char* max_r_d_s,
825 const char* max_e_d_s,
826 const char* max_l_d_s);
827
828 bool
829 check_result(const Checked_Number<mpq_class, Extended_Number_Policy>& computed,
830 const Checked_Number<mpq_class, Extended_Number_Policy>& known,
831 const char* max_r_d_s);
832
833 class FCAIBVP;
834
835 bool
836 operator==(const FCAIBVP& x, const FCAIBVP& y);
837
838 bool
839 operator!=(const FCAIBVP& x, const FCAIBVP& y);
840
841 std::ostream&
842 operator<<(std::ostream& s, const FCAIBVP& x);
843
844 /*! \brief
845 A class for representing Finite Conjunctions of Attribute
846 Independent Boolean Variable Properties.
847 */
848 class FCAIBVP {
849 private:
850 typedef size_t dim_t;
851
852 typedef std::set<dim_t> Set;
853
854 Set set;
855
856 public:
857 FCAIBVP();
858
859 explicit FCAIBVP(const Variable x);
860
861 explicit FCAIBVP(const Variables_Set& y);
862
863 FCAIBVP(const FCAIBVP& y, unsigned offset);
864
865 memory_size_type total_memory_in_bytes() const;
866
867 memory_size_type external_memory_in_bytes() const;
868
869 bool is_top() const;
870
871 bool is_bottom() const;
872
873 bool definitely_entails(const FCAIBVP& y) const;
874
875 void upper_bound_assign(const FCAIBVP& y);
876
877 void difference_assign(const FCAIBVP& y);
878
879 void meet_assign(const FCAIBVP& y);
880
881 void weakening_assign(const FCAIBVP& y);
882
883 static bool has_nontrivial_weakening();
884
885 bool OK() const;
886
887 friend std::ostream&
888 Parma_Polyhedra_Library::Test::operator<<(std::ostream& s,
889 const FCAIBVP& x);
890 };
891
892 inline
FCAIBVP()893 FCAIBVP::FCAIBVP()
894 : set() {
895 }
896
897 inline
FCAIBVP(const Variable x)898 FCAIBVP::FCAIBVP(const Variable x)
899 : set() {
900 set.insert(x.id());
901 }
902
903 inline
FCAIBVP(const Variables_Set & y)904 FCAIBVP::FCAIBVP(const Variables_Set& y)
905 : set() {
906 for (Variables_Set::const_iterator i = y.begin(),
907 y_end = y.end(); i != y_end; ++i)
908 set.insert(*i);
909 }
910
911 inline
FCAIBVP(const FCAIBVP & y,unsigned offset)912 FCAIBVP::FCAIBVP(const FCAIBVP& y, unsigned offset)
913 : set() {
914 for (Set::const_iterator i = y.set.begin(),
915 y_set_end = y.set.end(); i != y_set_end; ++i)
916 set.insert(*i + offset);
917 }
918
919 inline memory_size_type
total_memory_in_bytes() const920 FCAIBVP::total_memory_in_bytes() const {
921 return 1;
922 }
923
924 inline bool
is_top() const925 FCAIBVP::is_top() const {
926 return set.empty();
927 }
928
929 inline bool
is_bottom() const930 FCAIBVP::is_bottom() const {
931 return false;
932 }
933
934 inline bool
definitely_entails(const FCAIBVP & y) const935 FCAIBVP::definitely_entails(const FCAIBVP& y) const{
936 const FCAIBVP& x = *this;
937 return std::includes(x.set.begin(), x.set.end(),
938 y.set.begin(), y.set.end());
939 }
940
941 inline void
upper_bound_assign(const FCAIBVP & y)942 FCAIBVP::upper_bound_assign(const FCAIBVP& y) {
943 FCAIBVP& x = *this;
944 FCAIBVP z;
945 std::set_intersection(x.set.begin(), x.set.end(),
946 y.set.begin(), y.set.end(),
947 std::inserter(z.set, z.set.begin()));
948 using std::swap;
949 swap(x, z);
950 }
951
952 inline void
difference_assign(const FCAIBVP & y)953 FCAIBVP::difference_assign(const FCAIBVP& y) {
954 FCAIBVP& x = *this;
955 FCAIBVP z;
956 std::set_difference(x.set.begin(), x.set.end(),
957 y.set.begin(), y.set.end(),
958 std::inserter(z.set, z.set.begin()));
959 using std::swap;
960 swap(x, z);
961 }
962
963 inline void
meet_assign(const FCAIBVP & y)964 FCAIBVP::meet_assign(const FCAIBVP& y) {
965 set.insert(y.set.begin(), y.set.end());
966 }
967
968 inline void
weakening_assign(const FCAIBVP & y)969 FCAIBVP::weakening_assign(const FCAIBVP& y) {
970 difference_assign(y);
971 }
972
973 inline bool
has_nontrivial_weakening()974 FCAIBVP::has_nontrivial_weakening() {
975 return true;
976 }
977
978 inline bool
OK() const979 FCAIBVP::OK() const {
980 return true;
981 }
982
983 inline bool
operator ==(const FCAIBVP & x,const FCAIBVP & y)984 operator==(const FCAIBVP& x, const FCAIBVP& y) {
985 return x.definitely_entails(y) && y.definitely_entails(x);
986 }
987
988 inline bool
operator !=(const FCAIBVP & x,const FCAIBVP & y)989 operator!=(const FCAIBVP& x, const FCAIBVP& y) {
990 return !(x == y);
991 }
992
993 void
994 print_constraint(const Constraint& c,
995 const std::string& intro = "",
996 std::ostream& s = nout);
997
998 void
999 print_constraints(const Constraint_System& cs,
1000 const std::string& intro = "",
1001 std::ostream& s = nout);
1002
1003 void
1004 print_constraints(const Polyhedron& ph,
1005 const std::string& intro = "",
1006 std::ostream& s = nout);
1007
1008 #if 0
1009 void
1010 print_constraints(const Affine_Space& affs,
1011 const std::string& intro = "",
1012 std::ostream& s = nout);
1013 #endif
1014
1015 template <typename Interval>
1016 void
print_constraints(const Box<Interval> & box,const std::string & intro="",std::ostream & s=nout)1017 print_constraints(const Box<Interval>& box,
1018 const std::string& intro = "",
1019 std::ostream& s = nout) {
1020 if (!intro.empty())
1021 s << intro << std::endl;
1022 using IO_Operators::operator<<;
1023 s << box << std::endl;
1024 }
1025
1026 template <typename T>
1027 void
print_constraints(const BD_Shape<T> & bd,const std::string & intro="",std::ostream & s=nout)1028 print_constraints(const BD_Shape<T>& bd,
1029 const std::string& intro = "",
1030 std::ostream& s = nout) {
1031 if (!intro.empty())
1032 s << intro << std::endl;
1033 using IO_Operators::operator<<;
1034 s << bd << std::endl;
1035 }
1036
1037 template <typename T>
1038 void
print_constraints(const Octagonal_Shape<T> & oc,const std::string & intro="",std::ostream & s=nout)1039 print_constraints(const Octagonal_Shape<T>& oc,
1040 const std::string& intro = "",
1041 std::ostream& s = nout) {
1042 if (!intro.empty())
1043 s << intro << std::endl;
1044 using IO_Operators::operator<<;
1045 s << oc << std::endl;
1046 }
1047
1048 template <typename PH>
1049 void
print_constraints(const Pointset_Powerset<PH> & pps,const std::string & intro="",std::ostream & s=nout)1050 print_constraints(const Pointset_Powerset<PH>& pps,
1051 const std::string& intro = "",
1052 std::ostream& s = nout) {
1053 if (!intro.empty())
1054 s << intro << std::endl;
1055 using IO_Operators::operator<<;
1056 s << pps << std::endl;
1057 }
1058
1059 template <typename PH>
1060 void
print_congruences(const Pointset_Powerset<PH> & pps,const std::string & intro="",std::ostream & s=nout)1061 print_congruences(const Pointset_Powerset<PH>& pps,
1062 const std::string& intro = "",
1063 std::ostream& s = nout) {
1064 if (!intro.empty())
1065 s << intro << std::endl;
1066 using IO_Operators::operator<<;
1067 s << pps << std::endl;
1068 }
1069
1070 /*
1071 template <typename PH>
1072 void
1073 print_constraints(const Pointset_Ask_Tell<PH>& pat,
1074 const std::string& intro = "",
1075 std::ostream& s = nout) {
1076 if (!intro.empty())
1077 s << intro << std::endl;
1078 using IO_Operators::operator<<;
1079 s << pat << std::endl;
1080 }
1081 */
1082
1083 void
1084 print_congruence(const Congruence& c,
1085 const std::string& intro = "",
1086 std::ostream& s = nout);
1087
1088 void
1089 print_congruences(const Congruence_System& cgs,
1090 const std::string& intro = "",
1091 std::ostream& s = nout);
1092
1093 void
1094 print_congruences(const Grid& gr,
1095 const std::string& intro = "",
1096 std::ostream& s = nout);
1097
1098 void
1099 print_generator(const Generator& g,
1100 const std::string& intro = "",
1101 std::ostream& s = nout);
1102
1103 void
1104 print_generator(const Grid_Generator& g,
1105 const std::string& intro = "",
1106 std::ostream& s = nout);
1107
1108 void
1109 print_generators(const Generator_System& gs,
1110 const std::string& intro = "",
1111 std::ostream& s = nout);
1112
1113 void
1114 print_generators(const Grid_Generator_System& gs,
1115 const std::string& intro = "",
1116 std::ostream& s = nout);
1117
1118 void
1119 print_generators(const Polyhedron& ph,
1120 const std::string& intro = "",
1121 std::ostream& s = nout);
1122
1123 void
1124 print_generators(const Grid& gr,
1125 const std::string& intro = "",
1126 std::ostream& s = nout);
1127
1128 template <typename D1, typename D2, typename R>
1129 void
print_constraints(const Partially_Reduced_Product<D1,D2,R> & pd,const std::string & intro="",std::ostream & s=nout)1130 print_constraints(const Partially_Reduced_Product<D1, D2, R>& pd,
1131 const std::string& intro = "",
1132 std::ostream& s = nout) {
1133 print_constraints(pd.constraints(), intro, s);
1134 }
1135
1136 template <typename D1, typename D2, typename R>
1137 void
print_congruences(const Partially_Reduced_Product<D1,D2,R> & pd,const std::string & intro="",std::ostream & s=nout)1138 print_congruences(const Partially_Reduced_Product<D1, D2, R>& pd,
1139 const std::string& intro = "",
1140 std::ostream& s = nout) {
1141 print_congruences(pd.congruences(), intro, s);
1142 }
1143
1144 void
1145 print_function(const Parma_Polyhedra_Library::Partial_Function& function,
1146 const std::string& intro = "",
1147 std::ostream& s = nout);
1148
1149 } // namespace Test
1150
1151 } // namespace Parma_Polyhedra_Library
1152
1153 // These using directive and declaration are just to avoid the
1154 // corresponding namespace qualifications in all the tests.
1155 using namespace Parma_Polyhedra_Library;
1156 using namespace Parma_Polyhedra_Library::Test;
1157 using std::endl;
1158
1159 #endif // !defined(PPL_ppl_test_hh)
1160