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 #include "Pointset_Powerset.defs.hh"
00025 #include "Grid.defs.hh"
00026 #include <utility>
00027
00028 namespace PPL = Parma_Polyhedra_Library;
00029
00030 template <>
00031 void
00032 PPL::Pointset_Powerset<PPL::NNC_Polyhedron>
00033 ::difference_assign(const Pointset_Powerset& y) {
00034 Pointset_Powerset& x = *this;
00035
00036 x.omega_reduce();
00037 y.omega_reduce();
00038 Sequence new_sequence = x.sequence;
00039 for (const_iterator yi = y.begin(), y_end = y.end(); yi != y_end; ++yi) {
00040 const NNC_Polyhedron& py = yi->element();
00041 Sequence tmp_sequence;
00042 for (Sequence_const_iterator nsi = new_sequence.begin(),
00043 ns_end = new_sequence.end(); nsi != ns_end; ++nsi) {
00044 std::pair<NNC_Polyhedron, Pointset_Powerset<NNC_Polyhedron> > partition
00045 = linear_partition(py, nsi->element());
00046 const Pointset_Powerset<NNC_Polyhedron>& residues = partition.second;
00047
00048 std::copy(residues.begin(), residues.end(), back_inserter(tmp_sequence));
00049 }
00050 std::swap(tmp_sequence, new_sequence);
00051 }
00052 std::swap(x.sequence, new_sequence);
00053 x.reduced = false;
00054 assert(x.OK());
00055 }
00056
00057 template <>
00058 bool
00059 PPL::Pointset_Powerset<PPL::NNC_Polyhedron>
00060 ::geometrically_covers(const Pointset_Powerset& y) const {
00061 const Pointset_Powerset& x = *this;
00062 for (const_iterator yi = y.begin(), y_end = y.end(); yi != y_end; ++yi)
00063 if (!check_containment(yi->element(), x))
00064 return false;
00065 return true;
00066 }
00067
00069 bool
00070 PPL::check_containment(const NNC_Polyhedron& ph,
00071 const Pointset_Powerset<NNC_Polyhedron>& ps) {
00072 if (ph.is_empty())
00073 return true;
00074 Pointset_Powerset<NNC_Polyhedron> tmp(ph.space_dimension(), EMPTY);
00075 tmp.add_disjunct(ph);
00076 for (Pointset_Powerset<NNC_Polyhedron>::const_iterator
00077 i = ps.begin(), ps_end = ps.end(); i != ps_end; ++i) {
00078 const NNC_Polyhedron& pi = i->element();
00079 for (Pointset_Powerset<NNC_Polyhedron>::iterator
00080 j = tmp.begin(); j != tmp.end(); ) {
00081 const NNC_Polyhedron& pj = j->element();
00082 if (pi.contains(pj))
00083 j = tmp.drop_disjunct(j);
00084 else
00085 ++j;
00086 }
00087 if (tmp.empty())
00088 return true;
00089 else {
00090 Pointset_Powerset<NNC_Polyhedron> new_disjuncts(ph.space_dimension(),
00091 EMPTY);
00092 for (Pointset_Powerset<NNC_Polyhedron>::iterator
00093 j = tmp.begin(); j != tmp.end(); ) {
00094 const NNC_Polyhedron& pj = j->element();
00095 if (pj.is_disjoint_from(pi))
00096 ++j;
00097 else {
00098 std::pair<NNC_Polyhedron, Pointset_Powerset<NNC_Polyhedron> >
00099 partition = linear_partition(pi, pj);
00100 new_disjuncts.upper_bound_assign(partition.second);
00101 j = tmp.drop_disjunct(j);
00102 }
00103 }
00104 tmp.upper_bound_assign(new_disjuncts);
00105 }
00106 }
00107 return false;
00108 }
00109
00110
00111 namespace {
00112
00113 #ifdef PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS
00115
00121 #endif // defined(PPL_DOXYGEN_INCLUDE_IMPLEMENTATION_DETAILS)
00122 bool
00123 approximate_partition_aux(const PPL::Congruence& c,
00124 PPL::Grid& qq,
00125 PPL::Pointset_Powerset<PPL::Grid>& r) {
00126 using namespace PPL;
00127 const Coefficient& c_modulus = c.modulus();
00128 Grid qq_copy(qq);
00129 qq.add_congruence(c);
00130 if (qq.is_empty()) {
00131 r.add_disjunct(qq_copy);
00132 return true;
00133 }
00134
00135 Congruence_System cgs = qq.congruences();
00136 Congruence_System cgs_copy = qq_copy.congruences();
00137
00138
00139
00140 if (c_modulus == 0) {
00141 if (cgs.num_equalities() != cgs_copy.num_equalities()) {
00142 r.add_disjunct(qq_copy);
00143 return false;
00144 }
00145 return true;
00146 }
00147
00148
00149
00150
00151 if (cgs.num_proper_congruences() != cgs_copy.num_proper_congruences()) {
00152 r.add_disjunct(qq_copy);
00153 return false;
00154 }
00155
00156
00157
00158
00159 const Coefficient& c_inhomogeneous_term = c.inhomogeneous_term();
00160 Linear_Expression le(c);
00161 le -= c_inhomogeneous_term;
00162 TEMP_INTEGER(n);
00163 rem_assign(n, c_inhomogeneous_term, c_modulus);
00164 if (n < 0)
00165 n += c_modulus;
00166 TEMP_INTEGER(i);
00167 for (i = c_modulus; i-- > 0; )
00168 if (i != n) {
00169 Grid qqq(qq_copy);
00170 qqq.add_congruence((le+i %= 0) / c_modulus);
00171 if (!qqq.is_empty())
00172 r.add_disjunct(qqq);
00173 }
00174 return true;
00175 }
00176
00177 }
00178
00180 std::pair<PPL::Grid, PPL::Pointset_Powerset<PPL::Grid> >
00181 PPL::approximate_partition(const Grid& p, const Grid& q,
00182 bool& finite_partition) {
00183 using namespace PPL;
00184 finite_partition = true;
00185 Pointset_Powerset<Grid> r(p.space_dimension(), EMPTY);
00186
00187
00188 (void) q.minimized_congruences();
00189 Grid qq = q;
00190 const Congruence_System& pcs = p.congruences();
00191 for (Congruence_System::const_iterator i = pcs.begin(),
00192 pcs_end = pcs.end(); i != pcs_end; ++i)
00193 if (!approximate_partition_aux(*i, qq, r)) {
00194 finite_partition = false;
00195 Pointset_Powerset<Grid> s(q);
00196 return std::make_pair(qq, s);
00197 }
00198 return std::make_pair(qq, r);
00199 }
00200
00202 bool
00203 PPL::check_containment(const Grid& ph,
00204 const Pointset_Powerset<Grid>& ps) {
00205 if (ph.is_empty())
00206 return true;
00207 Pointset_Powerset<Grid> tmp(ph.space_dimension(), EMPTY);
00208 tmp.add_disjunct(ph);
00209 for (Pointset_Powerset<Grid>::const_iterator
00210 i = ps.begin(), ps_end = ps.end(); i != ps_end; ++i) {
00211 const Grid& pi = i->element();
00212 for (Pointset_Powerset<Grid>::iterator
00213 j = tmp.begin(); j != tmp.end(); ) {
00214 const Grid& pj = j->element();
00215 if (pi.contains(pj))
00216 j = tmp.drop_disjunct(j);
00217 else
00218 ++j;
00219 }
00220 if (tmp.empty())
00221 return true;
00222 else {
00223 Pointset_Powerset<Grid> new_disjuncts(ph.space_dimension(),
00224 EMPTY);
00225 for (Pointset_Powerset<Grid>::iterator
00226 j = tmp.begin(); j != tmp.end(); ) {
00227 const Grid& pj = j->element();
00228 if (pj.is_disjoint_from(pi))
00229 ++j;
00230 else {
00231 bool finite_partition;
00232 std::pair<Grid, Pointset_Powerset<Grid> >
00233 partition = approximate_partition(pi, pj, finite_partition);
00234
00235
00236
00237
00238
00239
00240
00241
00242 if (!finite_partition)
00243 break;
00244 new_disjuncts.upper_bound_assign(partition.second);
00245 j = tmp.drop_disjunct(j);
00246 }
00247 }
00248 tmp.upper_bound_assign(new_disjuncts);
00249 }
00250 }
00251 return false;
00252 }
00253
00254 template <>
00255 void
00256 PPL::Pointset_Powerset<PPL::Grid>
00257 ::difference_assign(const Pointset_Powerset& y) {
00258 Pointset_Powerset& x = *this;
00259
00260 x.omega_reduce();
00261 y.omega_reduce();
00262 Sequence new_sequence = x.sequence;
00263 for (const_iterator yi = y.begin(), y_end = y.end(); yi != y_end; ++yi) {
00264 const Grid& py = yi->element();
00265 Sequence tmp_sequence;
00266 for (Sequence_const_iterator nsi = new_sequence.begin(),
00267 ns_end = new_sequence.end(); nsi != ns_end; ++nsi) {
00268 bool finite_partition;
00269 std::pair<Grid, Pointset_Powerset<Grid> > partition
00270 = approximate_partition(py, nsi->element(), finite_partition);
00271 const Pointset_Powerset<Grid>& residues = partition.second;
00272
00273 std::copy(residues.begin(), residues.end(), back_inserter(tmp_sequence));
00274 }
00275 std::swap(tmp_sequence, new_sequence);
00276 }
00277 std::swap(x.sequence, new_sequence);
00278 x.reduced = false;
00279 assert(x.OK());
00280 }
00281
00282 template <>
00283 bool
00284 PPL::Pointset_Powerset<PPL::Grid>
00285 ::geometrically_covers(const Pointset_Powerset& y) const {
00286 const Pointset_Powerset& x = *this;
00287 for (const_iterator yi = y.begin(), y_end = y.end(); yi != y_end; ++yi)
00288 if (!check_containment(yi->element(), x))
00289 return false;
00290 return true;
00291 }
00292
00293 template <>
00294 template <>
00295 PPL::Pointset_Powerset<PPL::NNC_Polyhedron>
00296 ::Pointset_Powerset(const Pointset_Powerset<C_Polyhedron>& y,
00297 Complexity_Class)
00298 : Base(), space_dim(y.space_dimension()) {
00299 Pointset_Powerset& x = *this;
00300 for (Pointset_Powerset<C_Polyhedron>::const_iterator i = y.begin(),
00301 y_end = y.end(); i != y_end; ++i)
00302 x.sequence.push_back(Determinate<NNC_Polyhedron>
00303 (NNC_Polyhedron(i->element())));
00304 x.reduced = y.reduced;
00305 assert(x.OK());
00306 }
00307
00308 template <>
00309 template <>
00310 PPL::Pointset_Powerset<PPL::C_Polyhedron>
00311 ::Pointset_Powerset(const Pointset_Powerset<NNC_Polyhedron>& y,
00312 Complexity_Class)
00313 : Base(), space_dim(y.space_dimension()) {
00314 Pointset_Powerset& x = *this;
00315 for (Pointset_Powerset<NNC_Polyhedron>::const_iterator i = y.begin(),
00316 y_end = y.end(); i != y_end; ++i)
00317 x.sequence.push_back(Determinate<C_Polyhedron>
00318 (C_Polyhedron(i->element())));
00319
00320
00321
00322
00323
00324 x.reduced = false;
00325 assert(x.OK());
00326 }