00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023 #ifndef PPL_Powerset_templates_hh
00024 #define PPL_Powerset_templates_hh 1
00025
00026 #include <algorithm>
00027 #include <cassert>
00028 #include <iostream>
00029
00030 namespace Parma_Polyhedra_Library {
00031
00032 template <typename D>
00033 void
00034 Powerset<D>::collapse(const Sequence_iterator sink) {
00035 assert(sink != sequence.end());
00036 D& d = *sink;
00037 iterator x_sink = sink;
00038 iterator next_x_sink = x_sink;
00039 ++next_x_sink;
00040 iterator x_end = end();
00041 for (const_iterator xi = next_x_sink; xi != x_end; ++xi)
00042 d.upper_bound_assign(*xi);
00043
00044 drop_disjuncts(next_x_sink, x_end);
00045
00046
00047 for (iterator xi = begin(); xi != x_sink; )
00048 if (xi->definitely_entails(d))
00049 xi = drop_disjunct(xi);
00050 else
00051 ++xi;
00052
00053 assert(OK());
00054 }
00055
00056 template <typename D>
00057 void
00058 Powerset<D>::omega_reduce() const {
00059 if (reduced)
00060 return;
00061
00062 Powerset& x = const_cast<Powerset&>(*this);
00063
00064 for (iterator xi = x.begin(), x_end = x.end(); xi != x_end; )
00065 if (xi->is_bottom())
00066 xi = x.drop_disjunct(xi);
00067 else
00068 ++xi;
00069
00070 for (iterator xi = x.begin(); xi != x.end(); ) {
00071 const D& xv = *xi;
00072 bool dropping_xi = false;
00073 for (iterator yi = x.begin(); yi != x.end(); )
00074 if (xi == yi)
00075 ++yi;
00076 else {
00077 const D& yv = *yi;
00078 if (yv.definitely_entails(xv))
00079 yi = x.drop_disjunct(yi);
00080 else if (xv.definitely_entails(yv)) {
00081 dropping_xi = true;
00082 break;
00083 }
00084 else
00085 ++yi;
00086 }
00087 if (dropping_xi)
00088 xi = x.drop_disjunct(xi);
00089 else
00090 ++xi;
00091 if (abandon_expensive_computations && xi != x.end()) {
00092
00093 x.collapse(xi.base);
00094 break;
00095 }
00096 }
00097 reduced = true;
00098 assert(OK());
00099 }
00100
00101 template <typename D>
00102 void
00103 Powerset<D>::collapse(const unsigned max_disjuncts) {
00104 assert(max_disjuncts > 0);
00105
00106 omega_reduce();
00107 size_type n = size();
00108 if (n > max_disjuncts) {
00109
00110 iterator i = begin();
00111 std::advance(i, max_disjuncts-1);
00112
00113
00114 collapse(i.base);
00115 }
00116 assert(OK());
00117 assert(is_omega_reduced());
00118 }
00119
00120 template <typename D>
00121 bool
00122 Powerset<D>::check_omega_reduced() const {
00123 for (const_iterator x_begin = begin(), x_end = end(),
00124 xi = x_begin; xi != x_end; ++xi) {
00125 const D& xv = *xi;
00126 if (xv.is_bottom())
00127 return false;
00128 for (const_iterator yi = x_begin; yi != x_end; ++yi) {
00129 if (xi == yi)
00130 continue;
00131 const D& yv = *yi;
00132 if (xv.definitely_entails(yv) || yv.definitely_entails(xv))
00133 return false;
00134 }
00135 }
00136 return true;
00137 }
00138
00139 template <typename D>
00140 bool
00141 Powerset<D>::is_omega_reduced() const {
00142 if (!reduced && check_omega_reduced())
00143 reduced = true;
00144 return reduced;
00145 }
00146
00147 template <typename D>
00148 typename Powerset<D>::iterator
00149 Powerset<D>::add_non_bottom_disjunct(const D& d,
00150 iterator first,
00151 iterator last) {
00152 for (iterator xi = first; xi != last; ) {
00153 const D& xv = *xi;
00154 if (d.definitely_entails(xv))
00155 return first;
00156 else if (xv.definitely_entails(d)) {
00157 if (xi == first)
00158 ++first;
00159 xi = drop_disjunct(xi);
00160 }
00161 else
00162 ++xi;
00163 }
00164 sequence.push_back(d);
00165 return first;
00166 }
00167
00168 template <typename D>
00169 bool
00170 Powerset<D>::definitely_entails(const Powerset& y) const {
00171 const Powerset<D>& x = *this;
00172 bool found = true;
00173 for (const_iterator xi = x.begin(),
00174 x_end = x.end(); found && xi != x_end; ++xi) {
00175 found = false;
00176 for (const_iterator yi = y.begin(),
00177 y_end = y.end(); !found && yi != y_end; ++yi)
00178 found = (*xi).definitely_entails(*yi);
00179 }
00180 return found;
00181 }
00182
00184 template <typename D>
00185 bool
00186 operator==(const Powerset<D>& x, const Powerset<D>& y) {
00187 x.omega_reduce();
00188 y.omega_reduce();
00189 if (x.size() != y.size())
00190 return false;
00191
00192 Powerset<D> yy = y;
00193 for (typename Powerset<D>::const_iterator xi = x.begin(),
00194 x_end = x.end(); xi != x_end; ++xi) {
00195 typename Powerset<D>::iterator yyi = yy.begin();
00196 typename Powerset<D>::iterator yy_end = yy.end();
00197 yyi = std::find(yyi, yy_end, *xi);
00198 if (yyi == yy_end)
00199 return false;
00200 else
00201 yy.drop_disjunct(yyi);
00202 }
00203 return true;
00204 }
00205
00206 template <typename D>
00207 template <typename Binary_Operator_Assign>
00208 void
00209 Powerset<D>::pairwise_apply_assign(const Powerset& y,
00210 Binary_Operator_Assign op_assign) {
00211
00212 omega_reduce();
00213 y.omega_reduce();
00214 Sequence new_sequence;
00215 for (const_iterator xi = begin(), x_end = end(),
00216 y_begin = y.begin(), y_end = y.end(); xi != x_end; ++xi)
00217 for (const_iterator yi = y_begin; yi != y_end; ++yi) {
00218 D zi = *xi;
00219 op_assign(zi, *yi);
00220 if (!zi.is_bottom())
00221 new_sequence.push_back(zi);
00222 }
00223
00224 std::swap(sequence, new_sequence);
00225 reduced = false;
00226 }
00227
00228 template <typename D>
00229 void
00230 Powerset<D>::least_upper_bound_assign(const Powerset& y) {
00231
00232 omega_reduce();
00233 y.omega_reduce();
00234 iterator old_begin = begin();
00235 iterator old_end = end();
00236 for (const_iterator i = y.begin(), y_end = y.end(); i != y_end; ++i)
00237 old_begin = add_non_bottom_disjunct(*i, old_begin, old_end);
00238 }
00239
00240 namespace IO_Operators {
00241
00243 template <typename D>
00244 std::ostream&
00245 operator<<(std::ostream& s, const Powerset<D>& x) {
00246 if (x.is_bottom())
00247 s << "false";
00248 else if (x.is_top())
00249 s << "true";
00250 else
00251 for (typename Powerset<D>::const_iterator i = x.begin(),
00252 x_end = x.end(); i != x_end; ) {
00253 s << "{ " << *i++ << " }";
00254 if (i != x_end)
00255 s << ", ";
00256 }
00257 return s;
00258 }
00259
00260 }
00261
00262 template <typename D>
00263 memory_size_type
00264 Powerset<D>::external_memory_in_bytes() const {
00265 memory_size_type bytes = 0;
00266 for (const_iterator xi = begin(), x_end = end(); xi != x_end; ++xi) {
00267 bytes += xi->total_memory_in_bytes();
00268
00269
00270
00271 bytes += 2*sizeof(D*);
00272 }
00273 return bytes;
00274 }
00275
00276 template <typename D>
00277 bool
00278 Powerset<D>::OK(const bool disallow_bottom) const {
00279 for (const_iterator xi = begin(), x_end = end(); xi != x_end; ++xi) {
00280 if (!xi->OK())
00281 return false;
00282 if (disallow_bottom && xi->is_bottom()) {
00283 #ifndef NDEBUG
00284 std::cerr << "Bottom element in powerset!"
00285 << std::endl;
00286 #endif
00287 return false;
00288 }
00289 }
00290 if (reduced && !check_omega_reduced()) {
00291 #ifndef NDEBUG
00292 std::cerr << "Powerset claims to be reduced, but it is not!"
00293 << std::endl;
00294 #endif
00295 return false;
00296 }
00297 return true;
00298 }
00299
00300 }
00301
00302 #endif // !defined(PPL_Powerset_templates_hh)