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