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_preserve_reduction(const D& d,
00150 iterator first,
00151 iterator last) {
00152 assert(!d.is_bottom());
00153 for (iterator xi = first; xi != last; ) {
00154 const D& xv = *xi;
00155 if (d.definitely_entails(xv))
00156 return first;
00157 else if (xv.definitely_entails(d)) {
00158 if (xi == first)
00159 ++first;
00160 xi = drop_disjunct(xi);
00161 }
00162 else
00163 ++xi;
00164 }
00165 sequence.push_back(d);
00166 assert(OK());
00167 return first;
00168 }
00169
00170 template <typename D>
00171 bool
00172 Powerset<D>::definitely_entails(const Powerset& y) const {
00173 const Powerset<D>& x = *this;
00174 bool found = true;
00175 for (const_iterator xi = x.begin(),
00176 x_end = x.end(); found && xi != x_end; ++xi) {
00177 found = false;
00178 for (const_iterator yi = y.begin(),
00179 y_end = y.end(); !found && yi != y_end; ++yi)
00180 found = (*xi).definitely_entails(*yi);
00181 }
00182 return found;
00183 }
00184
00186 template <typename D>
00187 bool
00188 operator==(const Powerset<D>& x, const Powerset<D>& y) {
00189 x.omega_reduce();
00190 y.omega_reduce();
00191 if (x.size() != y.size())
00192 return false;
00193
00194 Powerset<D> yy = y;
00195 for (typename Powerset<D>::const_iterator xi = x.begin(),
00196 x_end = x.end(); xi != x_end; ++xi) {
00197 typename Powerset<D>::iterator yyi = yy.begin();
00198 typename Powerset<D>::iterator yy_end = yy.end();
00199 yyi = std::find(yyi, yy_end, *xi);
00200 if (yyi == yy_end)
00201 return false;
00202 else
00203 yy.drop_disjunct(yyi);
00204 }
00205 return true;
00206 }
00207
00208 template <typename D>
00209 template <typename Binary_Operator_Assign>
00210 void
00211 Powerset<D>::pairwise_apply_assign(const Powerset& y,
00212 Binary_Operator_Assign op_assign) {
00213
00214 omega_reduce();
00215 y.omega_reduce();
00216 Sequence new_sequence;
00217 for (const_iterator xi = begin(), x_end = end(),
00218 y_begin = y.begin(), y_end = y.end(); xi != x_end; ++xi)
00219 for (const_iterator yi = y_begin; yi != y_end; ++yi) {
00220 D zi = *xi;
00221 op_assign(zi, *yi);
00222 if (!zi.is_bottom())
00223 new_sequence.push_back(zi);
00224 }
00225
00226 std::swap(sequence, new_sequence);
00227 reduced = false;
00228 assert(OK());
00229 }
00230
00231 template <typename D>
00232 void
00233 Powerset<D>::least_upper_bound_assign(const Powerset& y) {
00234
00235 omega_reduce();
00236 y.omega_reduce();
00237 iterator old_begin = begin();
00238 iterator old_end = end();
00239 for (const_iterator i = y.begin(), y_end = y.end(); i != y_end; ++i)
00240 old_begin = add_non_bottom_disjunct_preserve_reduction(*i,
00241 old_begin,
00242 old_end);
00243 assert(OK());
00244 }
00245
00246 namespace IO_Operators {
00247
00249 template <typename D>
00250 std::ostream&
00251 operator<<(std::ostream& s, const Powerset<D>& x) {
00252 if (x.is_bottom())
00253 s << "false";
00254 else if (x.is_top())
00255 s << "true";
00256 else
00257 for (typename Powerset<D>::const_iterator i = x.begin(),
00258 x_end = x.end(); i != x_end; ) {
00259 s << "{ " << *i++ << " }";
00260 if (i != x_end)
00261 s << ", ";
00262 }
00263 return s;
00264 }
00265
00266 }
00267
00268 template <typename D>
00269 memory_size_type
00270 Powerset<D>::external_memory_in_bytes() const {
00271 memory_size_type bytes = 0;
00272 for (const_iterator xi = begin(), x_end = end(); xi != x_end; ++xi) {
00273 bytes += xi->total_memory_in_bytes();
00274
00275
00276
00277 bytes += 2*sizeof(D*);
00278 }
00279 return bytes;
00280 }
00281
00282 template <typename D>
00283 bool
00284 Powerset<D>::OK(const bool disallow_bottom) const {
00285 for (const_iterator xi = begin(), x_end = end(); xi != x_end; ++xi) {
00286 if (!xi->OK())
00287 return false;
00288 if (disallow_bottom && xi->is_bottom()) {
00289 #ifndef NDEBUG
00290 std::cerr << "Bottom element in powerset!"
00291 << std::endl;
00292 #endif
00293 return false;
00294 }
00295 }
00296 if (reduced && !check_omega_reduced()) {
00297 #ifndef NDEBUG
00298 std::cerr << "Powerset claims to be reduced, but it is not!"
00299 << std::endl;
00300 #endif
00301 return false;
00302 }
00303 return true;
00304 }
00305
00306 }
00307
00308 #endif // !defined(PPL_Powerset_templates_hh)