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 #include <cassert>
00028
00029 #define BE_LAZY 1
00030
00031 namespace PPL = Parma_Polyhedra_Library;
00032
00033 void
00034 PPL::Polyhedron::add_space_dimensions(Linear_System& sys1,
00035 Linear_System& sys2,
00036 Saturation_Matrix& sat1,
00037 Saturation_Matrix& sat2,
00038 dimension_type add_dim) {
00039 assert(sys1.topology() == sys2.topology());
00040 assert(sys1.num_columns() == sys2.num_columns());
00041 assert(add_dim != 0);
00042
00043 sys1.add_zero_columns(add_dim);
00044 dimension_type old_index = sys2.first_pending_row();
00045 sys2.add_rows_and_columns(add_dim);
00046
00047 sys2.set_index_first_pending_row(old_index + add_dim);
00048
00049
00050
00051
00052
00053
00054
00055 sat1.resize(sat1.num_rows() + add_dim, sat1.num_columns());
00056
00057 for (dimension_type i = sat1.num_rows() - add_dim; i-- > 0; )
00058 std::swap(sat1[i], sat1[i+add_dim]);
00059
00060 sat2.transpose_assign(sat1);
00061
00062 if (!sys1.is_necessarily_closed()) {
00063
00064 dimension_type new_eps_index = sys1.num_columns() - 1;
00065 dimension_type old_eps_index = new_eps_index - add_dim;
00066
00067 sys1.swap_columns(old_eps_index, new_eps_index);
00068
00069
00070 if (!sys2.is_sorted())
00071 sys2.swap_columns(old_eps_index, new_eps_index);
00072 else {
00073 for (dimension_type i = sys2.num_rows(); i-- > add_dim; ) {
00074 Linear_Row& r = sys2[i];
00075 std::swap(r[old_eps_index], r[new_eps_index]);
00076 }
00077
00078
00079 for (dimension_type i = add_dim; i-- > 0; ++old_eps_index) {
00080 Linear_Row& r = sys2[i];
00081 std::swap(r[old_eps_index], r[old_eps_index + 1]);
00082 }
00083 }
00084
00085
00086 }
00087 }
00088
00089 void
00090 PPL::Polyhedron::add_space_dimensions_and_embed(dimension_type m) {
00091
00092
00093 if (m > max_space_dimension() - space_dimension())
00094 throw_space_dimension_overflow(topology(),
00095 "add_space_dimensions_and_embed(m)",
00096 "adding m new space dimensions exceeds "
00097 "the maximum allowed space dimension");
00098
00099
00100 if (m == 0)
00101 return;
00102
00103
00104
00105
00106 if (marked_empty()) {
00107 space_dim += m;
00108 con_sys.clear();
00109 return;
00110 }
00111
00112
00113 if (space_dim == 0) {
00114
00115 assert(status.test_zero_dim_univ());
00116
00117
00118 Polyhedron ph(topology(), m, UNIVERSE);
00119 swap(ph);
00120 return;
00121 }
00122
00123
00124
00125
00126
00127
00128
00129
00130
00131 if (constraints_are_up_to_date())
00132 if (generators_are_up_to_date()) {
00133
00134 if (!sat_c_is_up_to_date())
00135 update_sat_c();
00136
00137
00138
00139 add_space_dimensions(con_sys, gen_sys, sat_c, sat_g, m);
00140 }
00141 else {
00142
00143 con_sys.add_zero_columns(m);
00144
00145
00146 if (!is_necessarily_closed())
00147 con_sys.swap_columns(space_dim + 1, space_dim + 1 + m);
00148 }
00149 else {
00150
00151 assert(generators_are_up_to_date());
00152 gen_sys.add_rows_and_columns(m);
00153
00154 gen_sys.unset_pending_rows();
00155
00156
00157 if (!is_necessarily_closed()) {
00158
00159 if (!gen_sys.is_sorted())
00160 gen_sys.swap_columns(space_dim + 1, space_dim + 1 + m);
00161 else {
00162 dimension_type old_eps_index = space_dim + 1;
00163 dimension_type new_eps_index = old_eps_index + m;
00164 for (dimension_type i = gen_sys.num_rows(); i-- > m; ) {
00165 Generator& r = gen_sys[i];
00166 std::swap(r[old_eps_index], r[new_eps_index]);
00167 }
00168
00169
00170 for (dimension_type i = m; i-- > 0; ++old_eps_index) {
00171 Generator& r = gen_sys[i];
00172 std::swap(r[old_eps_index], r[old_eps_index + 1]);
00173 }
00174 }
00175 }
00176 }
00177
00178 space_dim += m;
00179
00180
00181
00182 assert(OK());
00183 }
00184
00185 void
00186 PPL::Polyhedron::add_space_dimensions_and_project(dimension_type m) {
00187
00188
00189 if (m > max_space_dimension() - space_dimension())
00190 throw_space_dimension_overflow(topology(),
00191 "add_space_dimensions_and_project(m)",
00192 "adding m new space dimensions exceeds "
00193 "the maximum allowed space dimension");
00194
00195
00196 if (m == 0)
00197 return;
00198
00199
00200
00201 if (marked_empty()) {
00202 space_dim += m;
00203 con_sys.clear();
00204 return;
00205 }
00206
00207 if (space_dim == 0) {
00208 assert(status.test_zero_dim_univ() && gen_sys.num_rows() == 0);
00209
00210
00211
00212
00213
00214 if (!is_necessarily_closed())
00215 gen_sys.insert(Generator::zero_dim_closure_point());
00216 gen_sys.insert(Generator::zero_dim_point());
00217 gen_sys.adjust_topology_and_space_dimension(topology(), m);
00218 set_generators_minimized();
00219 space_dim = m;
00220 assert(OK());
00221 return;
00222 }
00223
00224
00225
00226
00227
00228
00229
00230
00231 if (constraints_are_up_to_date())
00232 if (generators_are_up_to_date()) {
00233
00234 if (!sat_g_is_up_to_date())
00235 update_sat_g();
00236
00237
00238
00239 add_space_dimensions(gen_sys, con_sys, sat_g, sat_c, m);
00240 }
00241 else {
00242
00243 con_sys.add_rows_and_columns(m);
00244
00245 con_sys.unset_pending_rows();
00246
00247
00248 if (!is_necessarily_closed()) {
00249
00250 if (!con_sys.is_sorted())
00251 con_sys.swap_columns(space_dim + 1, space_dim + 1 + m);
00252 else {
00253 dimension_type old_eps_index = space_dim + 1;
00254 dimension_type new_eps_index = old_eps_index + m;
00255 for (dimension_type i = con_sys.num_rows(); i-- > m; ) {
00256 Constraint& r = con_sys[i];
00257 std::swap(r[old_eps_index], r[new_eps_index]);
00258 }
00259
00260
00261 for (dimension_type i = m; i-- > 0; ++old_eps_index) {
00262 Constraint& r = con_sys[i];
00263 std::swap(r[old_eps_index], r[old_eps_index + 1]);
00264 }
00265 }
00266 }
00267 }
00268 else {
00269
00270 assert(generators_are_up_to_date());
00271 gen_sys.add_zero_columns(m);
00272
00273
00274 if (!is_necessarily_closed())
00275 gen_sys.swap_columns(space_dim + 1, space_dim + 1 + m);
00276 }
00277
00278 space_dim += m;
00279
00280
00281
00282 assert(OK());
00283 }
00284
00285 void
00286 PPL::Polyhedron::concatenate_assign(const Polyhedron& y) {
00287 if (topology() != y.topology())
00288 throw_topology_incompatible("concatenate_assign(y)", "y", y);
00289
00290
00291
00292 if (y.space_dim > max_space_dimension() - space_dimension())
00293 throw_space_dimension_overflow(topology(),
00294 "concatenate_assign(y)",
00295 "concatenation exceeds the maximum "
00296 "allowed space dimension");
00297
00298 const dimension_type added_columns = y.space_dim;
00299
00300
00301
00302 if (marked_empty() || y.marked_empty()) {
00303 space_dim += added_columns;
00304 set_empty();
00305 return;
00306 }
00307
00308
00309 if (added_columns == 0)
00310 return;
00311
00312
00313 if (space_dim == 0) {
00314 *this = y;
00315 return;
00316 }
00317
00318
00319 Constraint_System cs = y.constraints();
00320
00321
00322 if (has_pending_generators())
00323 process_pending_generators();
00324 else if (!constraints_are_up_to_date())
00325 update_constraints();
00326
00327
00328
00329
00330
00331 dimension_type old_num_rows = con_sys.num_rows();
00332 dimension_type old_num_columns = con_sys.num_columns();
00333 dimension_type added_rows = cs.num_rows();
00334
00335
00336
00337 assert(added_rows > 0 && added_columns > 0);
00338
00339 con_sys.add_zero_rows_and_columns(added_rows, added_columns,
00340 Linear_Row::Flags(topology(),
00341 Linear_Row::RAY_OR_POINT_OR_INEQUALITY));
00342
00343 if (!is_necessarily_closed())
00344 con_sys.swap_columns(old_num_columns - 1,
00345 old_num_columns - 1 + added_columns);
00346 dimension_type cs_num_columns = cs.num_columns();
00347
00348
00349 for (dimension_type i = added_rows; i-- > 0; ) {
00350 Constraint& c_old = cs[i];
00351 Constraint& c_new = con_sys[old_num_rows + i];
00352
00353
00354 if (c_old.is_equality())
00355 c_new.set_is_equality();
00356
00357 std::swap(c_new[0], c_old[0]);
00358
00359
00360 for (dimension_type j = 1; j < cs_num_columns; ++j)
00361 std::swap(c_old[j], c_new[space_dim + j]);
00362 }
00363
00364 if (can_have_something_pending()) {
00365
00366
00367
00368
00369
00370 gen_sys.add_rows_and_columns(added_columns);
00371 gen_sys.set_sorted(false);
00372 if (!is_necessarily_closed())
00373 gen_sys.swap_columns(old_num_columns - 1,
00374 old_num_columns - 1 + added_columns);
00375
00376 gen_sys.unset_pending_rows();
00377
00378
00379
00380
00381 if (!sat_c_is_up_to_date()) {
00382 sat_c.transpose_assign(sat_g);
00383 set_sat_c_up_to_date();
00384 }
00385 clear_sat_g_up_to_date();
00386 sat_c.resize(sat_c.num_rows() + added_columns, sat_c.num_columns());
00387
00388
00389
00390 for (dimension_type i = sat_c.num_rows() - added_columns; i-- > 0; )
00391 std::swap(sat_c[i], sat_c[i+added_columns]);
00392
00393 set_constraints_pending();
00394 }
00395 else {
00396
00397 con_sys.unset_pending_rows();
00398 #if BE_LAZY
00399 con_sys.set_sorted(false);
00400 #else
00401 con_sys.sort_rows();
00402 #endif
00403 clear_constraints_minimized();
00404 clear_generators_up_to_date();
00405 clear_sat_g_up_to_date();
00406 clear_sat_c_up_to_date();
00407 }
00408
00409 space_dim += added_columns;
00410
00411
00412
00413 assert(OK());
00414 }
00415
00416 void
00417 PPL::Polyhedron::remove_space_dimensions(const Variables_Set& to_be_removed) {
00418
00419
00420
00421 if (to_be_removed.empty()) {
00422 assert(OK());
00423 return;
00424 }
00425
00426
00427
00428 const dimension_type
00429 min_space_dim = to_be_removed.rbegin()->space_dimension();
00430 if (space_dim < min_space_dim)
00431 throw_dimension_incompatible("remove_space_dimensions(vs)", min_space_dim);
00432
00433 const dimension_type new_space_dim = space_dim - to_be_removed.size();
00434
00435
00436
00437 if (marked_empty()
00438 || (has_something_pending() && !remove_pending_to_obtain_generators())
00439 || (!generators_are_up_to_date() && !update_generators())) {
00440
00441
00442
00443 con_sys.clear();
00444
00445 space_dim = new_space_dim;
00446 assert(OK());
00447 return;
00448 }
00449
00450
00451
00452 if (new_space_dim == 0) {
00453 set_zero_dim_univ();
00454 return;
00455 }
00456
00457
00458
00459 Variables_Set::const_iterator tbr = to_be_removed.begin();
00460 Variables_Set::const_iterator tbr_end = to_be_removed.end();
00461 dimension_type dst_col = tbr->space_dimension();
00462 dimension_type src_col = dst_col + 1;
00463 for (++tbr; tbr != tbr_end; ++tbr) {
00464 dimension_type tbr_col = tbr->space_dimension();
00465
00466 while (src_col < tbr_col)
00467 gen_sys.Matrix::swap_columns(dst_col++, src_col++);
00468 ++src_col;
00469 }
00470
00471 const dimension_type gen_sys_num_columns = gen_sys.num_columns();
00472 while (src_col < gen_sys_num_columns)
00473 gen_sys.Matrix::swap_columns(dst_col++, src_col++);
00474
00475
00476
00477 gen_sys.remove_trailing_columns(gen_sys_num_columns - dst_col);
00478
00479 gen_sys.remove_invalid_lines_and_rays();
00480
00481
00482 clear_constraints_up_to_date();
00483 clear_generators_minimized();
00484
00485
00486 space_dim = new_space_dim;
00487
00488 assert(OK(true));
00489 }
00490
00491 void
00492 PPL::Polyhedron::remove_higher_space_dimensions(dimension_type new_dimension) {
00493
00494 if (new_dimension > space_dim)
00495 throw_dimension_incompatible("remove_higher_space_dimensions(nd)",
00496 new_dimension);
00497
00498
00499
00500
00501 if (new_dimension == space_dim) {
00502 assert(OK());
00503 return;
00504 }
00505
00506
00507
00508 if (marked_empty()
00509 || (has_something_pending() && !remove_pending_to_obtain_generators())
00510 || (!generators_are_up_to_date() && !update_generators())) {
00511
00512
00513 space_dim = new_dimension;
00514 con_sys.clear();
00515 assert(OK());
00516 return;
00517 }
00518
00519 if (new_dimension == 0) {
00520
00521
00522 set_zero_dim_univ();
00523 return;
00524 }
00525
00526 dimension_type new_num_cols = new_dimension + 1;
00527 if (!is_necessarily_closed()) {
00528
00529
00530 gen_sys.swap_columns(gen_sys.num_columns() - 1, new_num_cols);
00531
00532 ++new_num_cols;
00533 }
00534
00535 gen_sys.remove_trailing_columns(space_dim - new_dimension);
00536
00537 gen_sys.remove_invalid_lines_and_rays();
00538
00539
00540 clear_constraints_up_to_date();
00541 clear_generators_minimized();
00542
00543
00544 space_dim = new_dimension;
00545
00546 assert(OK(true));
00547 }
00548
00549 void
00550 PPL::Polyhedron::expand_space_dimension(Variable var, dimension_type m) {
00551
00552
00553
00554 if (var.space_dimension() > space_dim)
00555 throw_dimension_incompatible("expand_space_dimension(v, m)", "v", var);
00556
00557
00558
00559 if (m > max_space_dimension() - space_dimension())
00560 throw_space_dimension_overflow(topology(),
00561 "expand_dimension(v, m)",
00562 "adding m new space dimensions exceeds "
00563 "the maximum allowed space dimension");
00564
00565
00566 if (m == 0)
00567 return;
00568
00569
00570 dimension_type old_dim = space_dim;
00571
00572
00573 add_space_dimensions_and_embed(m);
00574
00575 const dimension_type src_d = var.id();
00576 const Constraint_System& cs = constraints();
00577 Constraint_System new_constraints;
00578 for (Constraint_System::const_iterator i = cs.begin(),
00579 cs_end = cs.end(); i != cs_end; ++i) {
00580 const Constraint& c = *i;
00581
00582
00583 if (c.coefficient(var) == 0)
00584 continue;
00585
00586
00587 for (dimension_type dst_d = old_dim; dst_d < old_dim+m; ++dst_d) {
00588 Linear_Expression e;
00589 for (dimension_type j = old_dim; j-- > 0; )
00590 e +=
00591 c.coefficient(Variable(j))
00592 * (j == src_d ? Variable(dst_d) : Variable(j));
00593 e += c.inhomogeneous_term();
00594 new_constraints.insert(c.is_equality()
00595 ? (e == 0)
00596 : (c.is_nonstrict_inequality()
00597 ? (e >= 0)
00598 : (e > 0)));
00599 }
00600 }
00601 add_constraints(new_constraints);
00602 assert(OK());
00603 }
00604
00605 void
00606 PPL::Polyhedron::fold_space_dimensions(const Variables_Set& to_be_folded,
00607 Variable var) {
00608
00609
00610
00611 if (var.space_dimension() > space_dim)
00612 throw_dimension_incompatible("fold_space_dimensions(tbf, v)", "v", var);
00613
00614
00615 if (to_be_folded.empty())
00616 return;
00617
00618
00619 if (to_be_folded.rbegin()->space_dimension() > space_dim)
00620 throw_dimension_incompatible("fold_space_dimensions(tbf, v)",
00621 "*tbf.rbegin()",
00622 *to_be_folded.rbegin());
00623
00624
00625 if (to_be_folded.find(var) != to_be_folded.end())
00626 throw_invalid_argument("fold_space_dimensions(tbf, v)",
00627 "v should not occur in tbf");
00628
00629 for (Variables_Set::const_iterator i = to_be_folded.begin(),
00630 tbf_end = to_be_folded.end(); i != tbf_end; ++i) {
00631 Polyhedron copy = *this;
00632 copy.affine_image(var, Linear_Expression(*i));
00633 poly_hull_assign(copy);
00634 }
00635 remove_space_dimensions(to_be_folded);
00636 assert(OK());
00637 }