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

CDDInterface.h

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

Generated on Wed Sep 29 2010 for PolyBoRi by  doxygen 1.7.1