00001
00002
00014
00015
00016 #ifndef polybori_diagram_CCuddDDFacade_h
00017 #define polybori_diagram_CCuddDDFacade_h
00018
00019
00020 #include <polybori/pbori_defs.h>
00021
00022 #include <polybori/cudd/cudd.h>
00023 #include <polybori/cudd/prefix.h>
00024 #include "CApplyNodeFacade.h"
00025 #include "CNodeCounter.h"
00026
00027 #include <polybori/routines/pbori_routines_cuddext.h>
00028 #include <polybori/common/CExtrusivePtr.h>
00029
00030
00031 #include <polybori/iterators/CCuddNavigator.h>
00032
00033
00034 #include <polybori/iterators/CCuddFirstIter.h>
00035
00036
00037 #include <polybori/iterators/CCuddLastIter.h>
00038
00039
00040 #include <polybori/iterators/PBoRiOutIter.h>
00041
00042
00043 #include <polybori/except/PBoRiGenericError.h>
00044
00045
00046 #include <polybori/common/CCheckedIdx.h>
00047
00048 #include <polybori/routines/pbori_algo.h>
00049 #include <polybori/common/tags.h>
00050 #include <polybori/routines/pbori_routines_hash.h>
00051
00052 #include <boost/preprocessor/cat.hpp>
00053 #include <boost/preprocessor/seq/for_each.hpp>
00054 #include <boost/preprocessor/facilities/expand.hpp>
00055 #include <boost/preprocessor/stringize.hpp>
00056 #include <stdexcept>
00057 #include <algorithm>
00058 #include <numeric>
00059
00060 BEGIN_NAMESPACE_PBORI
00061
00062
00064 template <class DataType>
00065 inline void
00066 extrusive_ptr_release(const DataType& data, DdNode* ptr) {
00067 if (ptr != NULL) {
00068 PBORI_PREFIX(Cudd_RecursiveDerefZdd)(data.getManager(), ptr);
00069 }
00070 }
00071
00073 template <class DataType>
00074 inline void
00075 extrusive_ptr_add_ref(const DataType&, DdNode* ptr) {
00076 if (ptr) PBORI_PREFIX(Cudd_Ref)(ptr);
00077 }
00078
00084 #define PBORI_NAME_Product product
00085 #define PBORI_NAME_UnateProduct unateProduct
00086 #define PBORI_NAME_WeakDiv weakDivide
00087 #define PBORI_NAME_Divide divide
00088 #define PBORI_NAME_WeakDivF weakDivF
00089 #define PBORI_NAME_DivideF divideF
00090 #define PBORI_NAME_Union unite
00091 #define PBORI_NAME_Intersect intersect
00092 #define PBORI_NAME_Diff diff
00093 #define PBORI_NAME_Subset1 subset1
00094 #define PBORI_NAME_Subset0 subset0
00095 #define PBORI_NAME_Change change
00096
00097 #define PB_ZDD_APPLY(count, data, funcname) \
00098 diagram_type BOOST_PP_CAT(PBORI_NAME_, funcname)(data rhs) const { \
00099 return apply(BOOST_PP_CAT(PBORI_PREFIX(Cudd_zdd), funcname), \
00100 rhs); }
00101
00102 template <class RingType, class DiagramType>
00103 class CCuddDDFacade:
00104 public CApplyNodeFacade<DiagramType, DdNode*>,
00105 public CAuxTypes {
00106
00108 typedef CCuddDDFacade self;
00109 public:
00110
00112 typedef CTypes::ostream_type ostream_type;
00113
00115 typedef RingType ring_type;
00116
00118 typedef DiagramType diagram_type;
00119
00121 typedef DdNode node_type;
00122
00124 typedef node_type* node_ptr;
00125
00127 typedef CApplyNodeFacade<diagram_type, node_ptr> base;
00128
00130 typedef CCuddFirstIter first_iterator;
00131
00133 typedef CCuddLastIter last_iterator;
00134
00136 typedef CCuddNavigator navigator;
00137
00139 typedef valid_tag easy_equality_property;
00140
00142 typedef typename ring_type::mgr_type mgr_type;
00143
00145 typedef int cudd_idx_type;
00146
00148 typedef CCheckedIdx checked_idx_type;
00149
00151 CCuddDDFacade(const ring_type& ring, node_ptr node):
00152 p_node(ring, node) {
00153 checkAssumption(node != NULL);
00154 }
00155
00157 CCuddDDFacade(const ring_type& ring, const navigator& navi):
00158 p_node(ring, navi.getNode()) {
00159 checkAssumption(navi.isValid());
00160 }
00162 CCuddDDFacade(const ring_type& ring,
00163 idx_type idx, navigator thenNavi, navigator elseNavi):
00164 p_node(ring, getNewNode(ring, idx, thenNavi, elseNavi)) { }
00165
00168 CCuddDDFacade(const ring_type& ring,
00169 idx_type idx, navigator navi):
00170 p_node(ring, getNewNode(ring, idx, navi, navi)) { }
00171
00173 CCuddDDFacade(idx_type idx, const self& thenDD, const self& elseDD):
00174 p_node(thenDD.ring(), getNewNode(idx, thenDD, elseDD)) { }
00175
00177 private: CCuddDDFacade(): p_node() {}
00178 public:
00180 CCuddDDFacade(const self &from): p_node(from.p_node) {}
00181
00183 ~CCuddDDFacade() {}
00184
00186 diagram_type& operator=(const diagram_type& rhs) {
00187 p_node = rhs.p_node;
00188 return static_cast<diagram_type&>(*this);
00189 }
00190
00193 BOOST_PP_SEQ_FOR_EACH(PB_ZDD_APPLY, const diagram_type&,
00194 (Product)(UnateProduct)(WeakDiv)(Divide)(WeakDivF)(DivideF)
00195 (Union)(Intersect)(Diff))
00196
00197 BOOST_PP_SEQ_FOR_EACH(PB_ZDD_APPLY, int, (Subset1)(Subset0)(Change))
00200
00201 bool implies(const self& rhs) const {
00202 return PBORI_PREFIX(Cudd_zddDiffConst)(getManager(), getNode(), rhs.getNode()) ==
00203 PBORI_PREFIX(Cudd_ReadZero)(getManager());
00204 }
00205
00206
00208
00209 std::ostream& printIntern(std::ostream& os) const {
00210 os << getNode() <<": ";
00211
00212 if (isZero())
00213 os << "empty";
00214 else
00215 os << nNodes() << " nodes " << count() << "terms";
00216
00217 return os;
00218
00219 }
00220 void PrintMinterm() const {
00221 checkAssumption(apply(PBORI_PREFIX(Cudd_zddPrintMinterm)) == 1);
00222 }
00224
00226 size_type count() const { return dd_long_count<size_type>(navigation()); }
00227
00229 double countDouble() const { return dd_long_count<double>(navigation()); }
00230
00232 size_type rootIndex() const { return PBORI_PREFIX(Cudd_NodeReadIndex)(getNode()); }
00233
00235 size_type nNodes() const { return CNodeCounter<navigator>()(navigation()); }
00236
00238 size_type refCount() const {
00239 PBORI_ASSERT(getNode() != NULL);
00240 return PBORI_PREFIX(Cudd_Regular)(getNode())->ref;
00241 }
00242
00244 bool isZero() const { return getNode() == PBORI_PREFIX(Cudd_ReadZero)(getManager()); }
00245
00247 bool isOne() const { return getNode() == DD_ONE(getManager()); }
00248
00250 const ring_type& ring() const { return p_node.data(); }
00251
00253 node_ptr getNode() const { return p_node.get(); }
00254
00256 mgr_type* getManager() const { return p_node.data().getManager(); }
00257
00258 protected:
00259
00261 using base::apply;
00262
00263
00264 template <class ResultType>
00265 ResultType memApply(ResultType (*func)(mgr_type *, node_ptr)) const {
00266 ResultType result = apply(func);
00267 checkAssumption(result != (ResultType) CUDD_OUT_OF_MEM);
00268 return result;
00269 }
00270
00272 void checkAssumption(bool isValid) const {
00273 if PBORI_UNLIKELY(!isValid)
00274 throw std::runtime_error(error_text(getManager()));
00275 }
00276
00278 template<class ManagerType, class ReverseIterator, class MultReverseIterator>
00279 diagram_type
00280 cudd_generate_multiples(const ManagerType& mgr,
00281 ReverseIterator start, ReverseIterator finish,
00282 MultReverseIterator multStart,
00283 MultReverseIterator multFinish) const {
00284
00285
00286 while ((multStart != multFinish) && (*multStart > CTypes::max_idx))
00287 ++multStart;
00288
00289 while ((multStart != multFinish) && (*multStart < 0))
00290 --multFinish;
00291
00292 DdNode* prev( (getManager())->one );
00293
00294 DdNode* zeroNode( (getManager())->zero );
00295
00296 PBORI_PREFIX(Cudd_Ref)(prev);
00297 while(start != finish) {
00298
00299 while((multStart != multFinish) && (*start < *multStart)) {
00300
00301 DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( getManager(), *multStart,
00302 prev, prev );
00303
00304 PBORI_PREFIX(Cudd_Ref)(result);
00305 PBORI_PREFIX(Cudd_RecursiveDerefZdd)(getManager(), prev);
00306
00307 prev = result;
00308 ++multStart;
00309
00310 };
00311
00312 DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( getManager(), *start,
00313 prev, zeroNode );
00314
00315 PBORI_PREFIX(Cudd_Ref)(result);
00316 PBORI_PREFIX(Cudd_RecursiveDerefZdd)(getManager(), prev);
00317
00318 prev = result;
00319
00320
00321 if((multStart != multFinish) && (*start == *multStart))
00322 ++multStart;
00323
00324
00325 ++start;
00326 }
00327
00328 while(multStart != multFinish) {
00329
00330 DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( getManager(), *multStart,
00331 prev, prev );
00332
00333 PBORI_PREFIX(Cudd_Ref)(result);
00334 PBORI_PREFIX(Cudd_RecursiveDerefZdd)(getManager(), prev);
00335
00336 prev = result;
00337 ++multStart;
00338
00339 };
00340
00341 PBORI_PREFIX(Cudd_Deref)(prev);
00342
00343
00344 return diagram_type(mgr, prev);
00345 }
00346
00348 template<class ManagerType, class ReverseIterator>
00349 diagram_type
00350 cudd_generate_divisors(const ManagerType& mgr,
00351 ReverseIterator start, ReverseIterator finish) const {
00352
00353
00354 DdNode* prev= (getManager())->one;
00355
00356 PBORI_PREFIX(Cudd_Ref)(prev);
00357 while(start != finish) {
00358
00359 DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( getManager(),
00360 *start, prev, prev);
00361
00362 PBORI_PREFIX(Cudd_Ref)(result);
00363 PBORI_PREFIX(Cudd_RecursiveDerefZdd)(getManager(), prev);
00364
00365 prev = result;
00366 ++start;
00367 }
00368
00369 PBORI_PREFIX(Cudd_Deref)(prev);
00371 return diagram_type(mgr, prev);
00372
00373 }
00374 public:
00375
00377 diagram_type Xor(const diagram_type& rhs) const {
00378 if (rhs.isZero())
00379 return *this;
00380
00381
00382 base::checkSameManager(rhs);
00383 return diagram_type(ring(), pboriCudd_zddUnionXor(getManager(), getNode(), rhs.getNode()) );
00384 }
00385
00387 diagram_type divideFirst(const diagram_type& rhs) const {
00388
00389 diagram_type result(*this);
00390 PBoRiOutIter<diagram_type, idx_type, subset1_assign<diagram_type> > outiter(result);
00391 std::copy(rhs.firstBegin(), rhs.firstEnd(), outiter);
00392
00393 return result;
00394 }
00395
00396
00398 ostream_type& print(ostream_type& os) const {
00399
00400 printIntern(os) << std::endl;;
00401 PrintMinterm();
00402
00403 return os;
00404 }
00405
00406
00408
00409
00411 first_iterator firstBegin() const {
00412 return first_iterator(navigation());
00413 }
00414
00416 first_iterator firstEnd() const {
00417 return first_iterator();
00418 }
00419
00421 last_iterator lastBegin() const {
00422 return last_iterator(getNode());
00423 }
00424
00426 last_iterator lastEnd() const {
00427 return last_iterator();
00428 }
00429
00431 diagram_type firstMultiples(const std::vector<idx_type>& input_multipliers) const {
00432
00433 std::set<idx_type> multipliers(input_multipliers.begin(), input_multipliers.end());
00434 std::vector<idx_type> indices( std::distance(firstBegin(), firstEnd()) );
00435
00436 std::copy( firstBegin(), firstEnd(), indices.begin() );
00437
00438 return cudd_generate_multiples( ring(),
00439 indices.rbegin(), indices.rend(),
00440 multipliers.rbegin(),
00441 multipliers.rend() );
00442 }
00443
00445 diagram_type firstDivisors() const {
00446
00447 std::vector<idx_type> indices( std::distance(firstBegin(), firstEnd()) );
00448
00449 std::copy( firstBegin(), firstEnd(), indices.begin() );
00450
00451 return cudd_generate_divisors(ring(), indices.rbegin(), indices.rend());
00452 }
00453
00455 navigator navigation() const {
00456 return navigator(getNode());
00457 }
00458
00460 bool_type isConstant() const {
00461 return (getNode()) && PBORI_PREFIX(Cudd_IsConstant)(getNode());
00462 }
00463
00464
00465
00466 private:
00467
00469 static node_ptr
00470 getNewNode(const ring_type& ring, checked_idx_type idx,
00471 navigator thenNavi, navigator elseNavi) {
00472
00473 if ((idx >= *thenNavi) || (idx >= *elseNavi))
00474 throw PBoRiGenericError<CTypes::invalid_ite>();
00475
00476 return PBORI_PREFIX(cuddZddGetNode)(ring.getManager(), idx,
00477 thenNavi.getNode(), elseNavi.getNode());
00478 }
00479
00481 static node_ptr
00482 getNewNode(idx_type idx, const self& thenDD, const self& elseDD) {
00483 thenDD.checkSameManager(elseDD);
00484 return getNewNode(thenDD.ring(),
00485 idx, thenDD.navigation(), elseDD.navigation());
00486 }
00487
00488 private:
00490 CExtrusivePtr<ring_type, node_type> p_node;
00491 };
00492
00493
00494 #undef PB_ZDD_APPLY
00495
00496 END_NAMESPACE_PBORI
00497
00498 #endif
