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 "Grid.defs.hh"
00027
00028 #include <cassert>
00029 #include <iostream>
00030
00031 namespace PPL = Parma_Polyhedra_Library;
00032
00033 void
00034 PPL::Grid::select_wider_congruences(const Grid& y,
00035 Congruence_System& cgs_selected) const {
00036
00037
00038 assert(space_dim == y.space_dim);
00039 assert(!marked_empty());
00040 assert(!y.marked_empty());
00041 assert(congruences_are_minimized());
00042 assert(y.congruences_are_minimized());
00043
00044
00045
00046 for (dimension_type dim = con_sys.space_dimension(), x_row = 0, y_row = 0;
00047 dim > 0; --dim) {
00048 assert(dim_kinds[dim] == CON_VIRTUAL
00049 || dim_kinds[dim] == y.dim_kinds[dim]);
00050 switch (dim_kinds[dim]) {
00051 case PROPER_CONGRUENCE:
00052 {
00053 const Congruence& cg = con_sys[x_row];
00054 const Congruence& y_cg = y.con_sys[y_row];
00055 if (cg.is_equal_at_dimension(dim, y_cg))
00056
00057 cgs_selected.insert(cg);
00058 ++x_row;
00059 ++y_row;
00060 }
00061 break;
00062 case EQUALITY:
00063 cgs_selected.insert(con_sys[x_row]);
00064 ++x_row;
00065 ++y_row;
00066 break;
00067 case CON_VIRTUAL:
00068 y.dim_kinds[dim] == CON_VIRTUAL || ++y_row;
00069 break;
00070 }
00071 }
00072 }
00073
00074 void
00075 PPL::Grid::congruence_widening_assign(const Grid& const_y, unsigned* tp) {
00076 Grid& x = *this;
00077 Grid& y = const_cast<Grid&>(const_y);
00078
00079 if (x.space_dim != y.space_dim)
00080 throw_dimension_incompatible("widening_assign(y)", "y", y);
00081
00082
00083
00084 #ifndef NDEBUG
00085 {
00086
00087 const Grid x_copy = x;
00088 const Grid y_copy = y;
00089 assert(x_copy.contains(y_copy));
00090 }
00091 #endif
00092
00093
00094 if (x.space_dim == 0 || x.marked_empty() || y.marked_empty())
00095 return;
00096
00097
00098 if (x.congruences_are_up_to_date()) {
00099 if (!x.congruences_are_minimized()) {
00100 if (simplify(x.con_sys, x.dim_kinds)) {
00101
00102 x.set_empty();
00103 return;
00104 }
00105 x.set_congruences_minimized();
00106 }
00107 }
00108 else
00109 x.update_congruences();
00110
00111
00112 if (y.congruences_are_up_to_date()) {
00113 if (!y.congruences_are_minimized()) {
00114 if (simplify(y.con_sys, y.dim_kinds)) {
00115
00116 y.set_empty();
00117 return;
00118 }
00119 y.set_congruences_minimized();
00120 }
00121 }
00122 else
00123 y.update_congruences();
00124
00125 if (con_sys.num_equalities() < y.con_sys.num_equalities())
00126 return;
00127
00128
00129
00130 Congruence_System cgs;
00131 x.select_wider_congruences(y, cgs);
00132
00133 if (cgs.num_rows() == con_sys.num_rows())
00134
00135 return;
00136
00137
00138
00139 Grid result(x.space_dim);
00140 result.add_recycled_congruences(cgs);
00141
00142
00143
00144 if (tp && *tp > 0) {
00145
00146
00147
00148 if (!x.contains(result))
00149 --(*tp);
00150 }
00151 else
00152
00153 std::swap(x, result);
00154
00155 assert(x.OK(true));
00156 }
00157
00158 void
00159 PPL::Grid::limited_congruence_extrapolation_assign(const Grid& y,
00160 const Congruence_System& cgs,
00161 unsigned* tp) {
00162 Grid& x = *this;
00163
00164
00165 if (x.space_dim != y.space_dim)
00166 throw_dimension_incompatible("limited_extrapolation_assign(y, cgs)",
00167 "y", y);
00168
00169 const dimension_type cgs_space_dim = cgs.space_dimension();
00170 if (x.space_dim < cgs_space_dim)
00171 throw_dimension_incompatible("limited_extrapolation_assign(y, cgs)",
00172 "cgs", cgs);
00173
00174 const dimension_type cgs_num_rows = cgs.num_rows();
00175
00176 if (cgs_num_rows == 0) {
00177 x.widening_assign(y, tp);
00178 return;
00179 }
00180
00181 #ifndef NDEBUG
00182 {
00183
00184 const Grid x_copy = x;
00185 const Grid y_copy = y;
00186 assert(x_copy.contains(y_copy));
00187 }
00188 #endif
00189
00190 if (y.marked_empty())
00191 return;
00192 if (x.marked_empty())
00193 return;
00194
00195
00196
00197 if (x.space_dim == 0)
00198 return;
00199
00200
00201
00202
00203 if (!x.generators_are_up_to_date() && !x.update_generators())
00204
00205 return;
00206
00207 if (tp == NULL || *tp == 0) {
00208
00209 Congruence_System new_cgs;
00210
00211
00212
00213 for (dimension_type i = 0; i < cgs_num_rows; ++i) {
00214 const Congruence& cg = cgs[i];
00215 if (x.relation_with(cg) == Poly_Con_Relation::is_included())
00216 new_cgs.insert(cg);
00217 }
00218 x.congruence_widening_assign(y, tp);
00219 x.add_recycled_congruences(new_cgs);
00220 }
00221 else
00222
00223 x.congruence_widening_assign(y, tp);
00224
00225 assert(OK());
00226 }
00227
00228 void
00229 PPL::Grid::select_wider_generators(const Grid& y,
00230 Grid_Generator_System& ggs_selected) const {
00231
00232
00233 assert(space_dim == y.space_dim);
00234 assert(!marked_empty());
00235 assert(!y.marked_empty());
00236 assert(generators_are_minimized());
00237 assert(y.generators_are_minimized());
00238
00239
00240
00241 for (dimension_type dim = 0, x_row = 0, y_row = 0;
00242 dim <= gen_sys.space_dimension(); ++dim) {
00243 assert(dim_kinds[dim] == LINE
00244 || y.dim_kinds[dim] == GEN_VIRTUAL
00245 || dim_kinds[dim] == y.dim_kinds[dim]);
00246 switch (dim_kinds[dim]) {
00247 case PARAMETER:
00248 {
00249 const Grid_Generator& gg = gen_sys[x_row];
00250 const Grid_Generator& y_gg = y.gen_sys[y_row];
00251 if (gg.is_equal_at_dimension(dim, y_gg))
00252
00253 ggs_selected.insert(gg);
00254 else {
00255 Linear_Expression e;
00256 for (dimension_type i = gg.space_dimension(); i-- > 0; )
00257 e += gg.coefficient(Variable(i)) * Variable(i);
00258 ggs_selected.insert(grid_line(e));
00259 }
00260 ++x_row;
00261 ++y_row;
00262 }
00263 break;
00264 case LINE:
00265 ggs_selected.insert(gen_sys[x_row]);
00266 ++x_row;
00267 ++y_row;
00268 break;
00269 case GEN_VIRTUAL:
00270 y.dim_kinds[dim] == GEN_VIRTUAL || ++y_row;
00271 break;
00272 }
00273 }
00274 }
00275
00276 void
00277 PPL::Grid::generator_widening_assign(const Grid& const_y, unsigned* tp) {
00278 Grid& x = *this;
00279 Grid& y = const_cast<Grid&>(const_y);
00280
00281 if (x.space_dim != y.space_dim)
00282 throw_dimension_incompatible("generator_widening_assign(y)", "y", y);
00283
00284
00285
00286 #ifndef NDEBUG
00287 {
00288
00289 const Grid x_copy = x;
00290 const Grid y_copy = y;
00291 assert(x_copy.contains(y_copy));
00292 }
00293 #endif
00294
00295
00296 if (x.space_dim == 0 || x.marked_empty() || y.marked_empty())
00297 return;
00298
00299
00300 if (x.generators_are_up_to_date()) {
00301 if (!x.generators_are_minimized()) {
00302 simplify(x.gen_sys, x.dim_kinds);
00303 assert(!x.gen_sys.has_no_rows());
00304 x.set_generators_minimized();
00305 }
00306 }
00307 else
00308 x.update_generators();
00309
00310 if (x.marked_empty())
00311 return;
00312
00313
00314 if (y.generators_are_up_to_date()) {
00315 if (!y.generators_are_minimized()) {
00316 simplify(y.gen_sys, y.dim_kinds);
00317 assert(!y.gen_sys.has_no_rows());
00318 y.set_generators_minimized();
00319 }
00320 }
00321 else
00322 y.update_generators();
00323
00324 if (gen_sys.num_rows() > y.gen_sys.num_rows())
00325 return;
00326
00327 if (gen_sys.num_lines() > y.gen_sys.num_lines())
00328 return;
00329
00330
00331
00332 Grid_Generator_System ggs;
00333 x.select_wider_generators(y, ggs);
00334
00335 if (ggs.num_parameters() == gen_sys.num_parameters())
00336
00337 return;
00338
00339
00340
00341 Grid result(x.space_dim, EMPTY);
00342 result.add_recycled_grid_generators(ggs);
00343
00344
00345
00346 if (tp && *tp > 0) {
00347
00348
00349
00350 if (!x.contains(result))
00351 --(*tp);
00352 }
00353 else
00354
00355 std::swap(x, result);
00356
00357 assert(x.OK(true));
00358 }
00359
00360 void
00361 PPL::Grid::limited_generator_extrapolation_assign(const Grid& y,
00362 const Congruence_System& cgs,
00363 unsigned* tp) {
00364 Grid& x = *this;
00365
00366
00367 if (x.space_dim != y.space_dim)
00368 throw_dimension_incompatible("limited_extrapolation_assign(y, cgs)",
00369 "y", y);
00370
00371 const dimension_type cgs_space_dim = cgs.space_dimension();
00372 if (x.space_dim < cgs_space_dim)
00373 throw_dimension_incompatible("limited_extrapolation_assign(y, cgs)",
00374 "cgs", cgs);
00375
00376 const dimension_type cgs_num_rows = cgs.num_rows();
00377
00378 if (cgs_num_rows == 0) {
00379 x.generator_widening_assign(y, tp);
00380 return;
00381 }
00382
00383 #ifndef NDEBUG
00384 {
00385
00386 const Grid x_copy = x;
00387 const Grid y_copy = y;
00388 assert(x_copy.contains(y_copy));
00389 }
00390 #endif
00391
00392 if (y.marked_empty())
00393 return;
00394 if (x.marked_empty())
00395 return;
00396
00397
00398
00399 if (x.space_dim == 0)
00400 return;
00401
00402
00403
00404
00405 if (!x.generators_are_up_to_date() && !x.update_generators())
00406
00407 return;
00408
00409 if (tp == NULL || *tp == 0) {
00410
00411 Congruence_System new_cgs;
00412
00413
00414
00415 for (dimension_type i = 0; i < cgs_num_rows; ++i) {
00416 const Congruence& cg = cgs[i];
00417 if (x.relation_with(cg) == Poly_Con_Relation::is_included())
00418 new_cgs.insert(cg);
00419 }
00420 x.generator_widening_assign(y, tp);
00421 x.add_recycled_congruences(new_cgs);
00422 }
00423 else
00424
00425 x.generator_widening_assign(y, tp);
00426
00427 assert(OK());
00428 }
00429
00430 void
00431 PPL::Grid::widening_assign(const Grid& const_y, unsigned* tp) {
00432 Grid& x = *this;
00433 Grid& y = const_cast<Grid&>(const_y);
00434
00435 if (x.space_dim != y.space_dim)
00436 throw_dimension_incompatible("widening_assign(y)", "y", y);
00437
00438
00439
00440 #ifndef NDEBUG
00441 {
00442
00443 const Grid x_copy = x;
00444 const Grid y_copy = y;
00445 assert(x_copy.contains(y_copy));
00446 }
00447 #endif
00448
00449
00450
00451 if (x.congruences_are_up_to_date() && y.congruences_are_up_to_date()) {
00452 x.congruence_widening_assign(y, tp);
00453 return;
00454 }
00455
00456
00457
00458 if (x.generators_are_up_to_date() && y.generators_are_up_to_date()) {
00459 x.generator_widening_assign(y, tp);
00460 return;
00461 }
00462
00463 x.congruence_widening_assign(y, tp);
00464 }
00465
00466 void
00467 PPL::Grid::limited_extrapolation_assign(const Grid& y,
00468 const Congruence_System& cgs,
00469 unsigned* tp) {
00470 Grid& x = *this;
00471
00472
00473 if (x.space_dim != y.space_dim)
00474 throw_dimension_incompatible("limited_extrapolation_assign(y, cgs)",
00475 "y", y);
00476
00477 const dimension_type cgs_space_dim = cgs.space_dimension();
00478 if (x.space_dim < cgs_space_dim)
00479 throw_dimension_incompatible("limited_extrapolation_assign(y, cgs)",
00480 "cgs", cgs);
00481
00482 const dimension_type cgs_num_rows = cgs.num_rows();
00483
00484 if (cgs_num_rows == 0) {
00485 x.widening_assign(y, tp);
00486 return;
00487 }
00488
00489 #ifndef NDEBUG
00490 {
00491
00492 const Grid x_copy = x;
00493 const Grid y_copy = y;
00494 assert(x_copy.contains(y_copy));
00495 }
00496 #endif
00497
00498 if (y.marked_empty())
00499 return;
00500 if (x.marked_empty())
00501 return;
00502
00503
00504
00505 if (x.space_dim == 0)
00506 return;
00507
00508
00509
00510
00511 if (!x.generators_are_up_to_date() && !x.update_generators())
00512
00513 return;
00514
00515 if (tp == NULL || *tp == 0) {
00516
00517 Congruence_System new_cgs;
00518
00519
00520
00521 for (dimension_type i = 0; i < cgs_num_rows; ++i) {
00522 const Congruence& cg = cgs[i];
00523 if (x.relation_with(cg) == Poly_Con_Relation::is_included())
00524 new_cgs.insert(cg);
00525 }
00526 x.widening_assign(y, tp);
00527 x.add_recycled_congruences(new_cgs);
00528 }
00529 else
00530
00531 x.widening_assign(y, tp);
00532
00533 assert(OK());
00534 }