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