PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00014 //***************************************************************************** 00015 00016 #ifndef polybori_diagram_CCuddDDFacade_h 00017 #define polybori_diagram_CCuddDDFacade_h 00018 00019 // include basic definitions 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 // Getting iterator type for navigating through Cudd's ZDDs structure 00031 #include <polybori/iterators/CCuddNavigator.h> 00032 00033 // Getting iterator type for retrieving first term from Cudd's ZDDs 00034 #include <polybori/iterators/CCuddFirstIter.h> 00035 00036 // Getting iterator type for retrieving last term from Cudd's ZDDs 00037 #include <polybori/iterators/CCuddLastIter.h> 00038 00039 // Getting output iterator functionality 00040 #include <polybori/iterators/PBoRiOutIter.h> 00041 00042 // Getting error coe functionality 00043 #include <polybori/except/PBoRiGenericError.h> 00044 00045 // test input idx_type 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 // signed case 00286 while ((multStart != multFinish) && (*multStart > CTypes::max_idx)) 00287 ++multStart; 00288 // unsigned case 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 // return apply(pboriPBORI_PREFIX(Cudd_zddUnionXor), rhs); 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 // size_type nSupport() const { return apply(PBORI_PREFIX(PBORI_PREFIX(Cudd_SupportSize));) } 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