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 "Grid_Generator.defs.hh"
00028 #include "Scalar_Products.defs.hh"
00029 #include <cassert>
00030 #include <string>
00031 #include <iostream>
00032 #include <sstream>
00033 #include <stdexcept>
00034
00035 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00036
00045 #endif // PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00046 #define BE_LAZY 1
00047
00048 namespace PPL = Parma_Polyhedra_Library;
00049
00050 void
00051 PPL::Grid::construct(const Congruence_System& ccgs) {
00052
00053 assert(ccgs.space_dimension() <= max_space_dimension());
00054
00055
00056 Congruence_System cgs = ccgs;
00057
00058
00059 space_dim = cgs.space_dimension();
00060
00061 if (space_dim > 0) {
00062
00063 std::swap(con_sys, cgs);
00064 con_sys.normalize_moduli();
00065 set_congruences_up_to_date();
00066 }
00067 else {
00068
00069 if (cgs.num_columns() > 1)
00070
00071 for (dimension_type i = cgs.num_rows(); i-- > 0; )
00072 if (cgs[i].is_trivial_false()) {
00073
00074
00075
00076
00077 set_empty();
00078 assert(OK());
00079 return;
00080 }
00081 set_zero_dim_univ();
00082 }
00083
00084 assert(OK());
00085 }
00086
00087 void
00088 PPL::Grid::construct(const Grid_Generator_System& const_gs) {
00089
00090 assert(const_gs.space_dimension() <= max_space_dimension());
00091
00092
00093 Grid_Generator_System gs = const_gs;
00094
00095
00096 space_dim = gs.space_dimension();
00097
00098
00099 if (gs.num_generators() == 0) {
00100
00101
00102
00103 set_empty();
00104 return;
00105 }
00106
00107
00108 if (!gs.has_points())
00109 throw_invalid_generators("Grid(const_gs)", "gs");
00110
00111 if (space_dim > 0) {
00112
00113 std::swap(gen_sys, gs);
00114 normalize_divisors(gen_sys);
00115
00116
00117 set_generators_up_to_date();
00118 }
00119 else
00120 set_zero_dim_univ();
00121
00122 assert(OK());
00123 }
00124
00125 PPL::Grid::Three_Valued_Boolean
00126 PPL::Grid::quick_equivalence_test(const Grid& y) const {
00127
00128 assert(space_dim == y.space_dim);
00129 assert(!marked_empty() && !y.marked_empty() && space_dim > 0);
00130
00131 const Grid& x = *this;
00132
00133 bool css_normalized = false;
00134
00135 if (x.congruences_are_minimized() && y.congruences_are_minimized()) {
00136
00137
00138 if (x.con_sys.num_rows() != y.con_sys.num_rows())
00139 return Grid::TVB_FALSE;
00140
00141 dimension_type x_num_equalities = x.con_sys.num_equalities();
00142 if (x_num_equalities != y.con_sys.num_equalities())
00143 return Grid::TVB_FALSE;
00144
00145
00146 css_normalized = (x_num_equalities == 0);
00147 }
00148
00149 if (x.generators_are_minimized() && y.generators_are_minimized()) {
00150
00151
00152 if (x.gen_sys.num_generators() != y.gen_sys.num_generators())
00153 return Grid::TVB_FALSE;
00154
00155 const dimension_type x_num_lines = x.gen_sys.num_lines();
00156 if (x_num_lines != y.gen_sys.num_lines())
00157 return Grid::TVB_FALSE;
00158
00159 if (x_num_lines == 0) {
00160
00161 if (x.gen_sys == y.gen_sys)
00162 return Grid::TVB_TRUE;
00163 else
00164 return Grid::TVB_FALSE;
00165 }
00166 }
00167
00168
00169
00170
00171 if (css_normalized)
00172 if (x.con_sys == y.con_sys)
00173 return Grid::TVB_TRUE;
00174 else
00175 return Grid::TVB_FALSE;
00176
00177 return Grid::TVB_DONT_KNOW;
00178 }
00179
00180 bool
00181 PPL::Grid::is_included_in(const Grid& y) const {
00182
00183 assert(space_dim == y.space_dim);
00184 assert(!marked_empty() && !y.marked_empty() && space_dim > 0);
00185
00186 const Grid& x = *this;
00187
00188 #if BE_LAZY
00189 if (!x.generators_are_up_to_date() && !x.update_generators())
00190
00191 return true;
00192 y.congruences_are_up_to_date() || y.update_congruences();
00193 #else
00194 if (!x.generators_are_minimized() && !x.minimize())
00195
00196 return true;
00197 y.congruences_are_minimized() || y.minimize();
00198 #endif
00199
00200 assert(x.OK());
00201 assert(y.OK());
00202
00203 const Grid_Generator_System& gs = x.gen_sys;
00204 const Congruence_System& cgs = y.con_sys;
00205
00206 dimension_type num_rows = gs.num_generators();
00207 for (dimension_type i = num_rows; i-- > 0; )
00208 if (!cgs.satisfies_all_congruences(gs[i]))
00209 return false;
00210
00211
00212 return true;
00213 }
00214
00215 bool
00216 PPL::Grid::bounds(const Linear_Expression& expr,
00217 const char* method_call) const {
00218
00219 if (space_dim < expr.space_dimension())
00220 throw_dimension_incompatible(method_call, "e", expr);
00221
00222
00223 if (space_dim == 0
00224 || marked_empty()
00225 || (!generators_are_up_to_date() && !update_generators()))
00226 return true;
00227
00228
00229 for (dimension_type i = gen_sys.num_generators(); i-- > 0; ) {
00230 const Grid_Generator& g = gen_sys[i];
00231
00232
00233 if (g.is_line_or_parameter()) {
00234 const int sp_sign = Scalar_Products::homogeneous_sign(expr, g);
00235 if (sp_sign != 0)
00236
00237 return false;
00238 }
00239 }
00240 return true;
00241 }
00242
00243 bool
00244 PPL::Grid::max_min(const Linear_Expression& expr,
00245 char* method_call,
00246 Coefficient& ext_n, Coefficient& ext_d, bool& included,
00247 Grid_Generator* point) const {
00248 if (bounds(expr, method_call)) {
00249 if (marked_empty())
00250 return false;
00251 if (space_dim == 0) {
00252 ext_n = 0;
00253 ext_d = 1;
00254 included = true;
00255 if (point)
00256 *point = Grid_Generator::point();
00257 return true;
00258 }
00259 if (!generators_are_minimized()) {
00260
00261 Grid& gr = const_cast<Grid&>(*this);
00262 gr.simplify(gr.gen_sys, gr.dim_kinds);
00263 gr.set_generators_minimized();
00264 }
00265
00266 const Grid_Generator& gen = gen_sys[0];
00267 Scalar_Products::homogeneous_assign(ext_n, expr, gen);
00268 ext_n += expr.inhomogeneous_term();
00269 ext_d = gen.divisor();
00270
00271 TEMP_INTEGER(gcd);
00272 gcd_assign(gcd, ext_n, ext_d);
00273 exact_div_assign(ext_n, ext_n, gcd);
00274 exact_div_assign(ext_d, ext_d, gcd);
00275
00276 included = true;
00277 if (point) {
00278 *point = gen;
00279 point->strong_normalize();
00280 }
00281 return true;
00282 }
00283 return false;
00284 }
00285
00286 void
00287 PPL::Grid::set_zero_dim_univ() {
00288 status.set_zero_dim_univ();
00289 space_dim = 0;
00290 con_sys.clear();
00291 gen_sys.clear();
00292 gen_sys.insert(Grid_Generator::point());
00293 }
00294
00295 void
00296 PPL::Grid::set_empty() {
00297 status.set_empty();
00298
00299
00300 Grid_Generator_System gs(space_dim);
00301 gen_sys.swap(gs);
00302
00303
00304
00305 Congruence_System cgs(Congruence::zero_dim_false());
00306 cgs.increase_space_dimension(space_dim);
00307 const_cast<Congruence_System&>(con_sys).swap(cgs);
00308 }
00309
00310 bool
00311 PPL::Grid::update_congruences() const {
00312
00313 assert(space_dim > 0);
00314 assert(!marked_empty());
00315 assert(gen_sys.num_generators() > 0);
00316 assert(gen_sys.space_dimension() > 0);
00317
00318 Grid& gr = const_cast<Grid&>(*this);
00319
00320 if (!generators_are_minimized())
00321 gr.simplify(gr.gen_sys, gr.dim_kinds);
00322
00323
00324
00325 assert(gen_sys.num_generators() > 0);
00326
00327
00328
00329 gr.conversion(gr.gen_sys, gr.con_sys, gr.dim_kinds);
00330
00331
00332 gr.set_congruences_minimized();
00333 gr.set_generators_minimized();
00334 return true;
00335 }
00336
00337 bool
00338 PPL::Grid::update_generators() const {
00339 assert(space_dim > 0);
00340 assert(!marked_empty());
00341 assert(congruences_are_up_to_date());
00342
00343 Grid& x = const_cast<Grid&>(*this);
00344
00345 if (!congruences_are_minimized())
00346
00347
00348 if (simplify(x.con_sys, x.dim_kinds)) {
00349 x.set_empty();
00350 return false;
00351 }
00352
00353
00354
00355 conversion(x.con_sys, x.gen_sys, x.dim_kinds);
00356
00357
00358 x.set_congruences_minimized();
00359 x.set_generators_minimized();
00360 return true;
00361 }
00362
00363 bool
00364 PPL::Grid::minimize() const {
00365
00366 if (marked_empty())
00367 return false;
00368 if (space_dim == 0)
00369 return true;
00370
00371
00372 if (congruences_are_minimized() && generators_are_minimized())
00373 return true;
00374
00375
00376
00377 if (congruences_are_up_to_date()) {
00378 if (generators_are_up_to_date()) {
00379 Grid& gr = const_cast<Grid&>(*this);
00380
00381 if (congruences_are_minimized()) {
00382
00383 gr.simplify(gr.gen_sys, gr.dim_kinds);
00384 gr.set_generators_minimized();
00385 }
00386 else {
00387 #ifndef NDEBUG
00388
00389
00390 bool empty = simplify(gr.con_sys, gr.dim_kinds);
00391 assert(!empty);
00392 #else
00393 simplify(gr.con_sys, gr.dim_kinds);
00394 #endif
00395 gr.set_congruences_minimized();
00396 if (!generators_are_minimized()) {
00397
00398 gr.simplify(gr.gen_sys, gr.dim_kinds);
00399 gr.set_generators_minimized();
00400 }
00401 }
00402 }
00403 else {
00404
00405 const bool ret = update_generators();
00406 assert(OK());
00407 return ret;
00408 }
00409 }
00410 else {
00411 assert(generators_are_up_to_date());
00412 update_congruences();
00413 }
00414 assert(OK());
00415 return true;
00416 }
00417
00418 void
00419 PPL::Grid::normalize_divisors(Grid_Generator_System& sys,
00420 Grid_Generator_System& gen_sys) {
00421 dimension_type row = 0;
00422 dimension_type num_rows = gen_sys.num_generators();
00423
00424 while (gen_sys[row].is_line_or_parameter())
00425 if (++row == num_rows)
00426
00427
00428 throw std::runtime_error("PPL::Grid::normalize_divisors(sys, gen_sys).");
00429 Grid_Generator& first_point = gen_sys[row];
00430 Coefficient_traits::const_reference gen_sys_divisor = first_point.divisor();
00431 Coefficient divisor = normalize_divisors(sys, gen_sys_divisor);
00432 if (divisor != gen_sys_divisor)
00433
00434
00435
00436 normalize_divisors(gen_sys, divisor, &first_point);
00437 }
00438
00439 PPL::Coefficient
00440 PPL::Grid::normalize_divisors(Grid_Generator_System& sys,
00441 Coefficient_traits::const_reference divisor,
00442 Grid_Generator* first_point) {
00443 assert(divisor >= 0);
00444 if (sys.space_dimension() > 0 && divisor > 0) {
00445 TEMP_INTEGER(lcm);
00446 lcm = divisor;
00447
00448 dimension_type row = 0;
00449 dimension_type num_rows = sys.num_generators();
00450
00451 if (first_point)
00452 lcm_assign(lcm, lcm, (*first_point).divisor());
00453 else {
00454
00455 while (sys[row].is_line())
00456 if (++row == num_rows)
00457
00458 return divisor;
00459
00460
00461
00462 while (row < num_rows) {
00463 Grid_Generator& g = sys[row];
00464 if (g.is_parameter_or_point())
00465 lcm_assign(lcm, lcm, g.divisor());
00466 ++row;
00467 }
00468 }
00469
00470
00471
00472 for (dimension_type row = 0; row < num_rows; ++row)
00473 sys[row].scale_to_divisor(lcm);
00474
00475 return lcm;
00476 }
00477 return divisor;
00478 }
00479
00480 void
00481 PPL::Grid::throw_runtime_error(const char* method) const {
00482 std::ostringstream s;
00483 s << "PPL::Grid::" << method << "." << std::endl;
00484 throw std::runtime_error(s.str());
00485 }
00486
00487 void
00488 PPL::Grid::throw_invalid_argument(const char* method,
00489 const char* reason) const {
00490 std::ostringstream s;
00491 s << "PPL::Grid::" << method << ":" << std::endl
00492 << reason << ".";
00493 throw std::invalid_argument(s.str());
00494 }
00495
00496 void
00497 PPL::Grid::throw_dimension_incompatible(const char* method,
00498 const char* other_name,
00499 dimension_type other_dim) const {
00500 std::ostringstream s;
00501 s << "PPL::Grid::" << method << ":\n"
00502 << "this->space_dimension() == " << space_dimension() << ", "
00503 << other_name << ".space_dimension() == " << other_dim << ".";
00504 throw std::invalid_argument(s.str());
00505 }
00506
00507 void
00508 PPL::Grid::throw_dimension_incompatible(const char* method,
00509 const char* gr_name,
00510 const Grid& gr) const {
00511 throw_dimension_incompatible(method, gr_name, gr.space_dimension());
00512 }
00513
00514 void
00515 PPL::Grid::throw_dimension_incompatible(const char* method,
00516 const char* e_name,
00517 const Linear_Expression& e) const {
00518 throw_dimension_incompatible(method, e_name, e.space_dimension());
00519 }
00520
00521 void
00522 PPL::Grid::throw_dimension_incompatible(const char* method,
00523 const char* cg_name,
00524 const Congruence& cg) const {
00525 throw_dimension_incompatible(method, cg_name, cg.space_dimension());
00526 }
00527
00528 void
00529 PPL::Grid::throw_dimension_incompatible(const char* method,
00530 const char* c_name,
00531 const Constraint& c) const {
00532 throw_dimension_incompatible(method, c_name, c.space_dimension());
00533 }
00534
00535 void
00536 PPL::Grid::throw_dimension_incompatible(const char* method,
00537 const char* g_name,
00538 const Grid_Generator& g) const {
00539 throw_dimension_incompatible(method, g_name, g.space_dimension());
00540 }
00541
00542 void
00543 PPL::Grid::throw_dimension_incompatible(const char* method,
00544 const char* cgs_name,
00545 const Congruence_System& cgs) const {
00546 throw_dimension_incompatible(method, cgs_name, cgs.space_dimension());
00547 }
00548
00549 void
00550 PPL::Grid::throw_dimension_incompatible(const char* method,
00551 const char* cs_name,
00552 const Constraint_System& cs) const {
00553 throw_dimension_incompatible(method, cs_name, cs.space_dimension());
00554 }
00555
00556 void
00557 PPL::Grid::throw_dimension_incompatible(const char* method,
00558 const char* gs_name,
00559 const Grid_Generator_System& gs) const {
00560 throw_dimension_incompatible(method, gs_name, gs.space_dimension());
00561 }
00562
00563 void
00564 PPL::Grid::throw_dimension_incompatible(const char* method,
00565 const char* var_name,
00566 const Variable var) const {
00567 std::ostringstream s;
00568 s << "PPL::Grid::" << method << ":" << std::endl
00569 << "this->space_dimension() == " << space_dimension() << ", "
00570 << var_name << ".space_dimension() == " << var.space_dimension() << ".";
00571 throw std::invalid_argument(s.str());
00572 }
00573
00574 void
00575 PPL::Grid::
00576 throw_dimension_incompatible(const char* method,
00577 dimension_type required_space_dim) const {
00578 std::ostringstream s;
00579 s << "PPL::Grid::" << method << ":" << std::endl
00580 << "this->space_dimension() == " << space_dimension()
00581 << ", required space dimension == " << required_space_dim << ".";
00582 throw std::invalid_argument(s.str());
00583 }
00584
00585 void
00586 PPL::Grid::throw_space_dimension_overflow(const char* method,
00587 const char* reason) {
00588 std::ostringstream s;
00589 s << "PPL::Grid::" << method << ":" << std::endl
00590 << reason << ".";
00591 throw std::length_error(s.str());
00592 }
00593
00594 void
00595 PPL::Grid::throw_invalid_generator(const char* method,
00596 const char* g_name) const {
00597 std::ostringstream s;
00598 s << "PPL::Grid::" << method << ":" << std::endl
00599 << "*this is an empty grid and "
00600 << g_name << " is not a point.";
00601 throw std::invalid_argument(s.str());
00602 }
00603
00604 void
00605 PPL::Grid::throw_invalid_generators(const char* method,
00606 const char* gs_name) const {
00607 std::ostringstream s;
00608 s << "PPL::Grid::" << method << ":" << std::endl
00609 << "*this is an empty grid and" << std::endl
00610 << "the non-empty generator system " << gs_name << " contains no points.";
00611 throw std::invalid_argument(s.str());
00612 }