00001
00002
00160
00161
00162
00163 #include "pbori_defs.h"
00164
00165
00166 #include "CDDInterface.h"
00167
00168
00169 #include "pbori_func.h"
00170 #include "BooleRing.h"
00171
00172
00173 #ifndef BooleSet_h_
00174 #define BooleSet_h_
00175
00176 BEGIN_NAMESPACE_PBORI
00177
00179 class BooleMonomial;
00180 class BooleExponent;
00181
00182 template<class OrderType, class NavigatorType, class MonomType>
00183 class CGenericIter;
00184
00185 class LexOrder;
00186
00187 template<class OrderType, class NavigatorType, class MonomType>
00188 class CReverseIter;
00189
00190
00191 #define PBORI_CONST_DDFUNCS(func) \
00192 self func(const self& rhs) const { return self(base::func(rhs.diagram())); }
00193
00194 #define PBORI_DDFUNCS(func) \
00195 self& func(const self& rhs) { base::func(rhs.diagram()); return *this; }
00196
00197 #define PBORI_CONST_DDFUNCS_IDX(func) \
00198 self func(idx_type idx) const { return self(base::func(idx)); }
00199
00200 #define PBORI_DDFUNCS_IDX(func) \
00201 self& func(idx_type idx) { base::func(idx); return *this; }
00202
00203
00204 class BooleSet:
00205 public CTypes::dd_type {
00206
00207 public:
00209 typedef BooleSet self;
00210
00212 typedef CTypes::dd_type base;
00213
00215 typedef base dd_type;
00216
00217 typedef base::navigator navigator;
00218 typedef base::size_type size_type;
00219 typedef base::idx_type idx_type;
00220
00222 typedef BooleMonomial term_type;
00223
00225 typedef BooleExponent exp_type;
00226
00228 typedef BooleRing ring_type;
00229
00231 typedef CGenericIter<LexOrder, navigator, term_type> const_iterator;
00232
00234 typedef CGenericIter<LexOrder, navigator, exp_type> exp_iterator;
00235
00237 typedef CReverseIter<LexOrder, navigator, term_type> const_reverse_iterator;
00238
00240 BooleSet();
00241
00243 BooleSet(const self& rhs): base(rhs) {}
00244
00246 BooleSet(const base& rhs): base(rhs) {}
00247
00249 BooleSet(idx_type idx, const self& first, const self& second):
00250 base(idx, first, second) {
00251
00252
00253 }
00254
00256 BooleSet(idx_type idx, navigator first, navigator second,
00257 const ring_type& ring):
00258 base(ring.manager(), idx, first, second) { }
00259
00261 BooleSet(idx_type idx, const self& rhs):
00262 base(rhs.ring().manager(), idx, rhs.navigation()) { }
00263
00265
00268
00270 BooleSet(navigator navi, const ring_type& ring):
00271 base(ring.manager().manager(), navi) { }
00272
00274 ~BooleSet() {}
00275
00277 const_iterator begin() const;
00278
00280 const_iterator end() const;
00281
00283 const_reverse_iterator rbegin() const;
00284
00286 const_reverse_iterator rend() const;
00287
00289 exp_iterator expBegin() const;
00290
00292 exp_iterator expEnd() const;
00293
00295 self& operator=(const self&);
00296
00298 using base::operator=;
00299
00301 term_type usedVariables() const;
00302
00304 exp_type usedVariablesExp() const;
00305
00307 self& addAssign(const term_type&);
00308
00310 self add(const term_type&) const;
00311
00313 bool_type owns(const term_type&) const;
00314
00316 bool_type owns(const exp_type&) const;
00317
00319 term_type lastLexicographicalTerm() const;
00320
00322 self divisorsOf(const term_type& rhs) const;
00323
00325 self divisorsOf(const exp_type& rhs) const;
00326
00328 self firstDivisorsOf(const self& rhs) const;
00329
00331 self multiplesOf(const term_type& rhs) const;
00332
00334 self divide(const term_type& rhs) const;
00335
00337 self& divideAssign(const term_type& rhs);
00338
00340 bool_type hasTermOfVariables(const term_type& rhs) const;
00341
00343 self minimalElements() const;
00344
00346 using base::ownsOne;
00347
00349 bool_type isSingleton() const { return dd_is_singleton(navigation()); }
00350
00352 bool_type isSingletonOrPair() const {
00353 return dd_is_singleton_or_pair(navigation());
00354 }
00355
00357 bool_type isPair() const { return dd_is_pair(navigation()); }
00358
00360 self existAbstract(const term_type& rhs) const;
00361
00363 const dd_type& diagram() const { return dynamic_cast<const dd_type&>(*this); }
00364
00366 self ite(const self& then_dd, const self& else_dd) {
00367 return self(base::ite(then_dd.diagram(), else_dd.diagram()));
00368 };
00369
00371 self& iteAssign(const self& then_dd, const self& else_dd) {
00372 base::iteAssign(then_dd.diagram(), else_dd.diagram());
00373 return *this;
00374 };
00375
00377 self cartesianProduct(const self& rhs) const {
00378 return base::unateProduct(rhs.diagram());
00379 };
00380
00382
00383 PBORI_CONST_DDFUNCS_IDX(subset0)
00384 PBORI_CONST_DDFUNCS_IDX(subset1)
00385 PBORI_CONST_DDFUNCS_IDX(change)
00386
00387
00388 PBORI_CONST_DDFUNCS(unite)
00389 PBORI_CONST_DDFUNCS(diff)
00390 PBORI_CONST_DDFUNCS(diffConst)
00391 PBORI_CONST_DDFUNCS(intersect)
00392 PBORI_CONST_DDFUNCS(product)
00393 PBORI_CONST_DDFUNCS(dotProduct)
00394 PBORI_CONST_DDFUNCS(Xor)
00395 PBORI_CONST_DDFUNCS(ddDivide)
00396 PBORI_CONST_DDFUNCS(weakDivide)
00397 PBORI_CONST_DDFUNCS(divideFirst)
00398
00400 PBORI_DDFUNCS_IDX(subset0Assign)
00401 PBORI_DDFUNCS_IDX(subset1Assign)
00402 PBORI_DDFUNCS_IDX(changeAssign)
00403
00404 PBORI_DDFUNCS(uniteAssign)
00405 PBORI_DDFUNCS(diffAssign)
00406 PBORI_DDFUNCS(diffConstAssign)
00407 PBORI_DDFUNCS(intersectAssign)
00408 PBORI_DDFUNCS(productAssign)
00409 PBORI_DDFUNCS(dotProductAssign)
00410 PBORI_DDFUNCS(ddDivideAssign)
00411 PBORI_DDFUNCS(weakDivideAssign)
00412 PBORI_DDFUNCS(divideFirstAssign)
00414
00416 bool_type contains(const self& rhs) const {
00417 return base::diffConst(rhs).emptiness();
00418 }
00419
00421 using base::hash;
00422
00424 using base::stableHash;
00425
00427 ostream_type& print(ostream_type&) const;
00428
00430 self emptyElement() const { return base::emptyElement(); }
00431
00433 size_type countIndex(idx_type idx) const;
00434
00436 double countIndexDouble(idx_type idx) const ;
00437
00439 ring_type ring() const { return ring_type(base::manager()); }
00440
00442 bool_type containsDivisorsOfDecDeg(const term_type& rhs) const;
00443
00445 bool_type containsDivisorsOfDecDeg(const exp_type& rhs) const;
00446 };
00447
00449 inline BooleSet::ostream_type&
00450 operator<<( BooleSet::ostream_type& os, const BooleSet& bset ) {
00451 return bset.print(os);
00452 }
00453 END_NAMESPACE_PBORI
00454
00455 #endif