00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024 #ifndef PPL_Partially_Reduced_Product_templates_hh
00025 #define PPL_Partially_Reduced_Product_templates_hh 1
00026
00027 #include "Grid_Generator.defs.hh"
00028 #include "Grid_Generator_System.defs.hh"
00029 #include "Grid_Generator_System.inlines.hh"
00030 #include <algorithm>
00031 #include <deque>
00032
00033 namespace Parma_Polyhedra_Library {
00034
00035 template <typename D1, typename D2, typename R>
00036 Constraint_System
00037 Partially_Reduced_Product<D1, D2, R>::constraints() const {
00038 reduce();
00039 Constraint_System cs = d2.constraints();
00040 const Constraint_System& cs1 = d1.constraints();
00041 for (Constraint_System::const_iterator i = cs1.begin(),
00042 cs_end = cs1.end(); i != cs_end; ++i)
00043 cs.insert(*i);
00044 return cs;
00045 }
00046
00047 template <typename D1, typename D2, typename R>
00048 Constraint_System
00049 Partially_Reduced_Product<D1, D2, R>::minimized_constraints() const {
00050 reduce();
00051 Constraint_System cs = d2.constraints();
00052 const Constraint_System& cs1 = d1.constraints();
00053 for (Constraint_System::const_iterator i = cs1.begin(),
00054 cs_end = cs1.end(); i != cs_end; ++i)
00055 cs.insert(*i);
00056 if (cs.has_strict_inequalities()) {
00057 NNC_Polyhedron ph(cs);
00058 return ph.minimized_constraints();
00059 }
00060 else {
00061 C_Polyhedron ph(cs);
00062 return ph.minimized_constraints();
00063 }
00064 }
00065
00066 template <typename D1, typename D2, typename R>
00067 Congruence_System
00068 Partially_Reduced_Product<D1, D2, R>::congruences() const {
00069 reduce();
00070 Congruence_System cgs = d2.congruences();
00071 const Congruence_System& cgs1 = d1.congruences();
00072 for (Congruence_System::const_iterator i = cgs1.begin(),
00073 cgs_end = cgs1.end(); i != cgs_end; ++i)
00074 cgs.insert(*i);
00075 return cgs;
00076 }
00077
00078 template <typename D1, typename D2, typename R>
00079 Congruence_System
00080 Partially_Reduced_Product<D1, D2, R>::minimized_congruences() const {
00081 reduce();
00082 Congruence_System cgs = d2.congruences();
00083 const Congruence_System& cgs1 = d1.congruences();
00084 for (Congruence_System::const_iterator i = cgs1.begin(),
00085 cgs_end = cgs1.end(); i != cgs_end; ++i)
00086 cgs.insert(*i);
00087 Grid gr(cgs);
00088 return gr.minimized_congruences();
00089 }
00090
00091 template <typename D1, typename D2, typename R>
00092 void
00093 Partially_Reduced_Product<D1, D2, R>
00094 ::add_recycled_constraints(Constraint_System& cs) {
00095 if (d1.can_recycle_constraint_systems()) {
00096 d2.refine_with_constraints(cs);
00097 d1.add_recycled_constraints(cs);
00098 }
00099 else
00100 if (d2.can_recycle_constraint_systems()) {
00101 d1.refine_with_constraints(cs);
00102 d2.add_recycled_constraints(cs);
00103 }
00104 else {
00105 d1.add_constraints(cs);
00106 d2.add_constraints(cs);
00107 }
00108 clear_reduced_flag();
00109 }
00110
00111 template <typename D1, typename D2, typename R>
00112 void
00113 Partially_Reduced_Product<D1, D2, R>
00114 ::add_recycled_congruences(Congruence_System& cgs) {
00115 if (d1.can_recycle_congruence_systems()) {
00116 d2.refine_with_congruences(cgs);
00117 d1.add_recycled_congruences(cgs);
00118 }
00119 else
00120 if (d2.can_recycle_congruence_systems()) {
00121 d1.refine_with_congruences(cgs);
00122 d2.add_recycled_congruences(cgs);
00123 }
00124 else {
00125 d1.add_congruences(cgs);
00126 d2.add_congruences(cgs);
00127 }
00128 clear_reduced_flag();
00129 }
00130
00131 template <typename D1, typename D2, typename R>
00132 Poly_Gen_Relation
00133 Partially_Reduced_Product<D1, D2, R>
00134 ::relation_with(const Generator& g) const {
00135 reduce();
00136 if (Poly_Gen_Relation::nothing() == d1.relation_with(g)
00137 || Poly_Gen_Relation::nothing() == d2.relation_with(g))
00138 return Poly_Gen_Relation::nothing();
00139 else
00140 return Poly_Gen_Relation::subsumes();
00141 }
00142
00143 template <typename D1, typename D2, typename R>
00144 Poly_Con_Relation
00145 Partially_Reduced_Product<D1, D2, R>
00146 ::relation_with(const Constraint& c) const {
00147 reduce();
00148 Poly_Con_Relation relation1 = d1.relation_with(c);
00149 Poly_Con_Relation relation2 = d2.relation_with(c);
00150
00151 Poly_Con_Relation result = Poly_Con_Relation::nothing();
00152
00153 if (relation1.implies(Poly_Con_Relation::is_included()))
00154 result = result && Poly_Con_Relation::is_included();
00155 else if (relation2.implies(Poly_Con_Relation::is_included()))
00156 result = result && Poly_Con_Relation::is_included();
00157 if (relation1.implies(Poly_Con_Relation::saturates()))
00158 result = result && Poly_Con_Relation::saturates();
00159 else if (relation2.implies(Poly_Con_Relation::saturates()))
00160 result = result && Poly_Con_Relation::saturates();
00161 if (relation1.implies(Poly_Con_Relation::is_disjoint()))
00162 result = result && Poly_Con_Relation::is_disjoint();
00163 else if (relation2.implies(Poly_Con_Relation::is_disjoint()))
00164 result = result && Poly_Con_Relation::is_disjoint();
00165
00166 return result;
00167 }
00168
00169 template <typename D1, typename D2, typename R>
00170 Poly_Con_Relation
00171 Partially_Reduced_Product<D1, D2, R>
00172 ::relation_with(const Congruence& cg) const {
00173 reduce();
00174 Poly_Con_Relation relation1 = d1.relation_with(cg);
00175 Poly_Con_Relation relation2 = d2.relation_with(cg);
00176
00177 Poly_Con_Relation result = Poly_Con_Relation::nothing();
00178
00179 if (relation1.implies(Poly_Con_Relation::is_included()))
00180 result = result && Poly_Con_Relation::is_included();
00181 else if (relation2.implies(Poly_Con_Relation::is_included()))
00182 result = result && Poly_Con_Relation::is_included();
00183 if (relation1.implies(Poly_Con_Relation::saturates()))
00184 result = result && Poly_Con_Relation::saturates();
00185 else if (relation2.implies(Poly_Con_Relation::saturates()))
00186 result = result && Poly_Con_Relation::saturates();
00187 if (relation1.implies(Poly_Con_Relation::is_disjoint()))
00188 result = result && Poly_Con_Relation::is_disjoint();
00189 else if (relation2.implies(Poly_Con_Relation::is_disjoint()))
00190 result = result && Poly_Con_Relation::is_disjoint();
00191
00192 return result;
00193 }
00194
00195 template <typename D1, typename D2, typename R>
00196 bool
00197 Partially_Reduced_Product<D1, D2, R>
00198 ::maximize(const Linear_Expression& expr,
00199 Coefficient& sup_n,
00200 Coefficient& sup_d,
00201 bool& maximum) const {
00202 reduce();
00203 if (is_empty())
00204 return false;
00205 Coefficient sup1_n;
00206 Coefficient sup1_d;
00207 Coefficient sup2_n;
00208 Coefficient sup2_d;
00209 bool maximum1;
00210 bool maximum2;
00211 bool r1 = d1.maximize(expr, sup1_n, sup1_d, maximum1);
00212 bool r2 = d2.maximize(expr, sup2_n, sup2_d, maximum2);
00213
00214 if (!r1 && !r2)
00215 return false;
00216
00217 if (!r1) {
00218 sup_n = sup2_n;
00219 sup_d = sup2_d;
00220 maximum = maximum2;
00221 return true;
00222 }
00223
00224 if (!r2) {
00225 sup_n = sup1_n;
00226 sup_d = sup1_d;
00227 maximum = maximum1;
00228 return true;
00229 }
00230
00231 if (sup2_d * sup1_n >= sup1_d * sup2_n) {
00232 sup_n = sup1_n;
00233 sup_d = sup1_d;
00234 maximum = maximum1;
00235 }
00236 else {
00237 sup_n = sup2_n;
00238 sup_d = sup2_d;
00239 maximum = maximum2;
00240 }
00241 return true;
00242 }
00243
00244 template <typename D1, typename D2, typename R>
00245 bool
00246 Partially_Reduced_Product<D1, D2, R>
00247 ::minimize(const Linear_Expression& expr,
00248 Coefficient& inf_n,
00249 Coefficient& inf_d,
00250 bool& minimum) const {
00251 reduce();
00252 if (is_empty())
00253 return false;
00254 Coefficient inf1_n;
00255 Coefficient inf1_d;
00256 Coefficient inf2_n;
00257 Coefficient inf2_d;
00258 bool minimum1;
00259 bool minimum2;
00260 bool r1 = d1.minimize(expr, inf1_n, inf1_d, minimum1);
00261 bool r2 = d2.minimize(expr, inf2_n, inf2_d, minimum2);
00262
00263 if (!r1 && !r2)
00264 return false;
00265
00266 if (!r1) {
00267 inf_n = inf2_n;
00268 inf_d = inf2_d;
00269 minimum = minimum2;
00270 return true;
00271 }
00272
00273 if (!r2) {
00274 inf_n = inf1_n;
00275 inf_d = inf1_d;
00276 minimum = minimum1;
00277 return true;
00278 }
00279
00280 if (inf2_d * inf1_n <= inf1_d * inf2_n) {
00281 inf_n = inf1_n;
00282 inf_d = inf1_d;
00283 minimum = minimum1;
00284 }
00285 else {
00286 inf_n = inf2_n;
00287 inf_d = inf2_d;
00288 minimum = minimum2;
00289 }
00290 return true;
00291 }
00292
00293 template <typename D1, typename D2, typename R>
00294 bool
00295 Partially_Reduced_Product<D1, D2, R>
00296 ::maximize(const Linear_Expression& expr,
00297 Coefficient& sup_n,
00298 Coefficient& sup_d,
00299 bool& maximum,
00300 Generator& pnt) const {
00301 reduce();
00302 if (is_empty())
00303 return false;
00304 Coefficient sup1_n;
00305 Coefficient sup1_d;
00306 Coefficient sup2_n;
00307 Coefficient sup2_d;
00308 bool maximum1;
00309 bool maximum2;
00310 Generator pnt1(point());
00311 Generator pnt2(point());
00312 bool r1 = d1.maximize(expr, sup1_n, sup1_d, maximum1, pnt1);
00313 bool r2 = d2.maximize(expr, sup2_n, sup2_d, maximum2, pnt2);
00314
00315 if (!r1 && !r2)
00316 return false;
00317
00318 if (!r1) {
00319 sup_n = sup2_n;
00320 sup_d = sup2_d;
00321 maximum = maximum2;
00322 pnt = pnt2;
00323 return true;
00324 }
00325
00326 if (!r2) {
00327 sup_n = sup1_n;
00328 sup_d = sup1_d;
00329 maximum = maximum1;
00330 pnt = pnt1;
00331 return true;
00332 }
00333
00334 if (sup2_d * sup1_n >= sup1_d * sup2_n) {
00335 sup_n = sup1_n;
00336 sup_d = sup1_d;
00337 maximum = maximum1;
00338 pnt = pnt1;
00339 }
00340 else {
00341 sup_n = sup2_n;
00342 sup_d = sup2_d;
00343 maximum = maximum2;
00344 pnt = pnt2;
00345 }
00346 return true;
00347 }
00348
00349 template <typename D1, typename D2, typename R>
00350 bool
00351 Partially_Reduced_Product<D1, D2, R>
00352 ::minimize(const Linear_Expression& expr,
00353 Coefficient& inf_n,
00354 Coefficient& inf_d,
00355 bool& minimum,
00356 Generator& pnt) const {
00357 reduce();
00358 if (is_empty())
00359 return false;
00360 Coefficient inf1_n;
00361 Coefficient inf1_d;
00362 Coefficient inf2_n;
00363 Coefficient inf2_d;
00364 bool minimum1;
00365 bool minimum2;
00366 Generator pnt1(point());
00367 Generator pnt2(point());
00368 bool r1 = d1.minimize(expr, inf1_n, inf1_d, minimum1, pnt1);
00369 bool r2 = d2.minimize(expr, inf2_n, inf2_d, minimum2, pnt2);
00370
00371 if (!r1 && !r2)
00372 return false;
00373
00374 if (!r1) {
00375 inf_n = inf2_n;
00376 inf_d = inf2_d;
00377 minimum = minimum2;
00378 pnt = pnt2;
00379 return true;
00380 }
00381
00382 if (!r2) {
00383 inf_n = inf1_n;
00384 inf_d = inf1_d;
00385 minimum = minimum1;
00386 pnt = pnt1;
00387 return true;
00388 }
00389
00390 if (inf2_d * inf1_n <= inf1_d * inf2_n) {
00391 inf_n = inf1_n;
00392 inf_d = inf1_d;
00393 minimum = minimum1;
00394 pnt = pnt1;
00395 }
00396 else {
00397 inf_n = inf2_n;
00398 inf_d = inf2_d;
00399 minimum = minimum2;
00400 pnt = pnt2;
00401 }
00402 return true;
00403 }
00404
00405 template <typename D1, typename D2, typename R>
00406 inline bool
00407 Partially_Reduced_Product<D1, D2, R>::OK() const {
00408 if (reduced) {
00409 Partially_Reduced_Product<D1, D2, R> pd1 = *this;
00410 Partially_Reduced_Product<D1, D2, R> pd2 = *this;
00411
00412 pd1.clear_reduced_flag();
00413 pd1.reduce();
00414 if (pd1 != pd2)
00415 return false;
00416 }
00417 return d1.OK() && d2.OK();
00418 }
00419
00420 template <typename D1, typename D2, typename R>
00421 bool
00422 Partially_Reduced_Product<D1, D2, R>::ascii_load(std::istream& s) {
00423 const char yes = '+';
00424 const char no = '-';
00425 std::string str;
00426 if (!(s >> str) || str != "Partially_Reduced_Product")
00427 return false;
00428 if (!(s >> str)
00429 || (str[0] != yes && str[0] != no)
00430 || str.substr(1) != "reduced")
00431 return false;
00432 reduced = (str[0] == yes);
00433 return ((s >> str) && str == "Domain"
00434 && (s >> str) && str == "1:"
00435 && d1.ascii_load(s)
00436 && (s >> str) && str == "Domain"
00437 && (s >> str) && str == "2:"
00438 && d2.ascii_load(s));
00439 }
00440
00441 }
00442
00443 namespace Parma_Polyhedra_Library {
00444
00445 template <typename D1, typename D2>
00446 inline
00447 Smash_Reduction<D1, D2>::Smash_Reduction() {
00448 }
00449
00450 template <typename D1, typename D2>
00451 void Smash_Reduction<D1, D2>::product_reduce(D1& d1, D2& d2) {
00452 if (d2.is_empty()) {
00453 if (!d1.is_empty()) {
00454 D1 new_d1(d1.space_dimension(), EMPTY);
00455 std::swap(d1, new_d1);
00456 }
00457 }
00458 else if (d1.is_empty()) {
00459 D2 new_d2(d2.space_dimension(), EMPTY);
00460 std::swap(d2, new_d2);
00461 }
00462 }
00463
00464 template <typename D1, typename D2>
00465 inline
00466 Smash_Reduction<D1, D2>::~Smash_Reduction() {
00467 }
00468
00469 }
00470
00471 #endif // !defined(PPL_Partially_Reduced_Product_templates_hh)