00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023 #include <config.h>
00024
00025 #include "Grid.defs.hh"
00026 #include "Topology.hh"
00027 #include "Scalar_Products.defs.hh"
00028
00029 #include <cassert>
00030 #include <iostream>
00031
00032 namespace PPL = Parma_Polyhedra_Library;
00033
00034 PPL::Grid::Grid(dimension_type num_dimensions,
00035 const Degenerate_Element kind)
00036 : con_sys(),
00037 gen_sys(num_dimensions > max_space_dimension()
00038 ? (throw_space_dimension_overflow("Grid(n, k)",
00039 "n exceeds the maximum "
00040 "allowed space dimension"),
00041 0)
00042 : num_dimensions) {
00043
00044 space_dim = num_dimensions;
00045
00046 if (kind == EMPTY) {
00047
00048
00049
00050 status.set_empty();
00051
00052
00053
00054 Congruence_System cgs(Congruence::zero_dim_false());
00055 cgs.increase_space_dimension(space_dim);
00056 const_cast<Congruence_System&>(con_sys).swap(cgs);
00057
00058 assert(OK());
00059 return;
00060 }
00061
00062 if (num_dimensions > 0) {
00063 con_sys.increase_space_dimension(num_dimensions);
00064
00065
00066
00067 set_congruences_minimized();
00068 set_generators_minimized();
00069 dim_kinds.resize(num_dimensions + 1);
00070
00071
00072
00073 Congruence_System cgs(Congruence::zero_dim_integrality());
00074 cgs.increase_space_dimension(space_dim);
00075 cgs[0][0] = 1;
00076 con_sys.swap(cgs);
00077
00078 dim_kinds[0] = PROPER_CONGRUENCE ;
00079
00080
00081 gen_sys.insert(grid_point(0*(Variable(0))));
00082
00083
00084 dimension_type dim = 0;
00085 while (dim < num_dimensions) {
00086 gen_sys.insert(grid_line(Variable(dim++)));
00087 dim_kinds[dim] = CON_VIRTUAL ;
00088 }
00089 }
00090 else
00091 set_zero_dim_univ();
00092
00093 assert(OK());
00094 }
00095
00096 PPL::Grid::Grid(const Grid& y)
00097 : con_sys(),
00098 gen_sys(),
00099 status(y.status),
00100 space_dim(y.space_dim),
00101 dim_kinds(y.dim_kinds) {
00102 if (space_dim == 0) {
00103 con_sys = y.con_sys;
00104 gen_sys = y.gen_sys;
00105 }
00106 else {
00107 if (y.congruences_are_up_to_date())
00108 con_sys = y.con_sys;
00109 else
00110 con_sys.increase_space_dimension(space_dim);
00111 if (y.generators_are_up_to_date())
00112 gen_sys = y.gen_sys;
00113 else
00114 gen_sys = Grid_Generator_System(y.space_dim);
00115 }
00116 }
00117
00118 PPL::Grid::Grid(const Constraint_System& ccs) {
00119 if (ccs.space_dimension() > max_space_dimension())
00120 throw_space_dimension_overflow("Grid(ccs)",
00121 "the space dimension of ccs "
00122 "exceeds the maximum allowed "
00123 "space dimension");
00124 Congruence_System cgs;
00125 cgs.insert(0*Variable(ccs.space_dimension() - 1) %= 1);
00126 for (Constraint_System::const_iterator i = ccs.begin(),
00127 ccs_end = ccs.end(); i != ccs_end; ++i)
00128 if (i->is_equality())
00129 cgs.insert(*i);
00130 construct(cgs);
00131 }
00132
00133 PPL::Grid::Grid(Constraint_System& cs) {
00134 if (cs.space_dimension() > max_space_dimension())
00135 throw_space_dimension_overflow("Grid(cs)",
00136 "the space dimension of cs "
00137 "exceeds the maximum allowed "
00138 "space dimension");
00139
00140 Congruence_System cgs;
00141 cgs.insert(0*Variable(cs.space_dimension() - 1) %= 1);
00142 for (Constraint_System::const_iterator i = cs.begin(),
00143 cs_end = cs.end(); i != cs_end; ++i)
00144 if (i->is_equality())
00145 cgs.insert(*i);
00146 construct(cgs);
00147 }
00148
00149 PPL::Grid&
00150 PPL::Grid::operator=(const Grid& y) {
00151 space_dim = y.space_dim;
00152 dim_kinds = y.dim_kinds;
00153 if (y.marked_empty())
00154 set_empty();
00155 else if (space_dim == 0)
00156 set_zero_dim_univ();
00157 else {
00158 status = y.status;
00159 if (y.congruences_are_up_to_date())
00160 con_sys = y.con_sys;
00161 if (y.generators_are_up_to_date())
00162 gen_sys = y.gen_sys;
00163 }
00164 return *this;
00165 }
00166
00167 PPL::dimension_type
00168 PPL::Grid::affine_dimension() const {
00169 if (space_dim == 0 || is_empty())
00170 return 0;
00171
00172
00173
00174
00175 const Congruence_System& cgs = minimized_congruences();
00176 dimension_type d = space_dim;
00177 for (dimension_type i = cgs.num_rows(); i-- > 0; )
00178 if (cgs[i].is_equality())
00179 --d;
00180 return d;
00181 }
00182
00183 const PPL::Congruence_System&
00184 PPL::Grid::congruences() const {
00185 if (marked_empty())
00186 return con_sys;
00187
00188 if (space_dim == 0) {
00189
00190 assert(con_sys.num_columns() == 2 && con_sys.num_rows() == 0);
00191 return con_sys;
00192 }
00193
00194 congruences_are_up_to_date() || update_congruences();
00195
00196 return con_sys;
00197 }
00198
00199 const PPL::Congruence_System&
00200 PPL::Grid::minimized_congruences() const {
00201 if (space_dim == 0) {
00202 if (!marked_empty()) {
00203
00204
00205
00206 Congruence_System cgs(Congruence::zero_dim_integrality());
00207 cgs.increase_space_dimension(space_dim);
00208 cgs[0][0] = 1;
00209 const_cast<Congruence_System&>(con_sys).swap(cgs);
00210 }
00211 return con_sys;
00212 }
00213 if (congruences_are_up_to_date() && !congruences_are_minimized()) {
00214
00215 Grid& gr = const_cast<Grid&>(*this);
00216 if (gr.simplify(gr.con_sys, gr.dim_kinds))
00217 gr.set_empty();
00218 else
00219 gr.set_congruences_minimized();
00220 }
00221 return congruences();
00222 }
00223
00224 const PPL::Grid_Generator_System&
00225 PPL::Grid::generators() const {
00226 if (space_dim == 0) {
00227 assert(gen_sys.space_dimension() == 0
00228 && gen_sys.num_generators() == (marked_empty() ? 0 : 1));
00229 return gen_sys;
00230 }
00231
00232 if (marked_empty()) {
00233 assert(gen_sys.num_generators() == 0);
00234 return gen_sys;
00235 }
00236
00237 if (!generators_are_up_to_date() && !update_generators()) {
00238
00239 const_cast<Grid&>(*this).set_empty();
00240 return gen_sys;
00241 }
00242
00243 return gen_sys;
00244 }
00245
00246 const PPL::Grid_Generator_System&
00247 PPL::Grid::minimized_generators() const {
00248 if (space_dim == 0) {
00249 assert(gen_sys.space_dimension() == 0
00250 && gen_sys.num_generators() == (marked_empty() ? 0 : 1));
00251 return gen_sys;
00252 }
00253
00254 if (marked_empty()) {
00255 assert(gen_sys.num_generators() == 0);
00256 return gen_sys;
00257 }
00258
00259 if (generators_are_up_to_date()) {
00260 if (!generators_are_minimized()) {
00261
00262 Grid& gr = const_cast<Grid&>(*this);
00263 gr.simplify(gr.gen_sys, gr.dim_kinds);
00264 gr.set_generators_minimized();
00265 }
00266 }
00267 else if (!update_generators()) {
00268
00269 const_cast<Grid&>(*this).set_empty();
00270 return gen_sys;
00271 }
00272
00273 return gen_sys;
00274 }
00275
00276 PPL::Poly_Con_Relation
00277 PPL::Grid::relation_with(const Congruence& cg) const {
00278
00279 if (space_dim < cg.space_dimension())
00280 throw_dimension_incompatible("relation_with(cg)", "cg", cg);
00281
00282 if (marked_empty())
00283 return Poly_Con_Relation::is_included()
00284 && Poly_Con_Relation::is_disjoint();
00285
00286 if (space_dim == 0)
00287
00288
00289
00290 if (cg.inhomogeneous_term() == 0)
00291 return Poly_Con_Relation::is_included();
00292 else if (cg.is_equality())
00293 return Poly_Con_Relation::is_disjoint();
00294 else if (cg.inhomogeneous_term() % cg.modulus() == 0)
00295 return Poly_Con_Relation::is_included();
00296 else
00297
00298 return Poly_Con_Relation::is_disjoint();
00299
00300 if (!generators_are_up_to_date() && !update_generators())
00301
00302 return Poly_Con_Relation::is_included()
00303 && Poly_Con_Relation::is_disjoint();
00304
00305
00306
00307
00308
00309
00310
00311
00312
00313
00314 TEMP_INTEGER(point_sp);
00315 point_sp = 0;
00316
00317 TEMP_INTEGER(modulus);
00318 modulus = cg.modulus();
00319
00320 TEMP_INTEGER(div);
00321 div = 0;
00322
00323 bool known_to_intersect = false;
00324
00325 for (Grid_Generator_System::const_iterator g = gen_sys.begin(),
00326 gen_sys_end = gen_sys.end(); g != gen_sys_end; ++g) {
00327 TEMP_INTEGER(sp);
00328 Scalar_Products::assign(sp, cg, *g);
00329
00330 switch (g->type()) {
00331
00332 case Grid_Generator::POINT:
00333 if (cg.is_proper_congruence())
00334 sp %= modulus;
00335 if (sp == 0)
00336
00337 if (point_sp == 0)
00338
00339 known_to_intersect = true;
00340 else
00341 return Poly_Con_Relation::strictly_intersects();
00342 else
00343 if (point_sp == 0) {
00344 if (known_to_intersect)
00345 return Poly_Con_Relation::strictly_intersects();
00346
00347
00348 point_sp = sp;
00349 }
00350 else {
00351
00352
00353
00354
00355
00356 sp -= point_sp;
00357
00358 if (sp != 0) {
00359
00360 gcd_assign(div, div, sp);
00361 if (point_sp % div == 0)
00362
00363 return Poly_Con_Relation::strictly_intersects();
00364 }
00365 }
00366 break;
00367
00368 case Grid_Generator::PARAMETER:
00369 if (cg.is_proper_congruence())
00370 sp %= (modulus * g->divisor());
00371 if (sp == 0)
00372
00373
00374 break;
00375
00376 if (known_to_intersect)
00377
00378
00379 return Poly_Con_Relation::strictly_intersects();
00380
00381
00382 gcd_assign(div, div, sp);
00383 if (point_sp != 0)
00384
00385
00386 if (point_sp == div)
00387
00388 return Poly_Con_Relation::strictly_intersects();
00389
00390 break;
00391
00392 case Grid_Generator::LINE:
00393 if (sp == 0)
00394
00395
00396 break;
00397
00398
00399
00400
00401
00402
00403
00404
00405
00406
00407
00408
00409
00410
00411 return Poly_Con_Relation::strictly_intersects();
00412 }
00413 }
00414
00415 if (point_sp == 0)
00416
00417 return Poly_Con_Relation::is_included();
00418
00419 assert(!known_to_intersect);
00420 return Poly_Con_Relation::is_disjoint();
00421 }
00422
00423 PPL::Poly_Gen_Relation
00424 PPL::Grid::relation_with(const Grid_Generator& g) const {
00425
00426 if (space_dim < g.space_dimension())
00427 throw_dimension_incompatible("relation_with(g)", "g", g);
00428
00429
00430 if (marked_empty())
00431 return Poly_Gen_Relation::nothing();
00432
00433
00434
00435 if (space_dim == 0)
00436 return Poly_Gen_Relation::subsumes();
00437
00438 congruences_are_up_to_date() || update_congruences();
00439
00440 return
00441 con_sys.satisfies_all_congruences(g)
00442 ? Poly_Gen_Relation::subsumes()
00443 : Poly_Gen_Relation::nothing();
00444 }
00445
00446 bool
00447 PPL::Grid::is_empty() const {
00448 if (marked_empty())
00449 return true;
00450
00451
00452 if (generators_are_up_to_date())
00453 return false;
00454 if (space_dim == 0)
00455 return false;
00456 if (congruences_are_minimized())
00457
00458 return false;
00459
00460 Grid& gr = const_cast<Grid&>(*this);
00461 if (gr.simplify(gr.con_sys, gr.dim_kinds)) {
00462 gr.set_empty();
00463 return true;
00464 }
00465 gr.set_congruences_minimized();
00466 return false;
00467 }
00468
00469 bool
00470 PPL::Grid::is_universe() const {
00471 if (marked_empty())
00472 return false;
00473
00474 if (space_dim == 0)
00475 return true;
00476
00477 if (congruences_are_up_to_date()) {
00478 if (congruences_are_minimized())
00479
00480
00481 return con_sys.num_rows() == 1 && con_sys[0].is_trivial_true();
00482 }
00483 else {
00484 update_congruences();
00485 return con_sys.num_rows() == 1 && con_sys[0].is_trivial_true();
00486 }
00487
00488
00489
00490
00491 Variable var(space_dim - 1);
00492 for (dimension_type i = space_dim; i-- > 0; )
00493 if (!con_sys.satisfies_all_congruences(grid_line(Variable(i) + var)))
00494 return false;
00495 assert(con_sys.satisfies_all_congruences(grid_point(0*var)));
00496 return true;
00497 }
00498
00499 bool
00500 PPL::Grid::is_bounded() const {
00501
00502 if (space_dim == 0
00503 || marked_empty()
00504 || (!generators_are_up_to_date() && !update_generators()))
00505 return true;
00506
00507
00508
00509 if (gen_sys.num_generators() > 1) {
00510
00511 const Grid_Generator& first_point = gen_sys[0];
00512 if (first_point.is_line_or_parameter())
00513 return false;
00514 for (dimension_type row = gen_sys.num_generators(); row-- > 0; ) {
00515 const Grid_Generator& gen = gen_sys[row];
00516 if (gen.is_line_or_parameter() || gen != first_point)
00517 return false;
00518 }
00519 }
00520 return true;
00521 }
00522
00523 bool
00524 PPL::Grid::is_discrete() const {
00525
00526 if (space_dim == 0 || marked_empty())
00527 return true;
00528
00529 if (generators_are_minimized()) {
00530 line_search:
00531
00532 for (dimension_type row = gen_sys.num_generators(); row-- > 1; )
00533 if (gen_sys[row].is_line())
00534 return false;
00535 return true;
00536 }
00537
00538 if (congruences_are_minimized())
00539 return con_sys.has_a_free_dimension();
00540
00541 Grid& gr = const_cast<Grid&>(*this);
00542 if (generators_are_up_to_date()) {
00543
00544 gr.simplify(gr.gen_sys, gr.dim_kinds);
00545 gr.set_generators_minimized();
00546
00547 goto line_search;
00548 }
00549
00550
00551
00552
00553 if (gr.simplify(gr.con_sys, gr.dim_kinds)) {
00554
00555 gr.set_empty();
00556 return true;
00557 }
00558 gr.set_congruences_minimized();
00559
00560 return gr.con_sys.has_a_free_dimension();
00561 }
00562
00563 bool
00564 PPL::Grid::is_topologically_closed() const {
00565
00566 if (marked_empty() || space_dim == 0)
00567 return true;
00568
00569 if (generators_are_minimized()) {
00570 param_search:
00571
00572 for (dimension_type row = gen_sys.num_generators(); row-- > 1; )
00573 if (gen_sys[row].is_parameter())
00574 return false;
00575 return true;
00576 }
00577
00578 if (congruences_are_minimized()) {
00579 proper_cg_search:
00580
00581
00582 for (dimension_type row = con_sys.num_rows() - 1; row-- > 0; )
00583 if (con_sys[row].is_proper_congruence())
00584 return false;
00585 return true;
00586 }
00587
00588 Grid& gr = const_cast<Grid&>(*this);
00589 if (generators_are_up_to_date()) {
00590 gr.simplify(gr.gen_sys, gr.dim_kinds);
00591 gr.set_generators_minimized();
00592 goto param_search;
00593 }
00594
00595
00596 if (gr.simplify(gr.con_sys, gr.dim_kinds)) {
00597
00598 gr.set_empty();
00599 return true;
00600 }
00601 gr.set_congruences_minimized();
00602 goto proper_cg_search;
00603 }
00604
00605 bool
00606 PPL::Grid::OK(bool check_not_empty) const {
00607 #ifndef NDEBUG
00608 using std::endl;
00609 using std::cerr;
00610 #endif
00611
00612
00613 if (!status.OK())
00614 goto fail;
00615
00616 if (marked_empty()) {
00617 if (check_not_empty) {
00618
00619 #ifndef NDEBUG
00620 cerr << "Empty grid!" << endl;
00621 #endif
00622 goto fail;
00623 }
00624
00625 if (con_sys.space_dimension() != space_dim) {
00626 #ifndef NDEBUG
00627 cerr << "The grid is in a space of dimension " << space_dim
00628 << " while the system of congruences is in a space of dimension "
00629 << con_sys.space_dimension()
00630 << endl;
00631 #endif
00632 goto fail;
00633 }
00634 return true;
00635 }
00636
00637
00638
00639
00640 if (space_dim == 0) {
00641 if (con_sys.num_rows() == 0)
00642 if (gen_sys.num_generators() == 1 && gen_sys[0].is_point())
00643 return true;
00644 #ifndef NDEBUG
00645 cerr << "Zero-dimensional grid should have an empty congruence" << endl
00646 << "system and a generator system of a single point." << endl;
00647 #endif
00648 goto fail;
00649 }
00650
00651
00652
00653 if (!congruences_are_up_to_date() && !generators_are_up_to_date()) {
00654 #ifndef NDEBUG
00655 cerr << "Grid not empty, not zero-dimensional" << endl
00656 << "and with neither congruences nor generators up-to-date!"
00657 << endl;
00658 #endif
00659 goto fail;
00660 }
00661
00662 {
00663
00664
00665
00666
00667
00668 const dimension_type num_columns = space_dim + 1;
00669
00670
00671
00672
00673
00674 if (congruences_are_up_to_date())
00675 if (con_sys.num_columns() != num_columns + 1 ) {
00676 #ifndef NDEBUG
00677 cerr << "Incompatible size! (con_sys and space_dim)"
00678 << endl;
00679 #endif
00680 goto fail;
00681 }
00682
00683 if (generators_are_up_to_date()) {
00684 if (gen_sys.space_dimension() + 1 != num_columns) {
00685 #ifndef NDEBUG
00686 cerr << "Incompatible size! (gen_sys and space_dim)"
00687 << endl;
00688 #endif
00689 goto fail;
00690 }
00691
00692
00693 if (!gen_sys.OK()) {
00694 #ifndef NDEBUG
00695 cerr << "gen_sys OK failed." << endl;
00696 #endif
00697 goto fail;
00698 }
00699
00700 for (dimension_type i = gen_sys.num_generators(); i-- > 0; ) {
00701 const Grid_Generator& g = gen_sys[i];
00702
00703 if (g.size() < 1) {
00704 #ifndef NDEBUG
00705 cerr << "Parameter should have coefficients." << endl;
00706 #endif
00707 goto fail;
00708 }
00709 }
00710
00711
00712
00713 if (gen_sys.num_generators() > 0 && !gen_sys.has_points()) {
00714 #ifndef NDEBUG
00715 cerr << "Non-empty generator system declared up-to-date "
00716 << "has no points!"
00717 << endl;
00718 #endif
00719 goto fail;
00720 }
00721
00722 if (generators_are_minimized()) {
00723 Grid_Generator_System gs = gen_sys;
00724
00725 if (dim_kinds.size() != num_columns) {
00726 #ifndef NDEBUG
00727 cerr << "Size of dim_kinds should equal the number of columns."
00728 << endl;
00729 #endif
00730 goto fail;
00731 }
00732
00733 if (!upper_triangular(gs, dim_kinds)) {
00734 #ifndef NDEBUG
00735 cerr << "Reduced generators should be upper triangular."
00736 << endl;
00737 #endif
00738 goto fail;
00739 }
00740
00741
00742 for (dimension_type dim = 0, row = 0;
00743 dim < space_dim + 1;
00744 ++dim, assert(row <= dim)) {
00745 if (dim_kinds[dim] == GEN_VIRTUAL
00746 || (gen_sys[row++].is_parameter_or_point()
00747 && dim_kinds[dim] == PARAMETER)
00748 || (assert(gen_sys[row-1].is_line()), dim_kinds[dim] == LINE))
00749 continue;
00750 #ifndef NDEBUG
00751 cerr << "Kinds in dim_kinds should match those in gen_sys."
00752 << endl;
00753 #endif
00754 goto fail;
00755 }
00756
00757
00758
00759 Dimension_Kinds dk = dim_kinds;
00760
00761
00762 assert(gs.num_generators() > 0);
00763 simplify(gs, dk);
00764
00765
00766 assert(gs.num_generators() > 0);
00767 for (dimension_type row = 0; row < gen_sys.num_generators(); ++row) {
00768 Grid_Generator& g = gs[row];
00769 const Grid_Generator& g_copy = gen_sys[row];
00770 if (g.is_equal_to(g_copy))
00771 continue;
00772 #ifndef NDEBUG
00773 cerr << "Generators are declared minimized,"
00774 " but they change under reduction.\n"
00775 << "Here is the generator system:\n";
00776 gen_sys.ascii_dump(cerr);
00777 cerr << "and here is the minimized form of the temporary copy:\n";
00778 gs.ascii_dump(cerr);
00779 #endif
00780 goto fail;
00781 }
00782 }
00783
00784 }
00785 }
00786
00787 if (congruences_are_up_to_date()) {
00788
00789 if (!con_sys.OK()) {
00790 #ifndef NDEBUG
00791 cerr << "con_sys OK failed." << endl;
00792 #endif
00793 goto fail;
00794 }
00795
00796 Grid tem_gr = *this;
00797 Congruence_System cs_copy = tem_gr.con_sys;
00798
00799
00800 Grid_Generator_System gs(space_dim);
00801 std::swap(tem_gr.gen_sys, gs);
00802 tem_gr.clear_generators_up_to_date();
00803
00804 if (!tem_gr.update_generators()) {
00805 if (check_not_empty) {
00806
00807 #ifndef NDEBUG
00808 cerr << "Unsatisfiable system of congruences!"
00809 << endl;
00810 #endif
00811 goto fail;
00812 }
00813
00814 return true;
00815 }
00816
00817 if (congruences_are_minimized()) {
00818
00819 if (!lower_triangular(con_sys, dim_kinds)) {
00820 #ifndef NDEBUG
00821 cerr << "Reduced congruences should be lower triangular." << endl;
00822 #endif
00823 goto fail;
00824 }
00825
00826
00827
00828
00829 if (!con_sys.is_equal_to(cs_copy)) {
00830 #ifndef NDEBUG
00831 cerr << "Congruences are declared minimized, but they change under reduction!"
00832 << endl
00833 << "Here is the minimized form of the congruence system:"
00834 << endl;
00835 cs_copy.ascii_dump(cerr);
00836 cerr << endl;
00837 #endif
00838 goto fail;
00839 }
00840
00841 if (dim_kinds.size() != con_sys.num_columns() - 1 ) {
00842 #ifndef NDEBUG
00843 cerr << "Size of dim_kinds should equal the number of columns."
00844 << endl;
00845 #endif
00846 goto fail;
00847 }
00848
00849
00850 for (dimension_type dim = 0, row = con_sys.num_rows() - 1;
00851 dim < space_dim + 1;
00852 ++dim) {
00853 if (dim_kinds[dim] == CON_VIRTUAL
00854 || (con_sys[row--].is_proper_congruence()
00855 && dim_kinds[dim] == PROPER_CONGRUENCE)
00856 || (assert(con_sys[row+1].is_equality()),
00857 dim_kinds[dim] == EQUALITY))
00858 continue;
00859 #ifndef NDEBUG
00860 cerr << "Kinds in dim_kinds should match those in con_sys." << endl;
00861 #endif
00862 goto fail;
00863 }
00864 }
00865 }
00866
00867 return true;
00868
00869 fail:
00870 #ifndef NDEBUG
00871 cerr << "Here is the grid under check:" << endl;
00872 ascii_dump(cerr);
00873 #endif
00874 return false;
00875 }
00876
00877 void
00878 PPL::Grid::add_congruence(const Congruence& cg) {
00879
00880
00881 if (space_dim < cg.space_dimension())
00882 throw_dimension_incompatible("add_congruence(cg)", "cg", cg);
00883
00884
00885
00886 if (marked_empty())
00887 return;
00888
00889
00890 if (space_dim == 0) {
00891 if (!cg.is_trivial_true())
00892 set_empty();
00893 return;
00894 }
00895
00896 congruences_are_up_to_date() || update_congruences();
00897
00898 con_sys.insert(cg);
00899
00900 clear_congruences_minimized();
00901 set_congruences_up_to_date();
00902 clear_generators_up_to_date();
00903
00904
00905
00906 assert(OK());
00907 }
00908
00909 void
00910 PPL::Grid::add_congruence(const Constraint& c) {
00911
00912 if (c.is_equality()) {
00913 Congruence_System cgs(c);
00914 add_recycled_congruences(cgs);
00915 }
00916 }
00917
00918 bool
00919 PPL::Grid::add_congruence_and_minimize(const Congruence& cg) {
00920
00921 Congruence_System cgs(cg);
00922 return add_recycled_congruences_and_minimize(cgs);
00923 }
00924
00925 bool
00926 PPL::Grid::add_congruence_and_minimize(const Constraint& c) {
00927
00928 if (c.is_equality()) {
00929 Congruence_System cgs(c);
00930 return add_recycled_congruences_and_minimize(cgs);
00931 }
00932 return minimize();
00933 }
00934
00935 void
00936 PPL::Grid::add_generator(const Grid_Generator& g) {
00937
00938 const dimension_type g_space_dim = g.space_dimension();
00939 if (space_dim < g_space_dim)
00940 throw_dimension_incompatible("add_generator(g)", "g", g);
00941
00942
00943 if (space_dim == 0) {
00944
00945
00946 if (marked_empty()) {
00947 if (g.is_parameter())
00948 throw_invalid_generator("add_generator(g)", "g");
00949 set_zero_dim_univ();
00950 }
00951 assert(OK());
00952 return;
00953 }
00954
00955 if (marked_empty()
00956 || (!generators_are_up_to_date() && !update_generators())) {
00957
00958
00959 if (g.is_line_or_parameter())
00960 throw_invalid_generator("add_generator(g)", "g");
00961 gen_sys.insert(g);
00962 clear_empty();
00963 }
00964 else {
00965 assert(generators_are_up_to_date());
00966 gen_sys.insert(g);
00967 if (g.is_parameter_or_point())
00968 normalize_divisors(gen_sys);
00969 }
00970
00971
00972 clear_congruences_up_to_date();
00973
00974 clear_generators_minimized();
00975 set_generators_up_to_date();
00976 assert(OK());
00977 }
00978
00979 bool
00980 PPL::Grid::add_generator_and_minimize(const Grid_Generator& g) {
00981
00982 Grid_Generator_System gs(g);
00983 return add_recycled_generators_and_minimize(gs);
00984 }
00985
00986 void
00987 PPL::Grid::add_recycled_congruences(Congruence_System& cgs) {
00988
00989
00990 const dimension_type cgs_space_dim = cgs.space_dimension();
00991 if (space_dim < cgs_space_dim)
00992 throw_dimension_incompatible("add_recycled_congruences(cgs)", "cgs", cgs);
00993
00994 if (cgs.num_rows() == 0)
00995 return;
00996
00997 if (space_dim == 0) {
00998
00999
01000
01001
01002 if (cgs.begin() != cgs.end())
01003
01004 if (status.test_zero_dim_univ())
01005 set_empty();
01006 return;
01007 }
01008
01009 if (marked_empty()) {
01010 assert(OK());
01011 return;
01012 }
01013
01014
01015 congruences_are_up_to_date() || update_congruences();
01016
01017
01018
01019 con_sys.recycling_insert(cgs);
01020
01021
01022 clear_congruences_minimized();
01023 clear_generators_up_to_date();
01024
01025
01026 assert(OK());
01027 }
01028
01029 void
01030 PPL::Grid::add_recycled_congruences(Constraint_System& cs) {
01031
01032
01033 if (space_dim < cs.space_dimension())
01034 throw_dimension_incompatible("add_recycled_congruences(cs)", "cs", cs);
01035 Congruence_System cgs(cs);
01036 add_recycled_congruences(cgs);
01037 }
01038
01039 void
01040 PPL::Grid::add_congruences(const Congruence_System& cgs) {
01041
01042
01043 if (space_dim < cgs.space_dimension())
01044 throw_dimension_incompatible("add_congruences(cgs)", "cgs", cgs);
01045 Congruence_System cgs_copy = cgs;
01046 add_recycled_congruences(cgs_copy);
01047 }
01048
01049 void
01050 PPL::Grid::add_congruences(const Constraint_System& cs) {
01051
01052
01053 if (space_dim < cs.space_dimension())
01054 throw_dimension_incompatible("add_congruences(cs)", "cs", cs);
01055 Congruence_System cgs(cs);
01056 add_recycled_congruences(cgs);
01057 }
01058
01059 bool
01060 PPL::Grid::add_recycled_congruences_and_minimize(Congruence_System& cgs) {
01061
01062
01063 const dimension_type cgs_space_dim = cgs.space_dimension();
01064 if (space_dim < cgs_space_dim)
01065 throw_dimension_incompatible("add_recycled_congruences_and_minimize(cgs)",
01066 "cgs", cgs);
01067
01068
01069 if (cgs.num_rows() == 0)
01070 return minimize();
01071
01072
01073 if (space_dim == 0) {
01074
01075
01076
01077
01078 if (cgs.begin() == cgs.end())
01079 return true;
01080
01081 if (status.test_zero_dim_univ())
01082 set_empty();
01083 return false;
01084 }
01085
01086 if (marked_empty())
01087 return false;
01088
01089 congruences_are_up_to_date() || update_congruences();
01090
01091 con_sys.recycling_insert(cgs);
01092
01093 clear_congruences_minimized();
01094
01095 #ifndef NDEBUG
01096 bool ret = update_generators();
01097 assert(OK());
01098 return ret;
01099 #else
01100 return update_generators();
01101 #endif
01102 }
01103
01104 bool
01105 PPL::Grid::add_recycled_congruences_and_minimize(Constraint_System& cs) {
01106
01107
01108 if (space_dim < cs.space_dimension())
01109 throw_dimension_incompatible("add_recycled_congruences_and_minimize(cs)",
01110 "cs", cs);
01111 Congruence_System cgs(cs);
01112 return add_recycled_congruences_and_minimize(cgs);
01113 }
01114
01115 bool
01116 PPL::Grid::add_congruences_and_minimize(const Congruence_System& cgs) {
01117
01118 Congruence_System cgs_copy = cgs;
01119 return add_recycled_congruences_and_minimize(cgs_copy);
01120 }
01121
01122 bool
01123 PPL::Grid::add_congruences_and_minimize(const Constraint_System& cs) {
01124
01125
01126 if (space_dim < cs.space_dimension())
01127 throw_dimension_incompatible("add_congruences_and_minimize(cs)", "cs", cs);
01128 Congruence_System cgs(cs);
01129 return add_recycled_congruences_and_minimize(cgs);
01130 }
01131
01132 void
01133 PPL::Grid::add_constraint(const Constraint& c) {
01134
01135 if (space_dim < c.space_dimension())
01136 throw_dimension_incompatible("add_constraint(c)", "c", c);
01137 if (c.is_equality()) {
01138 Congruence cg(c);
01139 add_congruence(cg);
01140 }
01141 }
01142
01143 bool
01144 PPL::Grid::add_constraint_and_minimize(const Constraint& c) {
01145
01146 if (space_dim < c.space_dimension())
01147 throw_dimension_incompatible("add_constraint_and_minimize(c)", "c", c);
01148 if (c.is_equality()) {
01149 Congruence cg(c);
01150 return add_congruence_and_minimize(cg);
01151 }
01152 return minimize();
01153 }
01154
01155 void
01156 PPL::Grid::add_constraints(const Constraint_System& cs) {
01157
01158 if (space_dim < cs.space_dimension())
01159 throw_dimension_incompatible("add_constraints(cs)", "cs", cs);
01160 Congruence_System cgs(cs);
01161 add_recycled_congruences(cgs);
01162 }
01163
01164 bool
01165 PPL::Grid::add_constraints_and_minimize(const Constraint_System& cs) {
01166
01167 if (space_dim < cs.space_dimension())
01168 throw_dimension_incompatible("add_constraints_and_minimize(cs)",
01169 "cs", cs);
01170 Congruence_System cgs(cs);
01171 return add_recycled_congruences_and_minimize(cgs);
01172 }
01173
01174 void
01175 PPL::Grid::add_recycled_constraints(Constraint_System& cs) {
01176
01177 if (space_dim < cs.space_dimension())
01178 throw_dimension_incompatible("add_recycled_constraints(cs)",
01179 "cs", cs);
01180 Congruence_System cgs(cs);
01181 add_recycled_congruences(cgs);
01182 }
01183
01184 bool
01185 PPL::Grid::add_recycled_constraints_and_minimize(Constraint_System& cs) {
01186
01187 if (space_dim < cs.space_dimension())
01188 throw_dimension_incompatible("add_recycled_constraints_and_minimize(cs)",
01189 "cs", cs);
01190 Congruence_System cgs(cs);
01191 return add_recycled_congruences_and_minimize(cgs);
01192 }
01193
01194 void
01195 PPL::Grid::add_recycled_generators(Grid_Generator_System& gs) {
01196
01197
01198 const dimension_type gs_space_dim = gs.space_dimension();
01199 if (space_dim < gs_space_dim)
01200 throw_dimension_incompatible("add_recycled_generators(gs)", "gs", gs);
01201
01202
01203 if (gs.num_generators() == 0)
01204 return;
01205
01206
01207
01208 if (space_dim == 0) {
01209 if (marked_empty())
01210 if (gs.has_points())
01211 set_zero_dim_univ();
01212 else
01213 throw_invalid_generators("add_recycled_generators(gs)", "gs");
01214 assert(OK(true));
01215 return;
01216 }
01217
01218 if (!marked_empty()
01219 && (generators_are_up_to_date() || update_generators())) {
01220
01221
01222 normalize_divisors(gs, gen_sys);
01223
01224 gen_sys.recycling_insert(gs);
01225
01226
01227 clear_congruences_up_to_date();
01228 clear_generators_minimized();
01229
01230 assert(OK(true));
01231 return;
01232 }
01233
01234
01235
01236
01237 if (!gs.has_points())
01238 throw_invalid_generators("add_recycled_generators(gs)", "gs");
01239
01240
01241 gs.insert(parameter(0*Variable(space_dim-1)));
01242
01243 std::swap(gen_sys, gs);
01244
01245 normalize_divisors(gen_sys);
01246
01247
01248 set_generators_up_to_date();
01249 clear_empty();
01250
01251 assert(OK());
01252 }
01253
01254 void
01255 PPL::Grid::add_generators(const Grid_Generator_System& gs) {
01256
01257 Grid_Generator_System gs_copy = gs;
01258 add_recycled_generators(gs_copy);
01259 }
01260
01261 bool
01262 PPL::Grid::add_recycled_generators_and_minimize(Grid_Generator_System& gs) {
01263
01264
01265 const dimension_type gs_space_dim = gs.space_dimension();
01266 if (space_dim < gs_space_dim)
01267 throw_dimension_incompatible("add_recycled_generators_and_minimize(gs)",
01268 "gs", gs);
01269
01270
01271 if (gs.num_generators() == 0)
01272 return minimize();
01273
01274
01275
01276 if (space_dim == 0) {
01277 if (marked_empty())
01278 if (gs.has_points())
01279 set_zero_dim_univ();
01280 else
01281 throw_invalid_generators("add_recycled_generators_and_minimize(gs)",
01282 "gs");
01283 assert(OK(true));
01284 return true;
01285 }
01286
01287
01288 gs.insert(parameter(0*Variable(space_dim-1)));
01289
01290 if (!marked_empty()
01291 && (generators_are_up_to_date() || update_generators())) {
01292
01293 normalize_divisors(gs, gen_sys);
01294
01295 for (dimension_type row = 0; row < gs.num_generators(); ++row)
01296 gen_sys.recycling_insert(gs[row]);
01297 }
01298 else {
01299
01300 if (!gs.has_points())
01301 throw_invalid_generators("add_recycled_generators_and_minimize(gs)",
01302 "gs");
01303 std::swap(gen_sys, gs);
01304 normalize_divisors(gen_sys);
01305 clear_empty();
01306 }
01307 clear_generators_minimized();
01308 update_congruences();
01309
01310 assert(OK(true));
01311 return true;
01312 }
01313
01314 bool
01315 PPL::Grid::add_generators_and_minimize(const Grid_Generator_System& gs) {
01316
01317 Grid_Generator_System gs_copy = gs;
01318 return add_recycled_generators_and_minimize(gs_copy);
01319 }
01320
01321 void
01322 PPL::Grid::intersection_assign(const Grid& y) {
01323 Grid& x = *this;
01324
01325 if (x.space_dim != y.space_dim)
01326 throw_dimension_incompatible("intersection_assign(y)", "y", y);
01327
01328
01329 if (x.marked_empty())
01330 return;
01331 if (y.marked_empty()) {
01332 x.set_empty();
01333 return;
01334 }
01335
01336
01337
01338 if (x.space_dim == 0)
01339 return;
01340
01341
01342 x.congruences_are_up_to_date() || x.update_congruences();
01343 y.congruences_are_up_to_date() || y.update_congruences();
01344
01345 if (y.con_sys.num_rows() > 0 ) {
01346 x.con_sys.insert(y.con_sys);
01347
01348
01349 x.clear_generators_up_to_date();
01350 x.clear_congruences_minimized();
01351 }
01352
01353
01354 assert(x.OK() && y.OK(true));
01355 }
01356
01357 bool
01358 PPL::Grid::intersection_assign_and_minimize(const Grid& y) {
01359 intersection_assign(y);
01360 return minimize();
01361 }
01362
01363 void
01364 PPL::Grid::join_assign(const Grid& y) {
01365 Grid& x = *this;
01366
01367 if (x.space_dim != y.space_dim)
01368 throw_dimension_incompatible("join_assign(y)", "y", y);
01369
01370
01371 if (y.marked_empty())
01372 return;
01373 if (x.marked_empty()) {
01374 x = y;
01375 return;
01376 }
01377
01378
01379
01380 if (x.space_dim == 0)
01381 return;
01382
01383
01384 if (!x.generators_are_up_to_date() && !x.update_generators()) {
01385
01386 x = y;
01387 return;
01388 }
01389 if (!y.generators_are_up_to_date() && !y.update_generators())
01390
01391 return;
01392
01393
01394 Grid_Generator_System gs(y.gen_sys);
01395 normalize_divisors(x.gen_sys, gs);
01396 x.gen_sys.recycling_insert(gs);
01397
01398
01399 x.clear_congruences_up_to_date();
01400 x.clear_generators_minimized();
01401
01402
01403 assert(x.OK(true) && y.OK(true));
01404 }
01405
01406 bool
01407 PPL::Grid::join_assign_and_minimize(const Grid& y) {
01408 join_assign(y);
01409 return minimize();
01410 }
01411
01412 bool
01413 PPL::Grid::join_assign_if_exact(const Grid& y) {
01414 Grid& x = *this;
01415
01416
01417 if (x.space_dim != y.space_dim)
01418 throw_dimension_incompatible("join_assign_if_exact(y)", "y", y);
01419
01420 if (x.marked_empty()
01421 || y.marked_empty()
01422 || x.space_dim == 0
01423 || x.is_included_in(y)
01424 || y.is_included_in(x)) {
01425 join_assign(y);
01426 return true;
01427 }
01428
01429 Grid x_copy = x;
01430 x_copy.join_assign(y);
01431 x_copy.grid_difference_assign(y);
01432 if (x_copy.is_included_in(x)) {
01433 join_assign(y);
01434 return true;
01435 }
01436
01437 return false;
01438 }
01439
01440 void
01441 PPL::Grid::grid_difference_assign(const Grid& y) {
01442 Grid& x = *this;
01443
01444 if (x.space_dim != y.space_dim)
01445 throw_dimension_incompatible("poly_difference_assign(y)", "y", y);
01446
01447 if (y.marked_empty() || x.marked_empty())
01448 return;
01449
01450
01451
01452 if (x.space_dim == 0) {
01453 x.set_empty();
01454 return;
01455 }
01456
01457 if (y.contains(x)) {
01458 x.set_empty();
01459 return;
01460 }
01461
01462 Grid new_grid(x.space_dim, EMPTY);
01463
01464 const Congruence_System& y_cgs = y.congruences();
01465 for (Congruence_System::const_iterator i = y_cgs.begin(),
01466 y_cgs_end = y_cgs.end(); i != y_cgs_end; ++i) {
01467 const Congruence& cg = *i;
01468
01469
01470
01471
01472
01473
01474
01475
01476
01477
01478
01479
01480
01481 if (x.relation_with(cg).implies(Poly_Con_Relation::is_included()))
01482 continue;
01483
01484 if (cg.is_proper_congruence()) {
01485 const Linear_Expression e = Linear_Expression(cg);
01486
01487 Coefficient_traits::const_reference m = cg.modulus();
01488
01489
01490
01491
01492 if (x.relation_with((2*e %= 0) / m)
01493 .implies(Poly_Con_Relation::is_included())) {
01494 Grid z = x;
01495 z.add_congruence((2*e %= m) / (2*m));
01496 new_grid.join_assign(z);
01497 continue;
01498 }
01499 }
01500 return;
01501 }
01502
01503 *this = new_grid;
01504
01505 assert(OK());
01506 }
01507
01508 void
01509 PPL::Grid::affine_image(const Variable var,
01510 const Linear_Expression& expr,
01511 Coefficient_traits::const_reference denominator) {
01512
01513 if (denominator == 0)
01514 throw_invalid_argument("affine_image(v, e, d)", "d == 0");
01515
01516
01517
01518 const dimension_type expr_space_dim = expr.space_dimension();
01519 if (space_dim < expr_space_dim)
01520 throw_dimension_incompatible("affine_image(v, e, d)", "e", expr);
01521
01522 const dimension_type var_space_dim = var.space_dimension();
01523 if (space_dim < var_space_dim)
01524 throw_dimension_incompatible("affine_image(v, e, d)", "v", var);
01525
01526 if (marked_empty())
01527 return;
01528
01529 if (var_space_dim <= expr_space_dim && expr[var_space_dim] != 0) {
01530
01531 if (generators_are_up_to_date()) {
01532
01533
01534 if (denominator > 0)
01535 gen_sys.affine_image(var_space_dim, expr, denominator);
01536 else
01537 gen_sys.affine_image(var_space_dim, -expr, -denominator);
01538 clear_generators_minimized();
01539
01540
01541 normalize_divisors(gen_sys);
01542 }
01543 if (congruences_are_up_to_date()) {
01544
01545
01546
01547 Linear_Expression inverse;
01548 if (expr[var_space_dim] > 0) {
01549 inverse = -expr;
01550 inverse[var_space_dim] = denominator;
01551 con_sys.affine_preimage(var_space_dim, inverse, expr[var_space_dim]);
01552 }
01553 else {
01554
01555
01556
01557 inverse = expr;
01558 inverse[var_space_dim] = denominator;
01559 neg_assign(inverse[var_space_dim]);
01560 con_sys.affine_preimage(var_space_dim, inverse, -expr[var_space_dim]);
01561 }
01562 clear_congruences_minimized();
01563 }
01564 }
01565 else {
01566
01567
01568 if (!generators_are_up_to_date())
01569 minimize();
01570 if (!marked_empty()) {
01571
01572
01573 if (denominator > 0)
01574 gen_sys.affine_image(var_space_dim, expr, denominator);
01575 else
01576 gen_sys.affine_image(var_space_dim, -expr, -denominator);
01577
01578 clear_congruences_up_to_date();
01579 clear_generators_minimized();
01580
01581
01582 normalize_divisors(gen_sys);
01583 }
01584 }
01585 assert(OK());
01586 }
01587
01588 void
01589 PPL::Grid::
01590 affine_preimage(const Variable var,
01591 const Linear_Expression& expr,
01592 Coefficient_traits::const_reference denominator) {
01593
01594 if (denominator == 0)
01595 throw_invalid_argument("affine_preimage(v, e, d)", "d == 0");
01596
01597
01598
01599
01600 const dimension_type expr_space_dim = expr.space_dimension();
01601 if (space_dim < expr_space_dim)
01602 throw_dimension_incompatible("affine_preimage(v, e, d)", "e", expr);
01603
01604 const dimension_type var_space_dim = var.space_dimension();
01605 if (space_dim < var_space_dim)
01606 throw_dimension_incompatible("affine_preimage(v, e, d)", "v", var);
01607
01608 if (marked_empty())
01609 return;
01610
01611 if (var_space_dim <= expr_space_dim && expr[var_space_dim] != 0) {
01612
01613 if (congruences_are_up_to_date()) {
01614
01615
01616 if (denominator > 0)
01617 con_sys.affine_preimage(var_space_dim, expr, denominator);
01618 else
01619 con_sys.affine_preimage(var_space_dim, -expr, -denominator);
01620 clear_congruences_minimized();
01621 }
01622 if (generators_are_up_to_date()) {
01623
01624
01625
01626 Linear_Expression inverse;
01627 if (expr[var_space_dim] > 0) {
01628 inverse = -expr;
01629 inverse[var_space_dim] = denominator;
01630 gen_sys.affine_image(var_space_dim, inverse, expr[var_space_dim]);
01631 }
01632 else {
01633
01634
01635
01636 inverse = expr;
01637 inverse[var_space_dim] = denominator;
01638 neg_assign(inverse[var_space_dim]);
01639 gen_sys.affine_image(var_space_dim, inverse, -expr[var_space_dim]);
01640 }
01641 clear_generators_minimized();
01642 }
01643 }
01644 else {
01645
01646
01647 if (!congruences_are_up_to_date())
01648 minimize();
01649
01650
01651 if (denominator > 0)
01652 con_sys.affine_preimage(var_space_dim, expr, denominator);
01653 else
01654 con_sys.affine_preimage(var_space_dim, -expr, -denominator);
01655
01656 clear_generators_up_to_date();
01657 clear_congruences_minimized();
01658 }
01659 assert(OK());
01660 }
01661
01662 void
01663 PPL::Grid::
01664 generalized_affine_image(const Variable var,
01665 const Linear_Expression& expr,
01666 Coefficient_traits::const_reference denominator,
01667 Coefficient_traits::const_reference modulus) {
01668
01669 if (denominator == 0)
01670 throw_invalid_argument("generalized_affine_image(v, r, e, d)", "d == 0");
01671
01672
01673
01674
01675 const dimension_type expr_space_dim = expr.space_dimension();
01676 if (space_dim < expr_space_dim)
01677 throw_dimension_incompatible("generalized_affine_image(v, r, e, d)",
01678 "e", expr);
01679
01680 const dimension_type var_space_dim = var.space_dimension();
01681 if (space_dim < var_space_dim)
01682 throw_dimension_incompatible("generalized_affine_image(v, r, e, d)",
01683 "v", var);
01684
01685
01686 if (marked_empty())
01687 return;
01688
01689 affine_image(var, expr, denominator);
01690
01691 if (modulus == 0)
01692 return;
01693
01694
01695
01696 generators_are_up_to_date() || minimize();
01697
01698
01699
01700 if (marked_empty())
01701 return;
01702
01703 if (modulus < 0)
01704 gen_sys.insert(parameter(-modulus * var));
01705 else
01706 gen_sys.insert(parameter(modulus * var));
01707
01708 normalize_divisors(gen_sys);
01709
01710 clear_generators_minimized();
01711 clear_congruences_up_to_date();
01712
01713 assert(OK());
01714 }
01715
01716 void PPL::Grid::
01717 generalized_affine_preimage(const Variable var,
01718 const Linear_Expression& expr,
01719 Coefficient_traits::const_reference denominator,
01720 Coefficient_traits::const_reference modulus) {
01721
01722 if (denominator == 0)
01723 throw_invalid_argument("generalized_affine_preimage(v, e, d, m)",
01724 "d == 0");
01725
01726
01727
01728 const dimension_type expr_space_dim = expr.space_dimension();
01729 if (space_dim < expr_space_dim)
01730 throw_dimension_incompatible("generalized_affine_preimage(v, e, d, m)",
01731 "e", expr);
01732
01733 const dimension_type var_space_dim = var.space_dimension();
01734 if (space_dim < var_space_dim)
01735 throw_dimension_incompatible("generalized_affine_preimage(v, e, d, m)",
01736 "v", var);
01737
01738
01739 if (modulus == 0) {
01740 affine_preimage(var, expr, denominator);
01741 return;
01742 }
01743
01744
01745
01746 Coefficient_traits::const_reference var_coefficient = expr.coefficient(var);
01747 if (var_space_dim <= expr_space_dim && var_coefficient != 0) {
01748 Linear_Expression inverse_expr
01749 = expr - (denominator + var_coefficient) * var;
01750 Coefficient inverse_denominator = - var_coefficient;
01751 if (modulus < 0)
01752 generalized_affine_image(var, inverse_expr, inverse_denominator,
01753 - modulus);
01754 else
01755 generalized_affine_image(var, inverse_expr, inverse_denominator,
01756 modulus);
01757 return;
01758 }
01759
01760
01761
01762
01763 if (modulus < 0)
01764 add_congruence((denominator*var %= expr) / denominator /= - modulus);
01765 else
01766 add_congruence((denominator*var %= expr) / denominator /= modulus);
01767
01768
01769
01770 if (is_empty())
01771 return;
01772 add_generator(grid_line(var));
01773 assert(OK());
01774 }
01775
01776 void
01777 PPL::Grid::
01778 generalized_affine_image(const Linear_Expression& lhs,
01779 const Linear_Expression& rhs,
01780 Coefficient_traits::const_reference modulus) {
01781
01782
01783
01784 dimension_type lhs_space_dim = lhs.space_dimension();
01785 if (space_dim < lhs_space_dim)
01786 throw_dimension_incompatible("generalized_affine_image(e1, r, e2)",
01787 "e1", lhs);
01788
01789
01790 const dimension_type rhs_space_dim = rhs.space_dimension();
01791 if (space_dim < rhs_space_dim)
01792 throw_dimension_incompatible("generalized_affine_image(e1, r, e2)",
01793 "e2", rhs);
01794
01795
01796 if (marked_empty())
01797 return;
01798
01799 TEMP_INTEGER(mod);
01800 if (modulus < 0)
01801 mod = -modulus;
01802 else
01803 mod = modulus;
01804
01805
01806
01807 do {
01808 if (lhs_space_dim == 0) {
01809
01810 add_congruence((lhs %= rhs) / mod);
01811 return;
01812 }
01813 }
01814 while (lhs.coefficient(Variable(--lhs_space_dim)) == 0);
01815
01816
01817
01818
01819
01820 Grid_Generator_System new_lines;
01821 bool lhs_vars_intersect_rhs_vars = false;
01822 for (dimension_type i = lhs_space_dim + 1; i-- > 0; )
01823 if (lhs.coefficient(Variable(i)) != 0) {
01824 new_lines.insert(Grid_Generator::line(Variable(i)));
01825 if (rhs.coefficient(Variable(i)) != 0)
01826 lhs_vars_intersect_rhs_vars = true;
01827 }
01828
01829 if (lhs_vars_intersect_rhs_vars) {
01830
01831
01832 const Variable new_var = Variable(space_dim);
01833 add_space_dimensions_and_embed(1);
01834
01835
01836
01837 Congruence_System new_cgs1(new_var == rhs);
01838 if (add_recycled_congruences_and_minimize(new_cgs1)) {
01839
01840
01841
01842
01843
01844
01845 new_lines.insert(parameter(0*Variable(space_dim-1)));
01846
01847 gen_sys.recycling_insert(new_lines);
01848 normalize_divisors(gen_sys);
01849
01850 clear_congruences_up_to_date();
01851 clear_generators_minimized();
01852
01853
01854
01855
01856 Congruence_System new_cgs2((lhs %= new_var) / mod);
01857 add_recycled_congruences(new_cgs2);
01858 }
01859
01860
01861 remove_higher_space_dimensions(space_dim-1);
01862 }
01863 else {
01864
01865
01866
01867
01868 if (is_empty())
01869 return;
01870
01871
01872
01873 add_recycled_generators(new_lines);
01874
01875
01876
01877 add_congruence((lhs %= rhs) / mod);
01878 }
01879
01880 assert(OK());
01881 }
01882
01883 void PPL::Grid::
01884 generalized_affine_preimage(const Linear_Expression& lhs,
01885 const Linear_Expression& rhs,
01886 Coefficient_traits::const_reference modulus) {
01887
01888 dimension_type lhs_space_dim = lhs.space_dimension();
01889 if (space_dim < lhs_space_dim)
01890 throw_dimension_incompatible("generalized_affine_preimage(e1, e2, m)",
01891 "lhs", lhs);
01892
01893 const dimension_type rhs_space_dim = rhs.space_dimension();
01894 if (space_dim < rhs_space_dim)
01895 throw_dimension_incompatible("generalized_affine_preimage(e1, e2, m)",
01896 "e2", rhs);
01897
01898
01899 if (marked_empty())
01900 return;
01901
01902 TEMP_INTEGER(mod);
01903 if (modulus < 0)
01904 mod = -modulus;
01905 else
01906 mod = modulus;
01907
01908
01909
01910 do {
01911 if (lhs_space_dim == 0) {
01912
01913
01914 add_congruence((lhs %= rhs) / mod);
01915 return;
01916 }
01917 }
01918 while (lhs.coefficient(Variable(--lhs_space_dim)) == 0);
01919
01920
01921
01922
01923
01924 Grid_Generator_System new_lines;
01925 bool lhs_vars_intersect_rhs_vars = false;
01926 for (dimension_type i = lhs_space_dim + 1; i-- > 0; )
01927 if (lhs.coefficient(Variable(i)) != 0) {
01928 new_lines.insert(Grid_Generator::line(Variable(i)));
01929 if (rhs.coefficient(Variable(i)) != 0)
01930 lhs_vars_intersect_rhs_vars = true;
01931 }
01932
01933 if (lhs_vars_intersect_rhs_vars) {
01934
01935
01936 const Variable new_var = Variable(space_dim);
01937 add_space_dimensions_and_embed(1);
01938
01939
01940
01941 Congruence_System new_cgs1(new_var == lhs);
01942 if (add_recycled_congruences_and_minimize(new_cgs1)) {
01943
01944
01945
01946
01947
01948
01949 new_lines.insert(parameter(0*Variable(space_dim-1)));
01950
01951 gen_sys.recycling_insert(new_lines);
01952 normalize_divisors(gen_sys);
01953
01954 clear_congruences_up_to_date();
01955 clear_generators_minimized();
01956
01957
01958
01959
01960 Congruence_System new_cgs2((rhs %= new_var) / mod);
01961 add_recycled_congruences(new_cgs2);
01962 }
01963
01964
01965 remove_higher_space_dimensions(space_dim-1);
01966 }
01967 else {
01968
01969
01970
01971
01972
01973 add_congruence((lhs %= rhs) / mod);
01974
01975
01976 if (is_empty())
01977 return;
01978
01979
01980
01981
01982
01983 add_recycled_generators(new_lines);
01984 }
01985 assert(OK());
01986 }
01987
01988 void
01989 PPL::Grid::time_elapse_assign(const Grid& y) {
01990 Grid& x = *this;
01991
01992 if (x.space_dim != y.space_dim)
01993 throw_dimension_incompatible("time_elapse_assign(y)", "y", y);
01994
01995
01996 if (x.space_dim == 0) {
01997 if (y.marked_empty())
01998 x.set_empty();
01999 return;
02000 }
02001
02002
02003 if (x.marked_empty())
02004 return;
02005 if (y.marked_empty()
02006 || (!x.generators_are_up_to_date() && !x.update_generators())
02007 || (!y.generators_are_up_to_date() && !y.update_generators())) {
02008 x.set_empty();
02009 return;
02010 }
02011
02012
02013 Grid_Generator_System gs = y.gen_sys;
02014 dimension_type gs_num_rows = gs.num_generators();
02015
02016 normalize_divisors(gs, gen_sys);
02017
02018 for (dimension_type i = gs_num_rows; i-- > 0; ) {
02019 Grid_Generator& g = gs[i];
02020 if (g.is_point()) {
02021
02022 TEMP_INTEGER(div);
02023 div = g.divisor();
02024 g.divisor() = 0;
02025 g.divisor() = div;
02026 }
02027 }
02028
02029 if (gs_num_rows == 0)
02030
02031
02032 return;
02033
02034
02035
02036 gen_sys.recycling_insert(gs);
02037
02038 x.clear_congruences_up_to_date();
02039 x.clear_generators_minimized();
02040
02041 assert(x.OK(true) && y.OK(true));
02042 }
02043
02045 bool
02046 PPL::operator==(const Grid& x, const Grid& y) {
02047 if (x.space_dim != y.space_dim)
02048 return false;
02049
02050 if (x.marked_empty())
02051 return y.is_empty();
02052 if (y.marked_empty())
02053 return x.is_empty();
02054 if (x.space_dim == 0)
02055 return true;
02056
02057 switch (x.quick_equivalence_test(y)) {
02058 case Grid::TVB_TRUE:
02059 return true;
02060
02061 case Grid::TVB_FALSE:
02062 return false;
02063
02064 default:
02065 if (x.is_included_in(y)) {
02066 if (x.marked_empty())
02067 return y.is_empty();
02068 return y.is_included_in(x);
02069 }
02070 return false;
02071 }
02072 }
02073
02074 bool
02075 PPL::Grid::contains(const Grid& y) const {
02076 const Grid& x = *this;
02077
02078
02079 if (x.space_dim != y.space_dim)
02080 throw_dimension_incompatible("contains(y)", "y", y);
02081
02082 if (y.marked_empty())
02083 return true;
02084 if (x.marked_empty())
02085 return y.is_empty();
02086 if (y.space_dim == 0)
02087 return true;
02088 if (x.quick_equivalence_test(y) == Grid::TVB_TRUE)
02089 return true;
02090 return y.is_included_in(x);
02091 }
02092
02093 bool
02094 PPL::Grid::is_disjoint_from(const Grid& y) const {
02095
02096 if (space_dim != y.space_dim)
02097 throw_dimension_incompatible("is_disjoint_from(y)", "y", y);
02098 Grid z = *this;
02099 return !z.intersection_assign_and_minimize(y);
02100 }
02101
02102 void
02103 PPL::Grid::ascii_dump(std::ostream& s) const {
02104 using std::endl;
02105
02106 s << "space_dim "
02107 << space_dim
02108 << endl;
02109 status.ascii_dump(s);
02110 s << "con_sys ("
02111 << (congruences_are_up_to_date() ? "" : "not_")
02112 << "up-to-date)"
02113 << endl;
02114 con_sys.ascii_dump(s);
02115 s << "gen_sys ("
02116 << (generators_are_up_to_date() ? "" : "not_")
02117 << "up-to-date)"
02118 << endl;
02119 gen_sys.ascii_dump(s);
02120 s << "dimension_kinds";
02121 if ((generators_are_up_to_date() && generators_are_minimized())
02122 || (congruences_are_up_to_date() && congruences_are_minimized()))
02123 for (Dimension_Kinds::const_iterator i = dim_kinds.begin();
02124 i != dim_kinds.end();
02125 ++i)
02126 s << " " << *i;
02127 s << endl;
02128 }
02129
02130 PPL_OUTPUT_DEFINITIONS(Grid);
02131
02132 bool
02133 PPL::Grid::ascii_load(std::istream& s) {
02134 std::string str;
02135
02136 if (!(s >> str) || str != "space_dim")
02137 return false;
02138
02139 if (!(s >> space_dim))
02140 return false;
02141
02142 if (!status.ascii_load(s))
02143 return false;
02144
02145 if (!(s >> str) || str != "con_sys")
02146 return false;
02147
02148 if (s >> str) {
02149 if (str == "(up-to-date)")
02150 set_congruences_up_to_date();
02151 else if (str != "(not_up-to-date)")
02152 return false;
02153 }
02154 else
02155 return false;
02156
02157 if (!con_sys.ascii_load(s))
02158 return false;
02159
02160 if (!(s >> str) || str != "gen_sys")
02161 return false;
02162
02163 if (s >> str) {
02164 if (str == "(up-to-date)")
02165 set_generators_up_to_date();
02166 else if (str != "(not_up-to-date)")
02167 return false;
02168 }
02169 else
02170 return false;
02171
02172 if (!gen_sys.ascii_load(s))
02173 return false;
02174
02175 if (!(s >> str) || str != "dimension_kinds")
02176 return false;
02177
02178 if (!marked_empty()
02179 && ((generators_are_up_to_date() && generators_are_minimized())
02180 || (congruences_are_up_to_date() && congruences_are_minimized()))) {
02181 dim_kinds.resize(space_dim + 1);
02182 for (Dimension_Kinds::size_type dim = 0; dim <= space_dim; ++dim) {
02183 short unsigned int dim_kind;
02184 if (!(s >> dim_kind))
02185 return false;
02186 switch(dim_kind) {
02187 case 0: dim_kinds[dim] = PARAMETER; break;
02188 case 1: dim_kinds[dim] = LINE; break;
02189 case 2: dim_kinds[dim] = GEN_VIRTUAL; break;
02190 default: return false;
02191 }
02192 }
02193 }
02194
02195
02196
02197 assert(OK());
02198 return true;
02199 }
02200
02201 PPL::memory_size_type
02202 PPL::Grid::external_memory_in_bytes() const {
02203 return
02204 con_sys.external_memory_in_bytes()
02205 + gen_sys.external_memory_in_bytes();
02206 }
02207
02209 std::ostream&
02210 PPL::IO_Operators::operator<<(std::ostream& s, const Grid& gr) {
02211 if (gr.is_empty())
02212 s << "false";
02213 else if (gr.is_universe())
02214 s << "true";
02215 else
02216 s << gr.minimized_congruences();
02217 return s;
02218 }