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