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 #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 // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
00046 #define BE_LAZY 1
00047
00048 namespace PPL = Parma_Polyhedra_Library;
00049
00050 void
00051 PPL::Grid::construct(dimension_type num_dimensions,
00052 const Degenerate_Element kind) {
00053 space_dim = num_dimensions;
00054
00055 if (kind == EMPTY) {
00056
00057
00058
00059 status.set_empty();
00060
00061
00062
00063 Congruence_System cgs(Congruence::zero_dim_false());
00064 cgs.increase_space_dimension(space_dim);
00065 const_cast<Congruence_System&>(con_sys).swap(cgs);
00066
00067 assert(OK());
00068 return;
00069 }
00070
00071 if (num_dimensions > 0) {
00072 con_sys.increase_space_dimension(num_dimensions);
00073
00074
00075
00076 set_congruences_minimized();
00077 set_generators_minimized();
00078 dim_kinds.resize(num_dimensions + 1);
00079
00080
00081
00082 Congruence_System cgs(Congruence::zero_dim_integrality());
00083 cgs.increase_space_dimension(space_dim);
00084 cgs[0][0] = 1;
00085 con_sys.swap(cgs);
00086
00087 dim_kinds[0] = PROPER_CONGRUENCE ;
00088
00089
00090 gen_sys.insert(grid_point(0*(Variable(0))));
00091
00092
00093 dimension_type dim = 0;
00094 while (dim < num_dimensions) {
00095 gen_sys.insert(grid_line(Variable(dim)));
00096 dim_kinds[++dim] = CON_VIRTUAL ;
00097 }
00098 }
00099 else
00100 set_zero_dim_univ();
00101 }
00102
00103 void
00104 PPL::Grid::construct(Congruence_System& cgs) {
00105
00106 assert(cgs.space_dimension() <= max_space_dimension());
00107
00108 assert(cgs.space_dimension() == con_sys.space_dimension());
00109 assert(cgs.space_dimension() == gen_sys.space_dimension());
00110 assert(con_sys.has_no_rows());
00111 assert(gen_sys.has_no_rows());
00112
00113
00114 space_dim = cgs.space_dimension();
00115
00116 if (space_dim > 0) {
00117
00118 std::swap(con_sys, cgs);
00119 con_sys.normalize_moduli();
00120 set_congruences_up_to_date();
00121 }
00122 else {
00123
00124 if (cgs.num_columns() > 1)
00125
00126 for (dimension_type i = cgs.num_rows(); i-- > 0; )
00127 if (cgs[i].is_inconsistent()) {
00128
00129 status.set_empty();
00130
00131
00132 con_sys.insert(Congruence::zero_dim_false());
00133 assert(OK());
00134 return;
00135 }
00136 set_zero_dim_univ();
00137 }
00138 assert(OK());
00139 }
00140
00141 void
00142 PPL::Grid::construct(Grid_Generator_System& ggs) {
00143
00144 assert(ggs.space_dimension() <= max_space_dimension());
00145
00146 assert(ggs.space_dimension() == con_sys.space_dimension());
00147 assert(ggs.space_dimension() == gen_sys.space_dimension());
00148 assert(con_sys.has_no_rows());
00149 assert(gen_sys.has_no_rows());
00150
00151
00152 space_dim = ggs.space_dimension();
00153
00154
00155 if (ggs.has_no_rows()) {
00156 status.set_empty();
00157
00158
00159 con_sys.insert(Congruence::zero_dim_false());
00160 return;
00161 }
00162
00163
00164 if (!ggs.has_points())
00165 throw_invalid_generators("Grid(ggs)", "ggs");
00166
00167 if (space_dim == 0)
00168 set_zero_dim_univ();
00169 else {
00170
00171 std::swap(gen_sys, ggs);
00172 normalize_divisors(gen_sys);
00173
00174 set_generators_up_to_date();
00175 }
00176
00177 assert(OK());
00178 }
00179
00180 PPL::Grid::Three_Valued_Boolean
00181 PPL::Grid::quick_equivalence_test(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 bool css_normalized = false;
00189
00190 if (x.congruences_are_minimized() && y.congruences_are_minimized()) {
00191
00192
00193 if (x.con_sys.num_rows() != y.con_sys.num_rows())
00194 return Grid::TVB_FALSE;
00195
00196 dimension_type x_num_equalities = x.con_sys.num_equalities();
00197 if (x_num_equalities != y.con_sys.num_equalities())
00198 return Grid::TVB_FALSE;
00199
00200
00201 css_normalized = (x_num_equalities == 0);
00202 }
00203
00204 if (x.generators_are_minimized() && y.generators_are_minimized()) {
00205
00206
00207 if (x.gen_sys.num_rows() != y.gen_sys.num_rows())
00208 return Grid::TVB_FALSE;
00209
00210 const dimension_type x_num_lines = x.gen_sys.num_lines();
00211 if (x_num_lines != y.gen_sys.num_lines())
00212 return Grid::TVB_FALSE;
00213
00214 if (x_num_lines == 0) {
00215
00216 if (x.gen_sys == y.gen_sys)
00217 return Grid::TVB_TRUE;
00218 else
00219 return Grid::TVB_FALSE;
00220 }
00221 }
00222
00223
00224
00225
00226 if (css_normalized) {
00227 if (x.con_sys == y.con_sys)
00228 return Grid::TVB_TRUE;
00229 else
00230 return Grid::TVB_FALSE;
00231 }
00232
00233 return Grid::TVB_DONT_KNOW;
00234 }
00235
00236 bool
00237 PPL::Grid::is_included_in(const Grid& y) const {
00238
00239 assert(space_dim == y.space_dim);
00240 assert(!marked_empty() && !y.marked_empty() && space_dim > 0);
00241
00242 const Grid& x = *this;
00243
00244 #if BE_LAZY
00245 if (!x.generators_are_up_to_date() && !x.update_generators())
00246
00247 return true;
00248 if (!y.congruences_are_up_to_date())
00249 y.update_congruences();
00250 #else
00251 if (!x.generators_are_minimized() && !x.minimize())
00252
00253 return true;
00254 if (!y.congruences_are_minimized())
00255 y.minimize();
00256 #endif
00257
00258 assert(x.OK());
00259 assert(y.OK());
00260
00261 const Grid_Generator_System& gs = x.gen_sys;
00262 const Congruence_System& cgs = y.con_sys;
00263
00264 dimension_type num_rows = gs.num_rows();
00265 for (dimension_type i = num_rows; i-- > 0; )
00266 if (!cgs.satisfies_all_congruences(gs[i]))
00267 return false;
00268
00269
00270 return true;
00271 }
00272
00273 bool
00274 PPL::Grid::bounds(const Linear_Expression& expr,
00275 const char* method_call) const {
00276
00277 if (space_dim < expr.space_dimension())
00278 throw_dimension_incompatible(method_call, "e", expr);
00279
00280
00281 if (space_dim == 0
00282 || marked_empty()
00283 || (!generators_are_up_to_date() && !update_generators()))
00284 return true;
00285
00286
00287 for (dimension_type i = gen_sys.num_rows(); i-- > 0; ) {
00288 const Grid_Generator& g = gen_sys[i];
00289
00290
00291 if (g.is_line_or_parameter()) {
00292 const int sp_sign = Scalar_Products::homogeneous_sign(expr, g);
00293 if (sp_sign != 0)
00294
00295 return false;
00296 }
00297 }
00298 return true;
00299 }
00300
00301 bool
00302 PPL::Grid::max_min(const Linear_Expression& expr,
00303 const char* method_call,
00304 Coefficient& ext_n, Coefficient& ext_d, bool& included,
00305 Generator* point) const {
00306 if (bounds(expr, method_call)) {
00307 if (marked_empty())
00308 return false;
00309 if (space_dim == 0) {
00310 ext_n = 0;
00311 ext_d = 1;
00312 included = true;
00313 if (point)
00314 *point = Generator::point();
00315 return true;
00316 }
00317
00318 if (!generators_are_minimized()) {
00319
00320 Grid& gr = const_cast<Grid&>(*this);
00321 gr.simplify(gr.gen_sys, gr.dim_kinds);
00322 gr.set_generators_minimized();
00323 }
00324
00325 const Grid_Generator& gen = gen_sys[0];
00326 Scalar_Products::homogeneous_assign(ext_n, expr, gen);
00327 ext_n += expr.inhomogeneous_term();
00328 ext_d = gen.divisor();
00329
00330 TEMP_INTEGER(gcd);
00331 gcd_assign(gcd, ext_n, ext_d);
00332 exact_div_assign(ext_n, ext_n, gcd);
00333 exact_div_assign(ext_d, ext_d, gcd);
00334
00335 included = true;
00336 if (point) {
00337 Linear_Expression e;
00338 for (dimension_type i = space_dim; i-- > 0; )
00339 e += gen.coefficient(Variable(i)) * Variable(i);
00340 *point = Generator::point(e, gen.divisor());
00341 }
00342 return true;
00343 }
00344 return false;
00345 }
00346
00347 void
00348 PPL::Grid::set_zero_dim_univ() {
00349 status.set_zero_dim_univ();
00350 space_dim = 0;
00351 con_sys.clear();
00352 gen_sys.clear();
00353 gen_sys.insert(grid_point());
00354 }
00355
00356 void
00357 PPL::Grid::set_empty() {
00358 status.set_empty();
00359
00360
00361 Grid_Generator_System gs(space_dim);
00362 gen_sys.swap(gs);
00363
00364
00365
00366 Congruence_System cgs(Congruence::zero_dim_false());
00367 cgs.increase_space_dimension(space_dim);
00368 const_cast<Congruence_System&>(con_sys).swap(cgs);
00369 }
00370
00371 void
00372 PPL::Grid::update_congruences() const {
00373
00374 assert(space_dim > 0);
00375 assert(!marked_empty());
00376 assert(!gen_sys.has_no_rows());
00377 assert(gen_sys.space_dimension() > 0);
00378
00379 Grid& gr = const_cast<Grid&>(*this);
00380
00381 if (!generators_are_minimized())
00382 gr.simplify(gr.gen_sys, gr.dim_kinds);
00383
00384
00385
00386 assert(!gen_sys.has_no_rows());
00387
00388
00389
00390 gr.conversion(gr.gen_sys, gr.con_sys, gr.dim_kinds);
00391
00392
00393 gr.set_congruences_minimized();
00394 gr.set_generators_minimized();
00395 }
00396
00397 bool
00398 PPL::Grid::update_generators() const {
00399 assert(space_dim > 0);
00400 assert(!marked_empty());
00401 assert(congruences_are_up_to_date());
00402
00403 Grid& x = const_cast<Grid&>(*this);
00404
00405 if (!congruences_are_minimized())
00406
00407
00408 if (simplify(x.con_sys, x.dim_kinds)) {
00409 x.set_empty();
00410 return false;
00411 }
00412
00413
00414
00415 conversion(x.con_sys, x.gen_sys, x.dim_kinds);
00416
00417
00418 x.set_congruences_minimized();
00419 x.set_generators_minimized();
00420 return true;
00421 }
00422
00423 bool
00424 PPL::Grid::minimize() const {
00425
00426 if (marked_empty())
00427 return false;
00428 if (space_dim == 0)
00429 return true;
00430
00431
00432 if (congruences_are_minimized() && generators_are_minimized())
00433 return true;
00434
00435
00436
00437 if (congruences_are_up_to_date()) {
00438 if (generators_are_up_to_date()) {
00439 Grid& gr = const_cast<Grid&>(*this);
00440
00441 if (congruences_are_minimized()) {
00442
00443 gr.simplify(gr.gen_sys, gr.dim_kinds);
00444 gr.set_generators_minimized();
00445 }
00446 else {
00447 #ifndef NDEBUG
00448
00449
00450 bool empty = simplify(gr.con_sys, gr.dim_kinds);
00451 assert(!empty);
00452 #else
00453 simplify(gr.con_sys, gr.dim_kinds);
00454 #endif
00455 gr.set_congruences_minimized();
00456 if (!generators_are_minimized()) {
00457
00458 gr.simplify(gr.gen_sys, gr.dim_kinds);
00459 gr.set_generators_minimized();
00460 }
00461 }
00462 }
00463 else {
00464
00465 const bool ret = update_generators();
00466 assert(OK());
00467 return ret;
00468 }
00469 }
00470 else {
00471 assert(generators_are_up_to_date());
00472 update_congruences();
00473 }
00474 assert(OK());
00475 return true;
00476 }
00477
00478 void
00479 PPL::Grid::normalize_divisors(Grid_Generator_System& sys,
00480 Grid_Generator_System& gen_sys) {
00481 #ifndef NDEBUG
00482 const dimension_type num_rows = gen_sys.num_rows();
00483 #endif
00484 assert(num_rows > 0);
00485
00486
00487 dimension_type row = 0;
00488 while (gen_sys[row].is_line_or_parameter()) {
00489 ++row;
00490
00491 assert(row < num_rows);
00492 }
00493 Grid_Generator& first_point = gen_sys[row];
00494 const Coefficient& gen_sys_divisor = first_point.divisor();
00495
00496 #ifndef NDEBUG
00497
00498 for (dimension_type i = row + 1; i < num_rows; ++i) {
00499 Grid_Generator& g = gen_sys[i];
00500 if (g.is_parameter_or_point())
00501 assert(gen_sys_divisor == g.divisor());
00502 }
00503 #endif // !defined(NDEBUG)
00504
00505 TEMP_INTEGER(divisor);
00506 divisor = gen_sys_divisor;
00507
00508 normalize_divisors(sys, divisor);
00509 if (divisor != gen_sys_divisor)
00510
00511
00512
00513
00514
00515 normalize_divisors(gen_sys, divisor, &first_point);
00516 }
00517
00518 void
00519 PPL::Grid::normalize_divisors(Grid_Generator_System& sys,
00520 Coefficient& divisor,
00521 const Grid_Generator* first_point) {
00522 assert(divisor >= 0);
00523 if (sys.space_dimension() > 0 && divisor > 0) {
00524 dimension_type row = 0;
00525 dimension_type num_rows = sys.num_rows();
00526
00527 if (first_point)
00528 lcm_assign(divisor, divisor, (*first_point).divisor());
00529 else {
00530 assert(num_rows > 0);
00531
00532 while (sys[row].is_line())
00533 if (++row == num_rows)
00534
00535 return;
00536
00537
00538
00539 while (row < num_rows) {
00540 const Grid_Generator& g = sys[row];
00541 if (g.is_parameter_or_point())
00542 lcm_assign(divisor, divisor, g.divisor());
00543 ++row;
00544 }
00545 }
00546
00547
00548
00549 for (row = num_rows; row-- > 0; )
00550 sys[row].scale_to_divisor(divisor);
00551 }
00552 }
00553
00554 void
00555 PPL::Grid::add_congruence_no_check(const Congruence& cg) {
00556 assert(!marked_empty());
00557 assert(space_dim >= cg.space_dimension());
00558
00559
00560 if (space_dim == 0) {
00561 if (cg.is_inconsistent())
00562 set_empty();
00563 return;
00564 }
00565
00566 if (!congruences_are_up_to_date())
00567 update_congruences();
00568
00569 con_sys.insert(cg);
00570
00571 clear_congruences_minimized();
00572 set_congruences_up_to_date();
00573 clear_generators_up_to_date();
00574
00575
00576
00577 assert(OK());
00578 }
00579
00580 void
00581 PPL::Grid::add_constraint_no_check(const Constraint& c) {
00582 assert(!marked_empty());
00583 assert(space_dim >= c.space_dimension());
00584
00585 if (c.is_inequality()) {
00586
00587 if (c.is_inconsistent()) {
00588 set_empty();
00589 return;
00590 }
00591 if (c.is_tautological())
00592 return;
00593
00594 throw_invalid_constraint("add_constraint(c)", "c");
00595 }
00596
00597 assert(c.is_equality());
00598 Congruence cg(c);
00599 add_congruence_no_check(cg);
00600 }
00601
00602 void
00603 PPL::Grid::refine_no_check(const Constraint& c) {
00604 assert(!marked_empty());
00605 assert(space_dim >= c.space_dimension());
00606
00607 if (c.is_equality()) {
00608 Congruence cg(c);
00609 add_congruence_no_check(cg);
00610 }
00611 else if (c.is_inconsistent())
00612 set_empty();
00613 }
00614
00615 void
00616 PPL::Grid::throw_runtime_error(const char* method) const {
00617 std::ostringstream s;
00618 s << "PPL::Grid::" << method << "." << std::endl;
00619 throw std::runtime_error(s.str());
00620 }
00621
00622 void
00623 PPL::Grid::throw_invalid_argument(const char* method,
00624 const char* reason) const {
00625 std::ostringstream s;
00626 s << "PPL::Grid::" << method << ":" << std::endl
00627 << reason << ".";
00628 throw std::invalid_argument(s.str());
00629 }
00630
00631 void
00632 PPL::Grid::throw_dimension_incompatible(const char* method,
00633 const char* other_name,
00634 dimension_type other_dim) const {
00635 std::ostringstream s;
00636 s << "PPL::Grid::" << method << ":\n"
00637 << "this->space_dimension() == " << space_dimension() << ", "
00638 << other_name << ".space_dimension() == " << other_dim << ".";
00639 throw std::invalid_argument(s.str());
00640 }
00641
00642 void
00643 PPL::Grid::throw_dimension_incompatible(const char* method,
00644 const char* gr_name,
00645 const Grid& gr) const {
00646 throw_dimension_incompatible(method, gr_name, gr.space_dimension());
00647 }
00648
00649 void
00650 PPL::Grid::throw_dimension_incompatible(const char* method,
00651 const char* e_name,
00652 const Linear_Expression& e) const {
00653 throw_dimension_incompatible(method, e_name, e.space_dimension());
00654 }
00655
00656 void
00657 PPL::Grid::throw_dimension_incompatible(const char* method,
00658 const char* cg_name,
00659 const Congruence& cg) const {
00660 throw_dimension_incompatible(method, cg_name, cg.space_dimension());
00661 }
00662
00663 void
00664 PPL::Grid::throw_dimension_incompatible(const char* method,
00665 const char* c_name,
00666 const Constraint& c) const {
00667 throw_dimension_incompatible(method, c_name, c.space_dimension());
00668 }
00669
00670 void
00671 PPL::Grid::throw_dimension_incompatible(const char* method,
00672 const char* g_name,
00673 const Grid_Generator& g) const {
00674 throw_dimension_incompatible(method, g_name, g.space_dimension());
00675 }
00676
00677 void
00678 PPL::Grid::throw_dimension_incompatible(const char* method,
00679 const char* g_name,
00680 const Generator& g) const {
00681 throw_dimension_incompatible(method, g_name, g.space_dimension());
00682 }
00683
00684 void
00685 PPL::Grid::throw_dimension_incompatible(const char* method,
00686 const char* cgs_name,
00687 const Congruence_System& cgs) const {
00688 throw_dimension_incompatible(method, cgs_name, cgs.space_dimension());
00689 }
00690
00691 void
00692 PPL::Grid::throw_dimension_incompatible(const char* method,
00693 const char* cs_name,
00694 const Constraint_System& cs) const {
00695 throw_dimension_incompatible(method, cs_name, cs.space_dimension());
00696 }
00697
00698 void
00699 PPL::Grid::throw_dimension_incompatible(const char* method,
00700 const char* gs_name,
00701 const Grid_Generator_System& gs) const {
00702 throw_dimension_incompatible(method, gs_name, gs.space_dimension());
00703 }
00704
00705 void
00706 PPL::Grid::throw_dimension_incompatible(const char* method,
00707 const char* var_name,
00708 const Variable var) const {
00709 std::ostringstream s;
00710 s << "PPL::Grid::" << method << ":" << std::endl
00711 << "this->space_dimension() == " << space_dimension() << ", "
00712 << var_name << ".space_dimension() == " << var.space_dimension() << ".";
00713 throw std::invalid_argument(s.str());
00714 }
00715
00716 void
00717 PPL::Grid::
00718 throw_dimension_incompatible(const char* method,
00719 dimension_type required_space_dim) const {
00720 std::ostringstream s;
00721 s << "PPL::Grid::" << method << ":" << std::endl
00722 << "this->space_dimension() == " << space_dimension()
00723 << ", required space dimension == " << required_space_dim << ".";
00724 throw std::invalid_argument(s.str());
00725 }
00726
00727 void
00728 PPL::Grid::throw_space_dimension_overflow(const char* method,
00729 const char* reason) {
00730 std::ostringstream s;
00731 s << "PPL::Grid::" << method << ":" << std::endl
00732 << reason << ".";
00733 throw std::length_error(s.str());
00734 }
00735
00736 void
00737 PPL::Grid::throw_invalid_constraint(const char* method,
00738 const char* c_name) const {
00739 std::ostringstream s;
00740 s << "PPL::Grid::" << method << ":" << std::endl
00741 << c_name << " is not an equality constraint.";
00742 throw std::invalid_argument(s.str());
00743 }
00744
00745 void
00746 PPL::Grid::throw_invalid_constraints(const char* method,
00747 const char* cs_name) const {
00748 std::ostringstream s;
00749 s << "PPL::Grid::" << method << ":" << std::endl
00750 << "the constraint system " << cs_name
00751 << " contains inequalities.";
00752 throw std::invalid_argument(s.str());
00753 }
00754
00755 void
00756 PPL::Grid::throw_invalid_generator(const char* method,
00757 const char* g_name) const {
00758 std::ostringstream s;
00759 s << "PPL::Grid::" << method << ":" << std::endl
00760 << "*this is an empty grid and "
00761 << g_name << " is not a point.";
00762 throw std::invalid_argument(s.str());
00763 }
00764
00765 void
00766 PPL::Grid::throw_invalid_generators(const char* method,
00767 const char* gs_name) const {
00768 std::ostringstream s;
00769 s << "PPL::Grid::" << method << ":" << std::endl
00770 << "*this is an empty grid and" << std::endl
00771 << "the non-empty generator system " << gs_name << " contains no points.";
00772 throw std::invalid_argument(s.str());
00773 }