PolyBoRi
CCuddDDFacade.h
Go to the documentation of this file.
00001 // -*- c++ -*-
00002 //*****************************************************************************
00014 //*****************************************************************************
00015 
00016 #ifndef polybori_diagram_CCuddDDFacade_h
00017 #define polybori_diagram_CCuddDDFacade_h
00018 
00019 // include basic definitions
00020 #include <polybori/pbori_defs.h>
00021 
00022 #include <polybori/cudd/cudd.h>
00023 #include <polybori/cudd/prefix.h>
00024 #include "CApplyNodeFacade.h"
00025 #include "CNodeCounter.h"
00026 
00027 #include <polybori/routines/pbori_routines_cuddext.h>
00028 #include <polybori/common/CExtrusivePtr.h>
00029 
00030 // Getting iterator type for navigating through Cudd's ZDDs structure
00031 #include <polybori/iterators/CCuddNavigator.h>
00032 
00033 // Getting iterator type for retrieving first term from Cudd's ZDDs
00034 #include <polybori/iterators/CCuddFirstIter.h>
00035 
00036 // Getting iterator type for retrieving last term from Cudd's ZDDs
00037 #include <polybori/iterators/CCuddLastIter.h>
00038 
00039 // Getting output iterator functionality
00040 #include <polybori/iterators/PBoRiOutIter.h>
00041 
00042 // Getting error coe functionality
00043 #include <polybori/except/PBoRiGenericError.h>
00044 
00045 // test input idx_type
00046 #include <polybori/common/CCheckedIdx.h>
00047 
00048 #include <polybori/routines/pbori_algo.h>
00049 #include <polybori/common/tags.h>
00050 #include <polybori/routines/pbori_routines_hash.h>
00051 
00052 #include <boost/preprocessor/cat.hpp>
00053 #include <boost/preprocessor/seq/for_each.hpp>
00054 #include <boost/preprocessor/facilities/expand.hpp>
00055 #include <boost/preprocessor/stringize.hpp>
00056 #include <stdexcept>
00057 #include <algorithm>
00058 #include <numeric>
00059 
00060 BEGIN_NAMESPACE_PBORI
00061 
00062 
00064 template <class DataType>
00065 inline void
00066 extrusive_ptr_release(const DataType& data, DdNode* ptr) {
00067    if (ptr != NULL) {
00068      PBORI_PREFIX(Cudd_RecursiveDerefZdd)(data.getManager(), ptr);
00069    }
00070 }
00071 
00073 template <class DataType>
00074 inline void 
00075 extrusive_ptr_add_ref(const DataType&, DdNode* ptr) {
00076   if (ptr) PBORI_PREFIX(Cudd_Ref)(ptr);
00077 }
00078 
00084 #define PBORI_NAME_Product product
00085 #define PBORI_NAME_UnateProduct unateProduct
00086 #define PBORI_NAME_WeakDiv weakDivide
00087 #define PBORI_NAME_Divide divide
00088 #define PBORI_NAME_WeakDivF weakDivF
00089 #define PBORI_NAME_DivideF divideF
00090 #define PBORI_NAME_Union unite
00091 #define PBORI_NAME_Intersect intersect
00092 #define PBORI_NAME_Diff diff
00093 #define PBORI_NAME_Subset1 subset1
00094 #define PBORI_NAME_Subset0 subset0
00095 #define PBORI_NAME_Change change
00096 
00097 #define PB_ZDD_APPLY(count, data, funcname) \
00098   diagram_type BOOST_PP_CAT(PBORI_NAME_, funcname)(data rhs) const {    \
00099     return apply(BOOST_PP_CAT(PBORI_PREFIX(Cudd_zdd), funcname),        \
00100                               rhs); }
00101 
00102 template <class RingType, class DiagramType>
00103 class CCuddDDFacade: 
00104   public CApplyNodeFacade<DiagramType, DdNode*>,
00105   public CAuxTypes {
00106 
00108   typedef CCuddDDFacade self;
00109 public:
00110 
00112   typedef CTypes::ostream_type ostream_type;
00113 
00115   typedef RingType ring_type;
00116 
00118   typedef DiagramType diagram_type;
00119 
00121   typedef DdNode node_type;
00122 
00124   typedef node_type* node_ptr;
00125 
00127   typedef CApplyNodeFacade<diagram_type, node_ptr> base;
00128 
00130   typedef CCuddFirstIter first_iterator;
00131 
00133   typedef CCuddLastIter last_iterator;
00134 
00136   typedef CCuddNavigator navigator;
00137 
00139   typedef valid_tag easy_equality_property;
00140 
00142   typedef typename ring_type::mgr_type mgr_type;
00143 
00145   typedef int cudd_idx_type;
00146 
00148   typedef CCheckedIdx checked_idx_type;
00149 
00151   CCuddDDFacade(const ring_type& ring, node_ptr node): 
00152     p_node(ring, node) {
00153     checkAssumption(node != NULL);
00154   }
00155 
00157   CCuddDDFacade(const ring_type& ring, const navigator& navi): 
00158     p_node(ring, navi.getNode()) {
00159     checkAssumption(navi.isValid());
00160   }
00162   CCuddDDFacade(const ring_type& ring, 
00163                idx_type idx, navigator thenNavi, navigator elseNavi): 
00164     p_node(ring, getNewNode(ring, idx, thenNavi, elseNavi)) { }
00165 
00168   CCuddDDFacade(const ring_type& ring, 
00169                idx_type idx, navigator navi): 
00170     p_node(ring, getNewNode(ring, idx, navi, navi)) { }
00171 
00173   CCuddDDFacade(idx_type idx, const self& thenDD, const self& elseDD):
00174     p_node(thenDD.ring(), getNewNode(idx, thenDD, elseDD)) { }
00175 
00177   private: CCuddDDFacade(): p_node()  {}  
00178     public:
00180   CCuddDDFacade(const self &from): p_node(from.p_node) {}
00181 
00183   ~CCuddDDFacade() {}
00184 
00186   diagram_type& operator=(const diagram_type& rhs) {
00187     p_node = rhs.p_node;
00188     return static_cast<diagram_type&>(*this);
00189   }
00190 
00193   BOOST_PP_SEQ_FOR_EACH(PB_ZDD_APPLY, const diagram_type&, 
00194     (Product)(UnateProduct)(WeakDiv)(Divide)(WeakDivF)(DivideF)
00195     (Union)(Intersect)(Diff))
00196 
00197   BOOST_PP_SEQ_FOR_EACH(PB_ZDD_APPLY, int, (Subset1)(Subset0)(Change))
00200 
00201   bool implies(const self& rhs) const {
00202     return PBORI_PREFIX(Cudd_zddDiffConst)(getManager(), getNode(), rhs.getNode()) ==
00203       PBORI_PREFIX(Cudd_ReadZero)(getManager());
00204   }
00205 
00206 
00208 
00209   std::ostream& printIntern(std::ostream& os) const {
00210     os << getNode() <<": ";
00211 
00212     if (isZero())
00213       os << "empty";
00214     else
00215       os << nNodes() << " nodes " <<  count() << "terms";
00216 
00217     return os;
00218 
00219   }
00220   void PrintMinterm() const  {
00221     checkAssumption(apply(PBORI_PREFIX(Cudd_zddPrintMinterm)) == 1);
00222   }
00224 
00226   size_type count() const { return dd_long_count<size_type>(navigation());  }
00227 
00229   double countDouble() const { return dd_long_count<double>(navigation()); }
00230 
00232   size_type rootIndex() const { return PBORI_PREFIX(Cudd_NodeReadIndex)(getNode()); }
00233 
00235   size_type nNodes() const { return CNodeCounter<navigator>()(navigation()); }
00236 
00238   size_type refCount() const { 
00239     PBORI_ASSERT(getNode() != NULL);
00240     return PBORI_PREFIX(Cudd_Regular)(getNode())->ref;
00241   }
00242 
00244   bool isZero() const { return getNode() == PBORI_PREFIX(Cudd_ReadZero)(getManager()); }
00245 
00247   bool isOne() const { return getNode() == DD_ONE(getManager()); }
00248 
00250   const ring_type& ring() const { return p_node.data(); }
00251 
00253   node_ptr getNode() const { return p_node.get(); }
00254 
00256   mgr_type* getManager() const { return p_node.data().getManager(); }
00257 
00258 protected:
00259 
00261   using base::apply;
00262 
00263 
00264   template <class ResultType>
00265   ResultType memApply(ResultType (*func)(mgr_type *, node_ptr)) const {
00266     ResultType result = apply(func);
00267     checkAssumption(result != (ResultType) CUDD_OUT_OF_MEM);
00268     return result;
00269   }
00270 
00272   void checkAssumption(bool isValid) const {
00273     if PBORI_UNLIKELY(!isValid)
00274       throw std::runtime_error(error_text(getManager()));
00275   }
00276 
00278   template<class ManagerType, class ReverseIterator, class MultReverseIterator>
00279   diagram_type
00280   cudd_generate_multiples(const ManagerType& mgr, 
00281                           ReverseIterator start, ReverseIterator finish,
00282                           MultReverseIterator multStart, 
00283                           MultReverseIterator multFinish) const {
00284 
00285     // signed case
00286     while ((multStart != multFinish) && (*multStart > CTypes::max_idx))
00287       ++multStart;
00288     // unsigned case
00289     while ((multStart != multFinish) && (*multStart < 0))
00290       --multFinish;
00291 
00292     DdNode* prev( (getManager())->one );
00293     
00294     DdNode* zeroNode( (getManager())->zero ); 
00295     
00296     PBORI_PREFIX(Cudd_Ref)(prev);
00297     while(start != finish) {
00298       
00299       while((multStart != multFinish) && (*start < *multStart)) {
00300 
00301         DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( getManager(), *multStart,
00302                                              prev, prev );
00303 
00304         PBORI_PREFIX(Cudd_Ref)(result);
00305         PBORI_PREFIX(Cudd_RecursiveDerefZdd)(getManager(), prev);
00306 
00307         prev = result;
00308         ++multStart;
00309 
00310       };
00311 
00312       DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( getManager(), *start,
00313                                            prev, zeroNode );
00314 
00315       PBORI_PREFIX(Cudd_Ref)(result);
00316       PBORI_PREFIX(Cudd_RecursiveDerefZdd)(getManager(), prev);
00317 
00318       prev = result;
00319 
00320 
00321       if((multStart != multFinish) && (*start == *multStart))
00322         ++multStart;
00323 
00324 
00325       ++start;
00326     }
00327 
00328     while(multStart != multFinish) {
00329 
00330       DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( getManager(), *multStart,
00331                                            prev, prev );
00332 
00333       PBORI_PREFIX(Cudd_Ref)(result);
00334       PBORI_PREFIX(Cudd_RecursiveDerefZdd)(getManager(), prev);
00335 
00336       prev = result;
00337       ++multStart;
00338 
00339     };
00340 
00341     PBORI_PREFIX(Cudd_Deref)(prev);
00342 
00343 
00344     return diagram_type(mgr, prev);
00345   }
00346 
00348   template<class ManagerType, class ReverseIterator>
00349   diagram_type
00350   cudd_generate_divisors(const ManagerType& mgr, 
00351                          ReverseIterator start, ReverseIterator finish) const {
00352 
00353 
00354     DdNode* prev= (getManager())->one;
00355 
00356     PBORI_PREFIX(Cudd_Ref)(prev);
00357     while(start != finish) {
00358 
00359       DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( getManager(),
00360                                            *start, prev, prev);
00361 
00362       PBORI_PREFIX(Cudd_Ref)(result);
00363       PBORI_PREFIX(Cudd_RecursiveDerefZdd)(getManager(), prev);
00364 
00365       prev = result;
00366       ++start;
00367     }
00368 
00369     PBORI_PREFIX(Cudd_Deref)(prev);
00371       return diagram_type(mgr, prev);
00372 
00373 }
00374 public:
00375 
00377   diagram_type Xor(const diagram_type& rhs) const {
00378     if (rhs.isZero())
00379       return *this;
00380 
00381     //    return apply(pboriPBORI_PREFIX(Cudd_zddUnionXor), rhs);
00382     base::checkSameManager(rhs);
00383     return diagram_type(ring(), pboriCudd_zddUnionXor(getManager(), getNode(), rhs.getNode()) );
00384   }
00385 
00387   diagram_type divideFirst(const diagram_type& rhs) const {
00388 
00389     diagram_type result(*this);
00390     PBoRiOutIter<diagram_type, idx_type, subset1_assign<diagram_type> >  outiter(result);
00391     std::copy(rhs.firstBegin(), rhs.firstEnd(), outiter);
00392 
00393     return result;
00394   }
00395 
00396 
00398   ostream_type& print(ostream_type& os) const {
00399 
00400     printIntern(os) << std::endl;;
00401     PrintMinterm();
00402 
00403     return os;
00404   }
00405 
00406 
00408   //  size_type nSupport() const { return apply(PBORI_PREFIX(PBORI_PREFIX(Cudd_SupportSize));) }
00409 
00411   first_iterator firstBegin() const {
00412     return first_iterator(navigation());
00413   }
00414 
00416   first_iterator firstEnd() const { 
00417     return first_iterator();
00418   }
00419 
00421   last_iterator lastBegin() const {
00422     return last_iterator(getNode());
00423   }
00424 
00426   last_iterator lastEnd() const { 
00427     return last_iterator();
00428   }
00429   
00431   diagram_type firstMultiples(const std::vector<idx_type>& input_multipliers) const {
00432 
00433     std::set<idx_type> multipliers(input_multipliers.begin(), input_multipliers.end());
00434     std::vector<idx_type> indices( std::distance(firstBegin(), firstEnd()) );
00435 
00436     std::copy( firstBegin(), firstEnd(), indices.begin() );
00437 
00438     return cudd_generate_multiples( ring(),
00439                                     indices.rbegin(), indices.rend(),
00440                                     multipliers.rbegin(),
00441                                     multipliers.rend() );
00442   }
00443 
00445   diagram_type firstDivisors() const {
00446 
00447     std::vector<idx_type> indices( std::distance(firstBegin(), firstEnd()) );
00448 
00449     std::copy( firstBegin(), firstEnd(), indices.begin() );
00450 
00451     return cudd_generate_divisors(ring(), indices.rbegin(), indices.rend());
00452   }
00453 
00455   navigator navigation() const {
00456     return navigator(getNode());
00457   }
00458 
00460   bool_type isConstant() const {
00461     return (getNode()) && PBORI_PREFIX(Cudd_IsConstant)(getNode());
00462   }
00463 
00464 
00465 
00466 private:
00467 
00469   static node_ptr
00470   getNewNode(const ring_type& ring, checked_idx_type idx, 
00471              navigator thenNavi, navigator elseNavi) {
00472 
00473     if ((idx >= *thenNavi) || (idx >= *elseNavi))
00474       throw PBoRiGenericError<CTypes::invalid_ite>();
00475     
00476     return PBORI_PREFIX(cuddZddGetNode)(ring.getManager(), idx, 
00477                           thenNavi.getNode(), elseNavi.getNode());
00478   }
00479 
00481   static node_ptr 
00482   getNewNode(idx_type idx, const self& thenDD, const self& elseDD) {
00483     thenDD.checkSameManager(elseDD);
00484     return getNewNode(thenDD.ring(), 
00485                       idx, thenDD.navigation(), elseDD.navigation());
00486   }
00487 
00488 private:
00490   CExtrusivePtr<ring_type, node_type> p_node;
00491 };
00492 
00493 
00494 #undef PB_ZDD_APPLY
00495 
00496 END_NAMESPACE_PBORI
00497 
00498 #endif