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