PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00014 //***************************************************************************** 00015 00016 // include basic definitions 00017 #include "pbori_defs.h" 00018 00019 #ifndef CCuddDDFacade_h 00020 #define CCuddDDFacade_h 00021 00022 #include "cuddInt.h" 00023 #include "CApplyNodeFacade.h" 00024 #include "pbori_routines_cuddext.h" 00025 00026 #include "CExtrusivePtr.h" 00027 00028 // Getting iterator type for navigating through Cudd's ZDDs structure 00029 #include "CCuddNavigator.h" 00030 00031 // Getting iterator type for retrieving first term from Cudd's ZDDs 00032 #include "CCuddFirstIter.h" 00033 00034 // Getting iterator type for retrieving last term from Cudd's ZDDs 00035 #include "CCuddLastIter.h" 00036 00037 // Getting output iterator functionality 00038 #include "PBoRiOutIter.h" 00039 00040 // Getting error coe functionality 00041 #include "PBoRiGenericError.h" 00042 00043 // test input idx_type 00044 #include "CCheckedIdx.h" 00045 00046 #include "pbori_algo.h" 00047 #include "pbori_tags.h" 00048 #include "pbori_routines_hash.h" 00049 00050 #include <boost/preprocessor/cat.hpp> 00051 #include <boost/preprocessor/seq/for_each.hpp> 00052 #include <boost/preprocessor/facilities/expand.hpp> 00053 #include <boost/preprocessor/stringize.hpp> 00054 #include <stdexcept> 00055 #include <algorithm> 00056 #include <numeric> 00057 00058 BEGIN_NAMESPACE_PBORI 00059 00060 00062 template <class DataType> 00063 inline void 00064 extrusive_ptr_release(const DataType& data, DdNode* ptr) { 00065 if (ptr != NULL) { 00066 Cudd_RecursiveDerefZdd(data.getManager(), ptr); 00067 } 00068 } 00069 00071 template <class DataType> 00072 inline void 00073 extrusive_ptr_add_ref(const DataType&, DdNode* ptr) { 00074 if (ptr) Cudd_Ref(ptr); 00075 } 00076 00082 #define PBORI_NAME_Product product 00083 #define PBORI_NAME_UnateProduct unateProduct 00084 #define PBORI_NAME_WeakDiv weakDivide 00085 #define PBORI_NAME_Divide divide 00086 #define PBORI_NAME_WeakDivF weakDivF 00087 #define PBORI_NAME_DivideF divideF 00088 #define PBORI_NAME_Union unite 00089 #define PBORI_NAME_Intersect intersect 00090 #define PBORI_NAME_Diff diff 00091 #define PBORI_NAME_Subset1 subset1 00092 #define PBORI_NAME_Subset0 subset0 00093 #define PBORI_NAME_Change change 00094 00095 00096 #define PB_ZDD_APPLY(count, data, funcname) \ 00097 diagram_type BOOST_PP_CAT(PBORI_NAME_, funcname)(data rhs) const { \ 00098 return apply(BOOST_PP_CAT(Cudd_zdd, funcname), \ 00099 rhs); } 00100 00101 template <class RingType, class DiagramType> 00102 class CCuddDDFacade: 00103 public CApplyNodeFacade<DiagramType, DdNode*>, 00104 public CAuxTypes { 00105 00107 typedef CCuddDDFacade self; 00108 public: 00109 00111 typedef CTypes::ostream_type ostream_type; 00112 00114 typedef RingType ring_type; 00115 00117 typedef DiagramType diagram_type; 00118 00120 typedef DdNode node_type; 00121 00123 typedef node_type* node_ptr; 00124 00126 typedef CApplyNodeFacade<diagram_type, node_ptr> base; 00127 00129 typedef CCuddFirstIter first_iterator; 00130 00132 typedef CCuddLastIter last_iterator; 00133 00135 typedef CCuddNavigator navigator; 00136 00138 typedef valid_tag easy_equality_property; 00139 00141 typedef typename ring_type::mgr_type mgr_type; 00142 00144 typedef int cudd_idx_type; 00145 00147 typedef CCheckedIdx checked_idx_type; 00148 00150 CCuddDDFacade(const ring_type& ring, node_ptr node): 00151 p_node(ring, node) { 00152 checkAssumption(node != NULL); 00153 } 00154 00156 CCuddDDFacade(const ring_type& ring, const navigator& navi): 00157 p_node(ring, navi.getNode()) { 00158 checkAssumption(navi.isValid()); 00159 } 00161 CCuddDDFacade(const ring_type& ring, 00162 idx_type idx, navigator thenNavi, navigator elseNavi): 00163 p_node(ring, getNewNode(ring, idx, thenNavi, elseNavi)) { } 00164 00167 CCuddDDFacade(const ring_type& ring, 00168 idx_type idx, navigator navi): 00169 p_node(ring, getNewNode(ring, idx, navi, navi)) { } 00170 00172 CCuddDDFacade(idx_type idx, const self& thenDD, const self& elseDD): 00173 p_node(thenDD.ring(), getNewNode(idx, thenDD, elseDD)) { } 00174 00176 private: CCuddDDFacade(): p_node() {} 00177 public: 00179 CCuddDDFacade(const self &from): p_node(from.p_node) {} 00180 00182 ~CCuddDDFacade() {} 00183 00185 diagram_type& operator=(const diagram_type& rhs) { 00186 p_node = rhs.p_node; 00187 return static_cast<diagram_type&>(*this); 00188 } 00189 00192 BOOST_PP_SEQ_FOR_EACH(PB_ZDD_APPLY, const diagram_type&, 00193 (Product)(UnateProduct)(WeakDiv)(Divide)(WeakDivF)(DivideF) 00194 (Union)(Intersect)(Diff)) 00195 00196 BOOST_PP_SEQ_FOR_EACH(PB_ZDD_APPLY, int, (Subset1)(Subset0)(Change)) 00199 00200 bool implies(const self& rhs) const { 00201 return Cudd_zddDiffConst(getManager(), getNode(), rhs.getNode()) == 00202 Cudd_ReadZero(getManager()); 00203 } 00204 00205 00207 00208 std::ostream& printIntern(std::ostream& os) const { 00209 os << getNode() <<": "; 00210 00211 if (isZero()) 00212 os << "empty"; 00213 else 00214 os << nNodes() << " nodes " << count() << "terms"; 00215 00216 return os; 00217 00218 } 00219 void PrintMinterm() const { 00220 checkAssumption(apply(Cudd_zddPrintMinterm) == 1); 00221 } 00223 00225 size_type count() const { return dd_long_count<size_type>(navigation()); } 00226 00228 double countDouble() const { return dd_long_count<double>(navigation()); } 00229 00231 size_type rootIndex() const { return Cudd_NodeReadIndex(getNode()); } 00232 00234 size_type nNodes() const { return (size_type)(Cudd_zddDagSize(getNode())); } 00235 00237 size_type refCount() const { 00238 assert(getNode() != NULL); 00239 return Cudd_Regular(getNode())->ref; 00240 } 00241 00243 bool isZero() const { return getNode() == Cudd_ReadZero(getManager()); } 00244 00246 bool isOne() const { return getNode() == DD_ONE(getManager()); } 00247 00249 const ring_type& ring() const { return p_node.data(); } 00250 00252 node_ptr getNode() const { return p_node.get(); } 00253 00255 mgr_type* getManager() const { return p_node.data().getManager(); } 00256 00257 protected: 00258 00260 using base::apply; 00261 00262 00263 template <class ResultType> 00264 ResultType memApply(ResultType (*func)(mgr_type *, node_ptr)) const { 00265 ResultType result = apply(func); 00266 checkAssumption(result != (ResultType) CUDD_OUT_OF_MEM); 00267 return result; 00268 } 00269 00271 void checkAssumption(bool isValid) const { 00272 if UNLIKELY(!isValid) 00273 throw std::runtime_error(error_text(getManager())); 00274 } 00275 00277 template<class ManagerType, class ReverseIterator, class MultReverseIterator> 00278 diagram_type 00279 cudd_generate_multiples(const ManagerType& mgr, 00280 ReverseIterator start, ReverseIterator finish, 00281 MultReverseIterator multStart, 00282 MultReverseIterator multFinish) const { 00283 00284 // signed case 00285 while ((multStart != multFinish) && (*multStart > CTypes::max_idx)) 00286 ++multStart; 00287 // unsigned case 00288 while ((multStart != multFinish) && (*multStart < 0)) 00289 --multFinish; 00290 00291 DdNode* prev( (getManager())->one ); 00292 00293 DdNode* zeroNode( (getManager())->zero ); 00294 00295 Cudd_Ref(prev); 00296 while(start != finish) { 00297 00298 while((multStart != multFinish) && (*start < *multStart)) { 00299 00300 DdNode* result = cuddUniqueInterZdd( getManager(), *multStart, 00301 prev, prev ); 00302 00303 Cudd_Ref(result); 00304 Cudd_RecursiveDerefZdd(getManager(), prev); 00305 00306 prev = result; 00307 ++multStart; 00308 00309 }; 00310 00311 DdNode* result = cuddUniqueInterZdd( getManager(), *start, 00312 prev, zeroNode ); 00313 00314 Cudd_Ref(result); 00315 Cudd_RecursiveDerefZdd(getManager(), prev); 00316 00317 prev = result; 00318 00319 00320 if((multStart != multFinish) && (*start == *multStart)) 00321 ++multStart; 00322 00323 00324 ++start; 00325 } 00326 00327 while(multStart != multFinish) { 00328 00329 DdNode* result = cuddUniqueInterZdd( getManager(), *multStart, 00330 prev, prev ); 00331 00332 Cudd_Ref(result); 00333 Cudd_RecursiveDerefZdd(getManager(), prev); 00334 00335 prev = result; 00336 ++multStart; 00337 00338 }; 00339 00340 Cudd_Deref(prev); 00341 00342 00343 return diagram_type(mgr, prev); 00344 } 00345 00347 template<class ManagerType, class ReverseIterator> 00348 diagram_type 00349 cudd_generate_divisors(const ManagerType& mgr, 00350 ReverseIterator start, ReverseIterator finish) const { 00351 00352 00353 DdNode* prev= (getManager())->one; 00354 00355 Cudd_Ref(prev); 00356 while(start != finish) { 00357 00358 DdNode* result = cuddUniqueInterZdd( getManager(), 00359 *start, prev, prev); 00360 00361 Cudd_Ref(result); 00362 Cudd_RecursiveDerefZdd(getManager(), prev); 00363 00364 prev = result; 00365 ++start; 00366 } 00367 00368 Cudd_Deref(prev); 00370 return diagram_type(mgr, prev); 00371 00372 } 00373 public: 00374 00376 diagram_type Xor(const diagram_type& rhs) const { 00377 if (rhs.isZero()) 00378 return *this; 00379 00380 // return apply(pboriCudd_zddUnionXor, rhs); 00381 base::checkSameManager(rhs); 00382 return diagram_type(ring(), pboriCudd_zddUnionXor(getManager(), getNode(), rhs.getNode()) ); 00383 } 00384 00386 diagram_type divideFirst(const diagram_type& rhs) const { 00387 00388 diagram_type result(*this); 00389 PBoRiOutIter<diagram_type, idx_type, subset1_assign<diagram_type> > outiter(result); 00390 std::copy(rhs.firstBegin(), rhs.firstEnd(), outiter); 00391 00392 return result; 00393 } 00394 00395 00397 ostream_type& print(ostream_type& os) const { 00398 00399 printIntern(os) << std::endl;; 00400 PrintMinterm(); 00401 00402 return os; 00403 } 00404 00405 00407 size_type nSupport() const { return apply(Cudd_SupportSize); } 00408 00410 template<class VectorLikeType> 00411 void usedIndices(VectorLikeType& indices) const { 00412 00413 int* pIdx = usedIndices(); 00414 size_type nlen(ring().nVariables()); 00415 00416 indices = VectorLikeType(); 00417 indices.reserve(std::accumulate(pIdx, pIdx + nlen, size_type())); 00418 00419 for(size_type idx = 0; idx < nlen; ++idx) 00420 if (pIdx[idx] == 1){ 00421 indices.push_back(idx); 00422 } 00423 FREE(pIdx); 00424 } 00425 00427 int* usedIndices() const { return apply(Cudd_SupportIndex); } 00428 00430 first_iterator firstBegin() const { 00431 return first_iterator(navigation()); 00432 } 00433 00435 first_iterator firstEnd() const { 00436 return first_iterator(); 00437 } 00438 00440 last_iterator lastBegin() const { 00441 return last_iterator(getNode()); 00442 } 00443 00445 last_iterator lastEnd() const { 00446 return last_iterator(); 00447 } 00448 00450 diagram_type firstMultiples(const std::vector<idx_type>& input_multipliers) const { 00451 00452 std::set<idx_type> multipliers(input_multipliers.begin(), input_multipliers.end()); 00453 std::vector<idx_type> indices( std::distance(firstBegin(), firstEnd()) ); 00454 00455 std::copy( firstBegin(), firstEnd(), indices.begin() ); 00456 00457 return cudd_generate_multiples( ring(), 00458 indices.rbegin(), indices.rend(), 00459 multipliers.rbegin(), 00460 multipliers.rend() ); 00461 } 00462 00464 diagram_type firstDivisors() const { 00465 00466 std::vector<idx_type> indices( std::distance(firstBegin(), firstEnd()) ); 00467 00468 std::copy( firstBegin(), firstEnd(), indices.begin() ); 00469 00470 return cudd_generate_divisors(ring(), indices.rbegin(), indices.rend()); 00471 } 00472 00474 navigator navigation() const { 00475 return navigator(getNode()); 00476 } 00477 00479 bool_type isConstant() const { 00480 return (getNode()) && Cudd_IsConstant(getNode()); 00481 } 00482 00483 00484 00485 private: 00486 00488 static node_ptr 00489 getNewNode(const ring_type& ring, checked_idx_type idx, 00490 navigator thenNavi, navigator elseNavi) { 00491 00492 if ((idx >= *thenNavi) || (idx >= *elseNavi)) 00493 throw PBoRiGenericError<CTypes::invalid_ite>(); 00494 00495 return cuddZddGetNode(ring.getManager(), idx, 00496 thenNavi.getNode(), elseNavi.getNode()); 00497 } 00498 00500 static node_ptr 00501 getNewNode(idx_type idx, const self& thenDD, const self& elseDD) { 00502 thenDD.checkSameManager(elseDD); 00503 return getNewNode(thenDD.ring(), 00504 idx, thenDD.navigation(), elseDD.navigation()); 00505 } 00506 00507 private: 00509 CExtrusivePtr<ring_type, node_type> p_node; 00510 }; 00511 00512 00513 #undef PB_ZDD_APPLY 00514 00515 END_NAMESPACE_PBORI 00516 00517 #endif