PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00220 //***************************************************************************** 00221 00222 #ifndef CDDInterface_h_ 00223 #define CDDInterface_h_ 00224 00225 #include "extrafwd.h" 00226 // load basic definitions 00227 #include "pbori_defs.h" 00228 00229 00230 00231 // Getting iterator type for navigating through Cudd's ZDDs structure 00232 #include "CCuddNavigator.h" 00233 00234 // Getting iterator type for retrieving first term from Cudd's ZDDs 00235 #include "CCuddFirstIter.h" 00236 00237 // Getting iterator type for retrieving last term from Cudd's ZDDs 00238 #include "CCuddLastIter.h" 00239 00240 // Getting functional for generating new Cudd's ZDD nodes 00241 #include "CCuddGetNode.h" 00242 00243 // Getting output iterator functionality 00244 #include "PBoRiOutIter.h" 00245 00246 // Getting error coe functionality 00247 #include "PBoRiGenericError.h" 00248 00249 // Cudd's internal definitions 00250 #include "cuddInt.h" 00251 00252 #include "pbori_algo.h" 00253 00254 #include "pbori_tags.h" 00255 #include "pbori_routines_hash.h" 00256 00257 // Using stl's vector 00258 #include <vector> 00259 #include <numeric> 00260 00261 #include "CCuddInterface.h" 00262 #include "pbori_traits.h" 00263 00264 BEGIN_NAMESPACE_PBORI 00265 00266 00267 inline Cudd* 00268 extract_manager(const Cudd& mgr) { 00269 return &const_cast<Cudd&>(mgr); 00270 } 00271 00272 inline CCuddInterface::mgrcore_ptr 00273 extract_manager(const CCuddInterface& mgr) { 00274 return mgr.managerCore(); 00275 } 00276 00277 template <class MgrType> 00278 inline const MgrType& 00279 extract_manager(const MgrType& mgr) { 00280 return mgr; 00281 } 00282 00283 inline Cudd& 00284 get_manager(Cudd* mgr) { 00285 return *mgr; 00286 } 00287 00288 template <class MgrType> 00289 inline const MgrType& 00290 get_manager(const MgrType& mgr) { 00291 return mgr; 00292 } 00300 template<class DDType> 00301 class CDDInterfaceBase { 00302 00303 public: 00304 00306 typedef DDType interfaced_type; 00307 00309 typedef CDDInterfaceBase<interfaced_type> self; 00310 00312 CDDInterfaceBase() : 00313 m_interfaced() {} 00314 00316 CDDInterfaceBase(const interfaced_type& interfaced) : 00317 m_interfaced(interfaced) {} 00318 00320 CDDInterfaceBase(const self& rhs) : 00321 m_interfaced(rhs.m_interfaced) {} 00322 00324 ~CDDInterfaceBase() {} 00325 00327 operator const interfaced_type&() const { return m_interfaced; } 00328 00329 protected: 00330 interfaced_type m_interfaced; 00331 }; 00332 00335 template<class CuddLikeZDD> 00336 class CDDInterface: 00337 public CDDInterfaceBase<CuddLikeZDD> { 00338 public: 00339 00341 typedef CuddLikeZDD interfaced_type; 00342 00344 typedef typename zdd_traits<interfaced_type>::manager_base manager_base; 00345 00347 typedef typename manager_traits<manager_base>::tmp_ref mgr_ref; 00348 00350 typedef typename manager_traits<manager_base>::core_type core_type; 00351 00353 typedef CDDManager<CCuddInterface> manager_type; 00354 00356 typedef CDDInterfaceBase<interfaced_type> base_type; 00357 typedef base_type base; 00358 using base::m_interfaced; 00359 00361 typedef CDDInterface<interfaced_type> self; 00362 00364 typedef CTypes::size_type size_type; 00365 00367 typedef CTypes::idx_type idx_type; 00368 00370 typedef CTypes::ostream_type ostream_type; 00371 00373 typedef CTypes::bool_type bool_type; 00374 00376 typedef CTypes::hash_type hash_type; 00377 00379 typedef CCuddFirstIter first_iterator; 00380 00382 typedef CCuddLastIter last_iterator; 00383 00385 typedef CCuddNavigator navigator; 00386 00388 typedef FILE* pretty_out_type; 00389 00391 typedef const char* filename_type; 00392 00394 typedef valid_tag easy_equality_property; 00395 00397 CDDInterface(): base_type() {} 00398 00400 CDDInterface(const self& rhs): base_type(rhs) {} 00401 00403 CDDInterface(const interfaced_type& rhs): base_type(rhs) {} 00404 00406 CDDInterface(const manager_base& mgr, const navigator& navi): 00407 base_type(self::newDiagram(mgr, navi)) {} 00408 00410 CDDInterface(const manager_base& mgr, 00411 idx_type idx, navigator thenNavi, navigator elseNavi): 00412 base_type( self::newNodeDiagram(mgr, idx, thenNavi, elseNavi) ) { 00413 } 00414 00417 CDDInterface(const manager_base& mgr, 00418 idx_type idx, navigator navi): 00419 base_type( self::newNodeDiagram(mgr, idx, navi, navi) ) { 00420 } 00421 00423 CDDInterface(idx_type idx, const self& thenDD, const self& elseDD): 00424 base_type( self::newNodeDiagram(thenDD.manager(), idx, 00425 thenDD.navigation(), 00426 elseDD.navigation()) ) { 00427 } 00428 00430 ~CDDInterface() {} 00431 00433 hash_type hash() const { 00434 return static_cast<hash_type>(reinterpret_cast<std::ptrdiff_t>(m_interfaced 00435 .getNode())); 00436 } 00437 00439 hash_type stableHash() const { 00440 return stable_hash_range(navigation()); 00441 } 00442 00444 self unite(const self& rhs) const { 00445 return self(base_type(m_interfaced.Union(rhs.m_interfaced))); 00446 }; 00447 00449 self& uniteAssign(const self& rhs) { 00450 m_interfaced = m_interfaced.Union(rhs.m_interfaced); 00451 return *this; 00452 }; 00454 self ite(const self& then_dd, const self& else_dd) const { 00455 return self(m_interfaced.Ite(then_dd, else_dd)); 00456 }; 00457 00459 self& iteAssign(const self& then_dd, const self& else_dd) { 00460 m_interfaced = m_interfaced.Ite(then_dd, else_dd); 00461 return *this; 00462 }; 00463 00465 self diff(const self& rhs) const { 00466 return m_interfaced.Diff(rhs.m_interfaced); 00467 }; 00468 00470 self& diffAssign(const self& rhs) { 00471 m_interfaced = m_interfaced.Diff(rhs.m_interfaced); 00472 return *this; 00473 }; 00474 00476 self diffConst(const self& rhs) const { 00477 return m_interfaced.DiffConst(rhs.m_interfaced); 00478 }; 00479 00481 self& diffConstAssign(const self& rhs) { 00482 m_interfaced = m_interfaced.DiffConst(rhs.m_interfaced); 00483 return *this; 00484 }; 00485 00487 self intersect(const self& rhs) const { 00488 return m_interfaced.Intersect(rhs.m_interfaced); 00489 }; 00490 00492 self& intersectAssign(const self& rhs) { 00493 m_interfaced = m_interfaced.Intersect(rhs.m_interfaced); 00494 return *this; 00495 }; 00496 00498 self product(const self& rhs) const { 00499 return m_interfaced.Product(rhs.m_interfaced); 00500 }; 00501 00503 self& productAssign(const self& rhs) { 00504 m_interfaced = m_interfaced.Product(rhs.m_interfaced); 00505 return *this; 00506 }; 00507 00509 self unateProduct(const self& rhs) const { 00510 return m_interfaced.UnateProduct(rhs.m_interfaced); 00511 }; 00512 00513 00514 00516 self dotProduct(const self& rhs) const { 00517 return interfaced_type(m_interfaced.manager(), 00518 Extra_zddDotProduct( 00519 manager().getManager(), 00520 m_interfaced.getNode(), 00521 rhs.m_interfaced.getNode())); 00522 } 00523 00524 self& dotProductAssign(const self& rhs){ 00525 m_interfaced=interfaced_type(m_interfaced.manager(), 00526 Extra_zddDotProduct( 00527 manager().getManager(), 00528 m_interfaced.getNode(), 00529 rhs.m_interfaced.getNode())); 00530 return *this; 00531 } 00532 00533 self Xor(const self& rhs) const { 00534 if (rhs.emptiness()) 00535 return *this; 00536 #ifdef PBORI_LOWLEVEL_XOR 00537 return interfaced_type(m_interfaced.manager(), 00538 pboriCudd_zddUnionXor( 00539 manager().getManager(), 00540 m_interfaced.getNode(), 00541 rhs.m_interfaced.getNode())); 00542 #else 00543 return interfaced_type(m_interfaced.manager(), 00544 Extra_zddUnionExor( 00545 manager().getManager(), 00546 m_interfaced.getNode(), 00547 rhs.m_interfaced.getNode())); 00548 #endif 00549 } 00550 00551 00553 self& unateProductAssign(const self& rhs) { 00554 m_interfaced = m_interfaced.UnateProduct(rhs.m_interfaced); 00555 return *this; 00556 }; 00557 00559 self subset0(idx_type idx) const { 00560 return m_interfaced.Subset0(idx); 00561 }; 00562 00564 self& subset0Assign(idx_type idx) { 00565 m_interfaced = m_interfaced.Subset0(idx); 00566 return *this; 00567 }; 00568 00570 self subset1(idx_type idx) const { 00571 return m_interfaced.Subset1(idx); 00572 }; 00573 00575 self& subset1Assign(idx_type idx) { 00576 m_interfaced = m_interfaced.Subset1(idx); 00577 return *this; 00578 }; 00579 00581 self change(idx_type idx) const { 00582 00583 return m_interfaced.Change(idx); 00584 }; 00585 00587 self& changeAssign(idx_type idx) { 00588 m_interfaced = m_interfaced.Change(idx); 00589 return *this; 00590 }; 00591 00593 self ddDivide(const self& rhs) const { 00594 return m_interfaced.Divide(rhs); 00595 }; 00596 00598 self& ddDivideAssign(const self& rhs) { 00599 m_interfaced = m_interfaced.Divide(rhs); 00600 return *this; 00601 }; 00603 self weakDivide(const self& rhs) const { 00604 return m_interfaced.WeakDiv(rhs); 00605 }; 00606 00608 self& weakDivideAssign(const self& rhs) { 00609 m_interfaced = m_interfaced.WeakDiv(rhs); 00610 return *this; 00611 }; 00612 00614 self& divideFirstAssign(const self& rhs) { 00615 00616 PBoRiOutIter<self, idx_type, subset1_assign<self> > outiter(*this); 00617 std::copy(rhs.firstBegin(), rhs.firstEnd(), outiter); 00618 00619 return *this; 00620 } 00621 00623 self divideFirst(const self& rhs) const { 00624 00625 self result(*this); 00626 result.divideFirstAssign(rhs); 00627 00628 return result; 00629 } 00630 00631 00633 size_type nNodes() const { 00634 return Cudd_zddDagSize(m_interfaced.getNode()); 00635 } 00636 00638 ostream_type& print(ostream_type& os) const { 00639 00640 FILE* oldstdout = manager().ReadStdout(); 00641 00643 if (os == std::cout) 00644 manager().SetStdout(stdout); 00645 else if (os == std::cerr) 00646 manager().SetStdout(stderr); 00647 00648 m_interfaced.print( Cudd_ReadZddSize(manager().getManager()) ); 00649 m_interfaced.PrintMinterm(); 00650 00651 manager().SetStdout(oldstdout); 00652 return os; 00653 } 00654 00656 void prettyPrint(pretty_out_type filehandle = stdout) const { 00657 DdNode* tmp = m_interfaced.getNode(); 00658 Cudd_zddDumpDot(m_interfaced.getManager(), 1, &tmp, 00659 NULL, NULL, filehandle); 00660 }; 00661 00663 bool_type prettyPrint(filename_type filename) const { 00664 00665 FILE* theFile = fopen( filename, "w"); 00666 if (theFile == NULL) 00667 return true; 00668 00669 prettyPrint(theFile); 00670 fclose(theFile); 00671 00672 return false; 00673 }; 00674 00676 bool_type operator==(const self& rhs) const { 00677 return (m_interfaced == rhs.m_interfaced); 00678 } 00679 00681 bool_type operator!=(const self& rhs) const { 00682 return (m_interfaced != rhs.m_interfaced); 00683 } 00684 00686 mgr_ref manager() const { 00687 return get_manager(m_interfaced.manager()); 00688 } 00689 core_type managerCore() const{ 00690 return m_interfaced.manager(); 00691 } 00693 size_type nSupport() const { 00694 return Cudd_SupportSize(manager().getManager(), m_interfaced.getNode()); 00695 } 00696 00697 #if 1 00698 00699 self support() const { 00700 00701 // BDD supp( &manager(), 00702 DdNode* tmp = Cudd_Support(manager().getManager(), m_interfaced.getNode()); 00703 Cudd_Ref(tmp); 00704 00705 self result = interfaced_type(m_interfaced.manager(), 00706 Cudd_zddPortFromBdd(manager().getManager(), tmp)); 00707 Cudd_RecursiveDeref(manager().getManager(), tmp); 00708 // return supp.PortToZdd(); 00709 00710 // assert(false); 00711 return result; 00712 } 00713 #endif 00714 00716 template<class VectorLikeType> 00717 void usedIndices(VectorLikeType& indices) const { 00718 00719 int* pIdx = Cudd_SupportIndex( manager().getManager(), 00720 m_interfaced.getNode() ); 00721 00722 00723 00724 size_type nlen(nVariables()); 00725 00726 indices.reserve(std::accumulate(pIdx, pIdx + nlen, size_type())); 00727 00728 for(size_type idx = 0; idx < nlen; ++idx) 00729 if (pIdx[idx] == 1){ 00730 indices.push_back(idx); 00731 } 00732 FREE(pIdx); 00733 } 00734 00736 int* usedIndices() const { 00737 00738 return Cudd_SupportIndex( manager().getManager(), 00739 m_interfaced.getNode() ); 00740 00741 00742 } 00743 00744 00746 first_iterator firstBegin() const { 00747 return first_iterator(navigation()); 00748 } 00749 00751 first_iterator firstEnd() const { 00752 return first_iterator(); 00753 } 00754 00756 last_iterator lastBegin() const { 00757 return last_iterator(m_interfaced.getNode()); 00758 } 00759 00761 last_iterator lastEnd() const { 00762 return last_iterator(); 00763 } 00764 00766 self firstMultiples(const std::vector<idx_type>& multipliers) const { 00767 00768 std::vector<idx_type> indices( std::distance(firstBegin(), firstEnd()) ); 00769 00770 std::copy( firstBegin(), firstEnd(), indices.begin() ); 00771 00772 return cudd_generate_multiples( manager(), 00773 indices.rbegin(), indices.rend(), 00774 multipliers.rbegin(), 00775 multipliers.rend() ); 00776 } 00777 00778 00779 00780 self subSet(const self& rhs) const { 00781 00782 return interfaced_type(m_interfaced.manager(), 00783 Extra_zddSubSet(manager().getManager(), 00784 m_interfaced.getNode(), 00785 rhs.m_interfaced.getNode()) ); 00786 } 00787 00788 self supSet(const self& rhs) const { 00789 00790 return interfaced_type(m_interfaced.manager(), 00791 Extra_zddSupSet(manager().getManager(), 00792 m_interfaced.getNode(), 00793 rhs.m_interfaced.getNode()) ); 00794 } 00796 self firstDivisors() const { 00797 00798 std::vector<idx_type> indices( std::distance(firstBegin(), firstEnd()) ); 00799 00800 std::copy( firstBegin(), firstEnd(), indices.begin() ); 00801 00802 return cudd_generate_divisors(manager(), indices.rbegin(), indices.rend()); 00803 } 00804 00806 navigator navigation() const { 00807 return navigator(m_interfaced.getNode()); 00808 } 00809 00811 bool_type emptiness() const { 00812 return ( m_interfaced.getNode() == manager().zddZero().getNode() ); 00813 } 00814 00816 bool_type blankness() const { 00817 00818 return ( m_interfaced.getNode() == 00819 manager().zddOne( nVariables() ).getNode() ); 00820 00821 } 00822 00823 bool_type isConstant() const { 00824 return (m_interfaced.getNode()) && Cudd_IsConstant(m_interfaced.getNode()); 00825 } 00826 00828 size_type size() const { 00829 return m_interfaced.Count(); 00830 } 00831 00833 size_type length() const { 00834 return size(); 00835 } 00836 00838 size_type nVariables() const { 00839 return Cudd_ReadZddSize(manager().getManager() ); 00840 } 00841 00843 self minimalElements() const { 00844 return interfaced_type(m_interfaced.manager(), 00845 Extra_zddMinimal(manager().getManager(),m_interfaced.getNode())); 00846 } 00847 00848 self cofactor0(const self& rhs) const { 00849 00850 return interfaced_type(m_interfaced.manager(), 00851 Extra_zddCofactor0(manager().getManager(), 00852 m_interfaced.getNode(), 00853 rhs.m_interfaced.getNode()) ); 00854 } 00855 00856 self cofactor1(const self& rhs, idx_type includeVars) const { 00857 00858 return interfaced_type(m_interfaced.manager(), 00859 Extra_zddCofactor1(manager().getManager(), 00860 m_interfaced.getNode(), 00861 rhs.m_interfaced.getNode(), 00862 includeVars) ); 00863 } 00864 00866 bool_type ownsOne() const { 00867 navigator navi(navigation()); 00868 00869 while (!navi.isConstant() ) 00870 navi.incrementElse(); 00871 00872 return navi.terminalValue(); 00873 } 00874 double sizeDouble() const { 00875 return m_interfaced.CountDouble(); 00876 } 00877 00879 self emptyElement() const { 00880 return manager().zddZero(); 00881 } 00882 00884 self blankElement() const { 00885 return manager().zddOne(); 00886 } 00887 00888 private: 00889 navigator newNode(const manager_base& mgr, idx_type idx, 00890 navigator thenNavi, navigator elseNavi) const { 00891 assert(idx < *thenNavi); 00892 assert(idx < *elseNavi); 00893 return navigator(cuddZddGetNode(mgr.getManager(), idx, 00894 thenNavi.getNode(), elseNavi.getNode())); 00895 } 00896 00897 interfaced_type newDiagram(const manager_base& mgr, navigator navi) const { 00898 return interfaced_type(extract_manager(mgr), navi.getNode()); 00899 } 00900 00901 self fromTemporaryNode(const navigator& navi) const { 00902 navi.decRef(); 00903 return self(manager(), navi.getNode()); 00904 } 00905 00906 00907 interfaced_type newNodeDiagram(const manager_base& mgr, idx_type idx, 00908 navigator thenNavi, 00909 navigator elseNavi) const { 00910 if ((idx >= *thenNavi) || (idx >= *elseNavi)) 00911 throw PBoRiGenericError<CTypes::invalid_ite>(); 00912 00913 return newDiagram(mgr, newNode(mgr, idx, thenNavi, elseNavi) ); 00914 } 00915 00916 interfaced_type newNodeDiagram(const manager_base& mgr, 00917 idx_type idx, navigator navi) const { 00918 if (idx >= *navi) 00919 throw PBoRiGenericError<CTypes::invalid_ite>(); 00920 00921 navi.incRef(); 00922 interfaced_type result = 00923 newDiagram(mgr, newNode(mgr, idx, navi, navi) ); 00924 navi.decRef(); 00925 return result; 00926 } 00927 00928 00929 00930 }; 00931 00932 00933 00934 00935 00937 template <class DDType> 00938 typename CDDInterface<DDType>::ostream_type& 00939 operator<<( typename CDDInterface<DDType>::ostream_type& os, 00940 const CDDInterface<DDType>& dd ) { 00941 return dd.print(os); 00942 } 00943 00944 END_NAMESPACE_PBORI 00945 00946 #endif // of #ifndef CDDInterface_h_