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 "Grid.defs.hh"
00027 #include <cassert>
00028
00029 #define BE_LAZY 1
00030
00031 namespace PPL = Parma_Polyhedra_Library;
00032
00033
00034 inline void
00035 PPL::Grid::add_space_dimensions(Congruence_System& cgs,
00036 Grid_Generator_System& gs,
00037 const dimension_type dims) {
00038 assert(cgs.num_columns() - 1 == gs.space_dimension() + 1);
00039 assert(dims > 0);
00040
00041 dimension_type tem = cgs.num_columns() - 1;
00042 cgs.add_zero_columns(dims);
00043
00044 cgs.swap_columns(tem, tem + dims);
00045
00046 if (congruences_are_minimized() || generators_are_minimized())
00047 dim_kinds.resize(tem + dims, CON_VIRTUAL );
00048
00049 gs.add_universe_rows_and_columns(dims);
00050 }
00051
00052
00053 inline void
00054 PPL::Grid::add_space_dimensions(Grid_Generator_System& gs,
00055 Congruence_System& cgs,
00056 const dimension_type dims) {
00057 assert(cgs.num_columns() - 1 == gs.space_dimension() + 1);
00058 assert(dims > 0);
00059
00060 cgs.add_unit_rows_and_columns(dims);
00061
00062
00063 gs.insert(parameter(0*Variable(space_dim + dims - 1)));
00064
00065 normalize_divisors(gs);
00066
00067 dim_kinds.resize(cgs.num_columns() - 1, EQUALITY );
00068 }
00069
00070
00071
00072
00073
00074
00075
00076
00077
00078 void
00079 PPL::Grid::add_space_dimensions_and_embed(dimension_type m) {
00080 if (m == 0)
00081 return;
00082
00083
00084
00085 if (m > max_space_dimension() - space_dimension())
00086 throw_space_dimension_overflow("add_space_dimensions_and_embed(m)",
00087 "adding m new space dimensions exceeds "
00088 "the maximum allowed space dimension");
00089
00090
00091
00092
00093 if (marked_empty()) {
00094 space_dim += m;
00095 set_empty();
00096 return;
00097 }
00098
00099
00100 if (space_dim == 0) {
00101
00102 assert(status.test_zero_dim_univ());
00103
00104 Grid gr(m, UNIVERSE);
00105 swap(gr);
00106 return;
00107 }
00108
00109
00110
00111
00112
00113
00114
00115
00116 if (congruences_are_up_to_date())
00117 if (generators_are_up_to_date())
00118
00119 add_space_dimensions(con_sys, gen_sys, m);
00120 else {
00121
00122 con_sys.add_zero_columns(m);
00123 dimension_type size = con_sys.num_columns() - 1;
00124
00125 con_sys.swap_columns(size - m, size);
00126 if (congruences_are_minimized())
00127 dim_kinds.resize(size, CON_VIRTUAL);
00128 }
00129 else {
00130
00131 assert(generators_are_up_to_date());
00132 gen_sys.add_universe_rows_and_columns(m);
00133 if (generators_are_minimized())
00134 dim_kinds.resize(gen_sys.space_dimension() + 1, LINE);
00135 }
00136
00137 space_dim += m;
00138
00139
00140
00141 assert(OK());
00142 }
00143
00144
00145
00146
00147
00148
00149
00150
00151
00152 void
00153 PPL::Grid::add_space_dimensions_and_project(dimension_type m) {
00154 if (m == 0)
00155 return;
00156
00157
00158
00159 if (m > max_space_dimension() - space_dimension())
00160 throw_space_dimension_overflow("add_space_dimensions_and_project(m)",
00161 "adding m new space dimensions exceeds "
00162 "the maximum allowed space dimension");
00163
00164
00165
00166 if (marked_empty()) {
00167 space_dim += m;
00168 set_empty();
00169 return;
00170 }
00171
00172 if (space_dim == 0) {
00173 assert(status.test_zero_dim_univ());
00174
00175 Grid gr(m, UNIVERSE);
00176 swap(gr);
00177 return;
00178 }
00179
00180
00181
00182
00183
00184
00185
00186
00187 if (congruences_are_up_to_date())
00188 if (generators_are_up_to_date())
00189
00190 add_space_dimensions(gen_sys, con_sys, m);
00191 else {
00192
00193 con_sys.add_unit_rows_and_columns(m);
00194 if (congruences_are_minimized())
00195 dim_kinds.resize(con_sys.num_columns() - 1, EQUALITY);
00196 }
00197 else {
00198
00199 assert(generators_are_up_to_date());
00200
00201
00202 gen_sys.insert(parameter(0*Variable(space_dim + m - 1)));
00203
00204 normalize_divisors(gen_sys);
00205
00206 if (generators_are_minimized())
00207 dim_kinds.resize(gen_sys.space_dimension() + 1, EQUALITY);
00208 }
00209
00210 space_dim += m;
00211
00212
00213
00214 assert(OK());
00215 }
00216
00217 void
00218 PPL::Grid::concatenate_assign(const Grid& y) {
00219
00220
00221 if (y.space_dim > max_space_dimension() - space_dimension())
00222 throw_space_dimension_overflow("concatenate_assign(y)",
00223 "concatenation exceeds the maximum "
00224 "allowed space dimension");
00225
00226 const dimension_type added_columns = y.space_dim;
00227
00228
00229
00230 if (marked_empty() || y.marked_empty()) {
00231 space_dim += added_columns;
00232 set_empty();
00233 return;
00234 }
00235
00236
00237 if (added_columns == 0)
00238 return;
00239
00240
00241 if (space_dim == 0) {
00242 *this = y;
00243 return;
00244 }
00245
00246 congruences_are_up_to_date() || update_congruences();
00247
00248 con_sys.concatenate(y.congruences());
00249
00250 space_dim += added_columns;
00251
00252 clear_congruences_minimized();
00253 clear_generators_up_to_date();
00254
00255
00256
00257 assert(OK());
00258 }
00259
00260 void
00261 PPL::Grid::remove_space_dimensions(const Variables_Set& to_be_removed) {
00262
00263
00264
00265 if (to_be_removed.empty()) {
00266 assert(OK());
00267 return;
00268 }
00269
00270
00271
00272 const dimension_type
00273 min_space_dim = to_be_removed.rbegin()->space_dimension();
00274 if (space_dim < min_space_dim)
00275 throw_dimension_incompatible("remove_space_dimensions(vs)", min_space_dim);
00276
00277 const dimension_type new_space_dim = space_dim - to_be_removed.size();
00278
00279 if (marked_empty()
00280 || (!generators_are_up_to_date() && !update_generators())) {
00281
00282 space_dim = new_space_dim;
00283 set_empty();
00284 assert(OK());
00285 return;
00286 }
00287
00288
00289
00290 if (new_space_dim == 0) {
00291 set_zero_dim_univ();
00292 return;
00293 }
00294
00295
00296
00297
00298 gen_sys.remove_space_dimensions(to_be_removed);
00299
00300 clear_congruences_up_to_date();
00301 clear_generators_minimized();
00302
00303
00304 space_dim = new_space_dim;
00305
00306 assert(OK(true));
00307 }
00308
00309 void
00310 PPL::Grid::remove_higher_space_dimensions(dimension_type new_dimension) {
00311
00312 if (new_dimension > space_dim)
00313 throw_dimension_incompatible("remove_higher_space_dimensions(nd)",
00314 new_dimension);
00315
00316
00317
00318
00319 if (new_dimension == space_dim) {
00320 assert(OK());
00321 return;
00322 }
00323
00324 if (marked_empty()
00325 || (!generators_are_up_to_date() && !update_generators())) {
00326
00327
00328 space_dim = new_dimension;
00329 set_empty();
00330 assert(OK());
00331 return;
00332 }
00333
00334 if (new_dimension == 0) {
00335
00336
00337 set_zero_dim_univ();
00338 return;
00339 }
00340
00341 gen_sys.remove_higher_space_dimensions(new_dimension);
00342
00343 #if 0
00344
00345
00346 if (generators_are_minimized()) {
00347 gen_sys.erase_to_end(new_dimension + 1);
00348 dim_kinds.erase(dim_kinds.begin() + new_dimension + 1, dim_kinds.end());
00349 }
00350 #else
00351 clear_generators_minimized();
00352 #endif
00353
00354 clear_congruences_up_to_date();
00355
00356
00357 space_dim = new_dimension;
00358
00359 assert(OK(true));
00360 }
00361
00362 void
00363 PPL::Grid::expand_space_dimension(Variable var, dimension_type m) {
00364
00365
00366
00367 if (var.space_dimension() > space_dim)
00368 throw_dimension_incompatible("expand_space_dimension(v, m)", "v", var);
00369
00370
00371 if (m == 0)
00372 return;
00373
00374
00375 if (m > max_space_dimension() - space_dimension())
00376 throw_space_dimension_overflow("expand_space_dimension(v, m)",
00377 "adding m new space dimensions exceeds "
00378 "the maximum allowed space dimension");
00379
00380
00381 dimension_type old_dim = space_dim;
00382
00383
00384 add_space_dimensions_and_embed(m);
00385
00386 const dimension_type src_d = var.id();
00387 const Congruence_System& cgs = congruences();
00388 Congruence_System new_congruences;
00389 for (Congruence_System::const_iterator i = cgs.begin(),
00390 cgs_end = cgs.end(); i != cgs_end; ++i) {
00391 const Congruence& cg = *i;
00392
00393
00394 if (cg.coefficient(var) == 0)
00395 continue;
00396
00397
00398 for (dimension_type dst_d = old_dim; dst_d < old_dim+m; ++dst_d) {
00399 Linear_Expression e;
00400 for (dimension_type j = old_dim; j-- > 0; )
00401 e +=
00402 cg.coefficient(Variable(j))
00403 * (j == src_d ? Variable(dst_d) : Variable(j));
00404 new_congruences.insert_verbatim((e + cg.inhomogeneous_term() %= 0)
00405 / cg.modulus());
00406 }
00407 }
00408 add_congruences(new_congruences);
00409 assert(OK());
00410 }
00411
00412 void
00413 PPL::Grid::fold_space_dimensions(const Variables_Set& to_be_folded,
00414 Variable var) {
00415
00416
00417
00418 if (var.space_dimension() > space_dim)
00419 throw_dimension_incompatible("fold_space_dimensions(tbf, v)", "v", var);
00420
00421
00422 if (to_be_folded.empty())
00423 return;
00424
00425
00426 if (to_be_folded.rbegin()->space_dimension() > space_dim)
00427 throw_dimension_incompatible("fold_space_dimensions(tbf, v)",
00428 "*tbf.rbegin()",
00429 *to_be_folded.rbegin());
00430
00431
00432 if (to_be_folded.find(var) != to_be_folded.end())
00433 throw_invalid_argument("fold_space_dimensions(tbf, v)",
00434 "v should not occur in tbf");
00435
00436 for (Variables_Set::const_iterator i = to_be_folded.begin(),
00437 tbf_end = to_be_folded.end(); i != tbf_end; ++i) {
00438 Grid copy = *this;
00439 copy.affine_image(var, Linear_Expression(*i));
00440 join_assign(copy);
00441 }
00442 remove_space_dimensions(to_be_folded);
00443 assert(OK());
00444 }