00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024 #include <ppl-config.h>
00025
00026 #include "Polyhedron.defs.hh"
00027 #include "BHRZ03_Certificate.defs.hh"
00028 #include "Rational_Box.hh"
00029 #include "Scalar_Products.defs.hh"
00030 #include <cassert>
00031 #include <iostream>
00032 #include <stdexcept>
00033 #include <deque>
00034
00035 namespace PPL = Parma_Polyhedra_Library;
00036
00037 void
00038 PPL::Polyhedron
00039 ::select_CH78_constraints(const Polyhedron& y,
00040 Constraint_System& cs_selection) const {
00041
00042 assert(topology() == y.topology()
00043 && topology() == cs_selection.topology()
00044 && space_dim == y.space_dim);
00045 assert(!marked_empty()
00046 && !has_pending_constraints()
00047 && generators_are_up_to_date());
00048 assert(!y.marked_empty()
00049 && !y.has_something_pending()
00050 && y.constraints_are_minimized());
00051
00052
00053
00054
00055
00056
00057 for (dimension_type i = 0, end = y.con_sys.num_rows(); i < end; ++i) {
00058 const Constraint& c = y.con_sys[i];
00059 if (gen_sys.satisfied_by_all_generators(c))
00060 cs_selection.insert(c);
00061 }
00062 }
00063
00064 void
00065 PPL::Polyhedron
00066 ::select_H79_constraints(const Polyhedron& y,
00067 Constraint_System& cs_selected,
00068 Constraint_System& cs_not_selected) const {
00069
00070
00071 assert(topology() == y.topology()
00072 && topology() == cs_selected.topology()
00073 && topology() == cs_not_selected.topology());
00074 assert(space_dim == y.space_dim);
00075 assert(!marked_empty()
00076 && !has_pending_generators()
00077 && constraints_are_up_to_date());
00078 assert(!y.marked_empty()
00079 && !y.has_something_pending()
00080 && y.constraints_are_minimized()
00081 && y.generators_are_up_to_date());
00082
00083
00084 if (!y.is_necessarily_closed()) {
00085
00086 y.strongly_minimize_constraints();
00087
00088 y.update_generators();
00089 }
00090
00091
00092 if (!y.sat_g_is_up_to_date())
00093 y.update_sat_g();
00094 Bit_Matrix tmp_sat_g = y.sat_g;
00095
00096
00097
00098
00099 const Constraint_System& y_cs = y.con_sys;
00100 dimension_type num_rows = y_cs.num_rows();
00101 for (dimension_type i = 0; i < num_rows; ++i)
00102 if (y_cs[i].is_tautological()) {
00103 --num_rows;
00104 std::swap(tmp_sat_g[i], tmp_sat_g[num_rows]);
00105 }
00106 tmp_sat_g.rows_erase_to_end(num_rows);
00107 tmp_sat_g.sort_rows();
00108
00109
00110
00111
00112
00113
00114
00115
00116
00117
00118
00119
00120
00121
00122
00123
00124
00125
00126
00127 Bit_Row buffer;
00128
00129
00130 for (dimension_type i = 0, end = con_sys.num_rows(); i < end; ++i) {
00131 const Constraint& ci = con_sys[i];
00132
00133
00134
00135 buffer.clear();
00136 for (dimension_type j = y.gen_sys.num_rows(); j-- > 0; ) {
00137 const int sp_sgn = Scalar_Products::sign(ci, y.gen_sys[j]);
00138
00139 assert(sp_sgn >= 0
00140 || (!is_necessarily_closed()
00141 && ci.is_strict_inequality()
00142 && y.gen_sys[j].is_point()));
00143 if (sp_sgn > 0)
00144 buffer.set(j);
00145 }
00146
00147
00148 if (tmp_sat_g.sorted_contains(buffer))
00149 cs_selected.insert(ci);
00150 else
00151 cs_not_selected.insert(ci);
00152 }
00153 }
00154
00155 void
00156 PPL::Polyhedron::H79_widening_assign(const Polyhedron& y, unsigned* tp) {
00157 Polyhedron& x = *this;
00158
00159 const Topology topol = x.topology();
00160 if (topol != y.topology())
00161 throw_topology_incompatible("H79_widening_assign(y)", "y", y);
00162
00163 if (x.space_dim != y.space_dim)
00164 throw_dimension_incompatible("H79_widening_assign(y)", "y", y);
00165
00166 #ifndef NDEBUG
00167 {
00168
00169 const Polyhedron x_copy = x;
00170 const Polyhedron y_copy = y;
00171 assert(x_copy.contains(y_copy));
00172 }
00173 #endif
00174
00175
00176
00177 if (x.space_dim == 0 || x.marked_empty() || y.marked_empty())
00178 return;
00179
00180
00181
00182 if (y.is_necessarily_closed()) {
00183 if (!y.minimize())
00184
00185 return;
00186 }
00187 else {
00188
00189
00190
00191
00192
00193
00194
00195 Polyhedron& yy = const_cast<Polyhedron&>(y);
00196 yy.intersection_assign(x);
00197 if (yy.is_empty())
00198
00199 return;
00200 }
00201
00202
00203
00204
00205
00206 if (x.has_pending_generators() || !x.constraints_are_up_to_date()) {
00207 Constraint_System CH78_cs(topol);
00208 x.select_CH78_constraints(y, CH78_cs);
00209
00210 if (CH78_cs.num_rows() == y.con_sys.num_rows()) {
00211
00212 x = y;
00213 return;
00214 }
00215
00216
00217
00218 else if (CH78_cs.num_equalities() == y.con_sys.num_equalities()) {
00219
00220 Polyhedron CH78(topol, x.space_dim, UNIVERSE);
00221 CH78.add_recycled_constraints(CH78_cs);
00222
00223
00224
00225 if (tp != 0 && *tp > 0) {
00226
00227
00228 if (!x.contains(CH78))
00229 --(*tp);
00230 }
00231 else
00232
00233 std::swap(x, CH78);
00234 assert(x.OK(true));
00235 return;
00236 }
00237 }
00238
00239
00240
00241
00242
00243
00244
00245
00246
00247
00248 if (has_pending_generators())
00249 process_pending_generators();
00250 else if (!x.constraints_are_up_to_date())
00251 x.update_constraints();
00252
00253
00254
00255 Constraint_System H79_cs(topol);
00256 Constraint_System x_minus_H79_cs(topol);
00257 x.select_H79_constraints(y, H79_cs, x_minus_H79_cs);
00258
00259 if (x_minus_H79_cs.has_no_rows())
00260
00261
00262 return;
00263 else {
00264
00265
00266
00267
00268 Polyhedron H79(topol, x.space_dim, UNIVERSE);
00269 H79.add_recycled_constraints(H79_cs);
00270
00271
00272
00273 if (tp != 0 && *tp > 0) {
00274
00275
00276 if (!x.contains(H79))
00277 --(*tp);
00278 }
00279 else
00280
00281 std::swap(x, H79);
00282 assert(x.OK(true));
00283 }
00284 }
00285
00286 void
00287 PPL::Polyhedron::limited_H79_extrapolation_assign(const Polyhedron& y,
00288 const Constraint_System& cs,
00289 unsigned* tp) {
00290 Polyhedron& x = *this;
00291
00292 const dimension_type cs_num_rows = cs.num_rows();
00293
00294 if (cs_num_rows == 0) {
00295 x.H79_widening_assign(y, tp);
00296 return;
00297 }
00298
00299
00300 if (x.is_necessarily_closed()) {
00301 if (!y.is_necessarily_closed())
00302 throw_topology_incompatible("limited_H79_extrapolation_assign(y, cs)",
00303 "y", y);
00304 if (cs.has_strict_inequalities())
00305 throw_topology_incompatible("limited_H79_extrapolation_assign(y, cs)",
00306 "cs", cs);
00307 }
00308 else if (y.is_necessarily_closed())
00309 throw_topology_incompatible("limited_H79_extrapolation_assign(y, cs)",
00310 "y", y);
00311
00312
00313 if (x.space_dim != y.space_dim)
00314 throw_dimension_incompatible("limited_H79_extrapolation_assign(y, cs)",
00315 "y", y);
00316
00317 const dimension_type cs_space_dim = cs.space_dimension();
00318 if (x.space_dim < cs_space_dim)
00319 throw_dimension_incompatible("limited_H79_extrapolation_assign(y, cs)",
00320 "cs", cs);
00321
00322 #ifndef NDEBUG
00323 {
00324
00325 const Polyhedron x_copy = x;
00326 const Polyhedron y_copy = y;
00327 assert(x_copy.contains(y_copy));
00328 }
00329 #endif
00330
00331 if (y.marked_empty())
00332 return;
00333 if (x.marked_empty())
00334 return;
00335
00336
00337
00338
00339 if (x.space_dim == 0)
00340 return;
00341
00342 if (!y.minimize())
00343
00344 return;
00345
00346
00347
00348
00349 if ((x.has_pending_constraints() && !x.process_pending_constraints())
00350 || (!x.generators_are_up_to_date() && !x.update_generators()))
00351
00352 return;
00353
00354 Constraint_System new_cs;
00355
00356
00357 const Generator_System& x_gen_sys = x.gen_sys;
00358
00359
00360 for (dimension_type i = 0; i < cs_num_rows; ++i) {
00361 const Constraint& c = cs[i];
00362 if (x_gen_sys.satisfied_by_all_generators(c))
00363 new_cs.insert(c);
00364 }
00365 x.H79_widening_assign(y, tp);
00366 x.add_recycled_constraints(new_cs);
00367 assert(OK());
00368 }
00369
00370 void
00371 PPL::Polyhedron::bounded_H79_extrapolation_assign(const Polyhedron& y,
00372 const Constraint_System& cs,
00373 unsigned* tp) {
00374 Rational_Box x_box(*this, ANY_COMPLEXITY);
00375 Rational_Box y_box(y, ANY_COMPLEXITY);
00376 x_box.CC76_widening_assign(y_box);
00377 limited_H79_extrapolation_assign(y, cs, tp);
00378 Constraint_System x_box_cs = x_box.constraints();
00379 add_recycled_constraints(x_box_cs);
00380 }
00381
00382 bool
00383 PPL::Polyhedron
00384 ::BHRZ03_combining_constraints(const Polyhedron& y,
00385 const BHRZ03_Certificate& y_cert,
00386 const Polyhedron& H79,
00387 const Constraint_System& x_minus_H79_cs) {
00388 Polyhedron& x = *this;
00389
00390 assert(x.topology() == y.topology()
00391 && x.topology() == H79.topology()
00392 && x.topology() == x_minus_H79_cs.topology());
00393 assert(x.space_dim == y.space_dim
00394 && x.space_dim == H79.space_dim
00395 && x.space_dim == x_minus_H79_cs.space_dimension());
00396 assert(!x.marked_empty() && !x.has_something_pending()
00397 && x.constraints_are_minimized() && x.generators_are_minimized());
00398 assert(!y.marked_empty() && !y.has_something_pending()
00399 && y.constraints_are_minimized() && y.generators_are_minimized());
00400 assert(!H79.marked_empty() && !H79.has_something_pending()
00401 && H79.constraints_are_minimized() && H79.generators_are_minimized());
00402
00403
00404
00405
00406
00407
00408
00409
00410 const dimension_type x_minus_H79_cs_num_rows = x_minus_H79_cs.num_rows();
00411 if (x_minus_H79_cs_num_rows <= 1)
00412 return false;
00413
00414 const Topology topol = x.topology();
00415 Constraint_System combining_cs(topol);
00416 Constraint_System new_cs(topol);
00417
00418
00419
00420 const bool closed = x.is_necessarily_closed();
00421 for (dimension_type i = y.gen_sys.num_rows(); i-- > 0; ) {
00422 const Generator& g = y.gen_sys[i];
00423 if ((g.is_point() && closed) || (g.is_closure_point() && !closed)) {
00424
00425
00426
00427 bool lies_on_the_boundary_of_H79 = false;
00428 const Constraint_System& H79_cs = H79.con_sys;
00429 for (dimension_type j = H79_cs.num_rows(); j-- > 0; ) {
00430 const Constraint& c = H79_cs[j];
00431 if (c.is_inequality() && Scalar_Products::sign(c, g) == 0) {
00432 lies_on_the_boundary_of_H79 = true;
00433 break;
00434 }
00435 }
00436 if (lies_on_the_boundary_of_H79)
00437 continue;
00438
00439
00440
00441 combining_cs.clear();
00442 for (dimension_type j = x_minus_H79_cs_num_rows; j-- > 0; ) {
00443 const Constraint& c = x_minus_H79_cs[j];
00444 if (Scalar_Products::sign(c, g) == 0)
00445 combining_cs.insert(c);
00446 }
00447
00448 const dimension_type combining_cs_num_rows = combining_cs.num_rows();
00449 if (combining_cs_num_rows > 0) {
00450 if (combining_cs_num_rows == 1)
00451
00452 new_cs.insert(combining_cs[0]);
00453 else {
00454 Linear_Expression e(0);
00455 bool strict_inequality = false;
00456 for (dimension_type h = combining_cs_num_rows; h-- > 0; ) {
00457 if (combining_cs[h].is_strict_inequality())
00458 strict_inequality = true;
00459 e += Linear_Expression(combining_cs[h]);
00460 }
00461
00462 if (!e.all_homogeneous_terms_are_zero()) {
00463 if (strict_inequality)
00464 new_cs.insert(e > 0);
00465 else
00466 new_cs.insert(e >= 0);
00467 }
00468 }
00469 }
00470 }
00471 }
00472
00473
00474
00475 bool improves_upon_H79 = false;
00476 const Poly_Con_Relation si = Poly_Con_Relation::strictly_intersects();
00477 for (dimension_type i = new_cs.num_rows(); i-- > 0; )
00478 if (H79.relation_with(new_cs[i]) == si) {
00479 improves_upon_H79 = true;
00480 break;
00481 }
00482 if (!improves_upon_H79)
00483 return false;
00484
00485
00486
00487 Polyhedron result = H79;
00488 result.add_recycled_constraints(new_cs);
00489
00490 result.minimize();
00491
00492
00493
00494 if (y_cert.is_stabilizing(result) && !result.contains(H79)) {
00495
00496 std::swap(x, result);
00497 assert(x.OK(true));
00498 return true;
00499 }
00500 else
00501
00502 return false;
00503 }
00504
00505 bool
00506 PPL::Polyhedron::BHRZ03_evolving_points(const Polyhedron& y,
00507 const BHRZ03_Certificate& y_cert,
00508 const Polyhedron& H79) {
00509 Polyhedron& x = *this;
00510
00511 assert(x.topology() == y.topology()
00512 && x.topology() == H79.topology());
00513 assert(x.space_dim == y.space_dim
00514 && x.space_dim == H79.space_dim);
00515 assert(!x.marked_empty() && !x.has_something_pending()
00516 && x.constraints_are_minimized() && x.generators_are_minimized());
00517 assert(!y.marked_empty() && !y.has_something_pending()
00518 && y.constraints_are_minimized() && y.generators_are_minimized());
00519 assert(!H79.marked_empty() && !H79.has_something_pending()
00520 && H79.constraints_are_minimized() && H79.generators_are_minimized());
00521
00522
00523
00524
00525
00526 Generator_System candidate_rays;
00527
00528 const dimension_type x_gen_sys_num_rows = x.gen_sys.num_rows();
00529 const dimension_type y_gen_sys_num_rows = y.gen_sys.num_rows();
00530 const bool closed = x.is_necessarily_closed();
00531 for (dimension_type i = x_gen_sys_num_rows; i-- > 0; ) {
00532 Generator& g1 = x.gen_sys[i];
00533
00534
00535
00536
00537 if (((g1.is_point() && closed) || (g1.is_closure_point() && !closed))
00538 && y.relation_with(g1) == Poly_Gen_Relation::nothing()) {
00539
00540
00541
00542 for (dimension_type j = y_gen_sys_num_rows; j-- > 0; ) {
00543 const Generator& g2 = y.gen_sys[j];
00544 if ((g2.is_point() && closed)
00545 || (g2.is_closure_point() && !closed)) {
00546 assert(compare(g1, g2) != 0);
00547 Generator ray_from_g2_to_g1 = g1;
00548 ray_from_g2_to_g1.linear_combine(g2, 0);
00549 candidate_rays.insert(ray_from_g2_to_g1);
00550 }
00551 }
00552 }
00553 }
00554
00555
00556 Polyhedron result = x;
00557 result.add_recycled_generators(candidate_rays);
00558 result.intersection_assign(H79);
00559
00560 result.minimize();
00561
00562
00563
00564 if (y_cert.is_stabilizing(result) && !result.contains(H79)) {
00565
00566 std::swap(x, result);
00567 assert(x.OK(true));
00568 return true;
00569 }
00570 else
00571
00572 return false;
00573 }
00574
00575 bool
00576 PPL::Polyhedron::BHRZ03_evolving_rays(const Polyhedron& y,
00577 const BHRZ03_Certificate& y_cert,
00578 const Polyhedron& H79) {
00579 Polyhedron& x = *this;
00580
00581 assert(x.topology() == y.topology()
00582 && x.topology() == H79.topology());
00583 assert(x.space_dim == y.space_dim
00584 && x.space_dim == H79.space_dim);
00585 assert(!x.marked_empty() && !x.has_something_pending()
00586 && x.constraints_are_minimized() && x.generators_are_minimized());
00587 assert(!y.marked_empty() && !y.has_something_pending()
00588 && y.constraints_are_minimized() && y.generators_are_minimized());
00589 assert(!H79.marked_empty() && !H79.has_something_pending()
00590 && H79.constraints_are_minimized() && H79.generators_are_minimized());
00591
00592 const dimension_type x_gen_sys_num_rows = x.gen_sys.num_rows();
00593 const dimension_type y_gen_sys_num_rows = y.gen_sys.num_rows();
00594
00595
00596 Generator_System candidate_rays;
00597 TEMP_INTEGER(tmp);
00598 for (dimension_type i = x_gen_sys_num_rows; i-- > 0; ) {
00599 const Generator& x_g = x.gen_sys[i];
00600
00601 if (x_g.is_ray() && y.relation_with(x_g) == Poly_Gen_Relation::nothing()) {
00602 for (dimension_type j = y_gen_sys_num_rows; j-- > 0; ) {
00603 const Generator& y_g = y.gen_sys[j];
00604 if (y_g.is_ray()) {
00605 Generator new_ray(x_g);
00606
00607
00608 std::deque<bool> considered(x.space_dim + 1);
00609 for (dimension_type k = 1; k < x.space_dim; ++k)
00610 if (!considered[k])
00611 for (dimension_type h = k + 1; h <= x.space_dim; ++h)
00612 if (!considered[h]) {
00613 tmp = x_g[k] * y_g[h];
00614
00615
00616 sub_mul_assign(tmp, x_g[h], y_g[k]);
00617 const int clockwise
00618 = sgn(tmp);
00619 const int first_or_third_quadrant
00620 = sgn(x_g[k]) * sgn(x_g[h]);
00621 switch (clockwise * first_or_third_quadrant) {
00622 case -1:
00623 new_ray[k] = 0;
00624 considered[k] = true;
00625 break;
00626 case 1:
00627 new_ray[h] = 0;
00628 considered[h] = true;
00629 break;
00630 default:
00631 break;
00632 }
00633 }
00634 new_ray.normalize();
00635 candidate_rays.insert(new_ray);
00636 }
00637 }
00638 }
00639 }
00640
00641
00642 if (candidate_rays.has_no_rows())
00643 return false;
00644
00645
00646 Polyhedron result = x;
00647 result.add_recycled_generators(candidate_rays);
00648 result.intersection_assign(H79);
00649
00650 result.minimize();
00651
00652
00653 if (y_cert.is_stabilizing(result) && !result.contains(H79)) {
00654
00655 std::swap(x, result);
00656 assert(x.OK(true));
00657 return true;
00658 }
00659 else
00660
00661 return false;
00662 }
00663
00664 void
00665 PPL::Polyhedron::BHRZ03_widening_assign(const Polyhedron& y, unsigned* tp) {
00666 Polyhedron& x = *this;
00667
00668 if (x.topology() != y.topology())
00669 throw_topology_incompatible("BHRZ03_widening_assign(y)", "y", y);
00670
00671 if (x.space_dim != y.space_dim)
00672 throw_dimension_incompatible("BHRZ03_widening_assign(y)", "y", y);
00673
00674 #ifndef NDEBUG
00675 {
00676
00677 const Polyhedron x_copy = x;
00678 const Polyhedron y_copy = y;
00679 assert(x_copy.contains(y_copy));
00680 }
00681 #endif
00682
00683
00684
00685 if (x.space_dim == 0 || x.marked_empty() || y.marked_empty())
00686 return;
00687
00688
00689 if (!y.minimize())
00690
00691 return;
00692
00693 x.minimize();
00694
00695
00696 BHRZ03_Certificate y_cert(y);
00697
00698
00699
00700
00701 if (y_cert.is_stabilizing(x) || y.contains(x)) {
00702 assert(OK());
00703 return;
00704 }
00705
00706
00707
00708
00709 if (tp != 0 && *tp > 0) {
00710 --(*tp);
00711 assert(OK());
00712 return;
00713 }
00714
00715
00716
00717
00718 const Topology topol = x.topology();
00719 Constraint_System H79_cs(topol);
00720 Constraint_System x_minus_H79_cs(topol);
00721 x.select_H79_constraints(y, H79_cs, x_minus_H79_cs);
00722
00723
00724
00725 assert(!x_minus_H79_cs.has_no_rows());
00726
00727
00728 Polyhedron H79(topol, x.space_dim, UNIVERSE);
00729 H79.add_recycled_constraints(H79_cs);
00730
00731 H79.minimize();
00732
00733
00734
00735 if (x.BHRZ03_combining_constraints(y, y_cert, H79, x_minus_H79_cs))
00736 return;
00737
00738 assert(H79.OK() && x.OK() && y.OK());
00739
00740 if (x.BHRZ03_evolving_points(y, y_cert, H79))
00741 return;
00742
00743 assert(H79.OK() && x.OK() && y.OK());
00744
00745 if (x.BHRZ03_evolving_rays(y, y_cert, H79))
00746 return;
00747
00748 assert(H79.OK() && x.OK() && y.OK());
00749
00750
00751 std::swap(x, H79);
00752 assert(x.OK(true));
00753
00754 #ifndef NDEBUG
00755
00756 assert(y_cert.is_stabilizing(x));
00757 #endif
00758 }
00759
00760 void
00761 PPL::Polyhedron
00762 ::limited_BHRZ03_extrapolation_assign(const Polyhedron& y,
00763 const Constraint_System& cs,
00764 unsigned* tp) {
00765 Polyhedron& x = *this;
00766 const dimension_type cs_num_rows = cs.num_rows();
00767
00768 if (cs_num_rows == 0) {
00769 x.BHRZ03_widening_assign(y, tp);
00770 return;
00771 }
00772
00773
00774 if (x.is_necessarily_closed()) {
00775 if (!y.is_necessarily_closed())
00776 throw_topology_incompatible("limited_BHRZ03_extrapolation_assign(y, cs)",
00777 "y", y);
00778 if (cs.has_strict_inequalities())
00779 throw_topology_incompatible("limited_BHRZ03_extrapolation_assign(y, cs)",
00780 "cs", cs);
00781 }
00782 else if (y.is_necessarily_closed())
00783 throw_topology_incompatible("limited_BHRZ03_extrapolation_assign(y, cs)",
00784 "y", y);
00785
00786
00787 if (x.space_dim != y.space_dim)
00788 throw_dimension_incompatible("limited_BHRZ03_extrapolation_assign(y, cs)",
00789 "y", y);
00790
00791 const dimension_type cs_space_dim = cs.space_dimension();
00792 if (x.space_dim < cs_space_dim)
00793 throw_dimension_incompatible("limited_BHRZ03_extrapolation_assign(y, cs)",
00794 "cs", cs);
00795
00796 #ifndef NDEBUG
00797 {
00798
00799 const Polyhedron x_copy = x;
00800 const Polyhedron y_copy = y;
00801 assert(x_copy.contains(y_copy));
00802 }
00803 #endif
00804
00805 if (y.marked_empty())
00806 return;
00807 if (x.marked_empty())
00808 return;
00809
00810
00811
00812
00813 if (x.space_dim == 0)
00814 return;
00815
00816 if (!y.minimize())
00817
00818 return;
00819
00820
00821
00822
00823 if ((x.has_pending_constraints() && !x.process_pending_constraints())
00824 || (!x.generators_are_up_to_date() && !x.update_generators()))
00825
00826 return;
00827
00828 Constraint_System new_cs;
00829
00830
00831 const Generator_System& x_gen_sys = x.gen_sys;
00832
00833
00834 for (dimension_type i = 0; i < cs_num_rows; ++i) {
00835 const Constraint& c = cs[i];
00836 if (x_gen_sys.satisfied_by_all_generators(c))
00837 new_cs.insert(c);
00838 }
00839 x.BHRZ03_widening_assign(y, tp);
00840 x.add_recycled_constraints(new_cs);
00841 assert(OK());
00842 }
00843
00844 void
00845 PPL::Polyhedron
00846 ::bounded_BHRZ03_extrapolation_assign(const Polyhedron& y,
00847 const Constraint_System& cs,
00848 unsigned* tp) {
00849 Rational_Box x_box(*this, ANY_COMPLEXITY);
00850 Rational_Box y_box(y, ANY_COMPLEXITY);
00851 x_box.CC76_widening_assign(y_box);
00852 limited_BHRZ03_extrapolation_assign(y, cs, tp);
00853 Constraint_System x_box_cs = x_box.constraints();
00854 add_recycled_constraints(x_box_cs);
00855 }