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