• Main Page
  • Related Pages
  • Namespaces
  • Classes
  • Files
  • File List
  • File Members

CDDInterface.h

Go to the documentation of this file.
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_

Generated on Thu Nov 4 2010 08:06:20 for PolyBoRi by  doxygen 1.7.1