PolyBoRi

CCuddZDD.h

Go to the documentation of this file.
00001 // -*- c++ -*-
00002 //*****************************************************************************
00046 //*****************************************************************************
00047 
00048 #ifndef CCuddZDD_h
00049 #define CCuddZDD_h
00050 
00051 // include basic definitions
00052 #include "pbori_defs.h"
00053 
00054 #include <algorithm>
00055 
00056 #include <boost/shared_ptr.hpp>
00057 #include <boost/scoped_array.hpp>
00058 
00059 #include <boost/weak_ptr.hpp>
00060 
00061 #include <boost/intrusive_ptr.hpp>
00062 
00063 #include <boost/preprocessor/cat.hpp>
00064 #include <boost/preprocessor/seq/for_each.hpp>
00065 #include <boost/preprocessor/facilities/expand.hpp>
00066 #include <boost/preprocessor/stringize.hpp>
00067 
00068 #include "pbori_func.h"
00069 #include "pbori_traits.h"
00070 #include "CCuddCore.h"
00071 
00072 BEGIN_NAMESPACE_PBORI
00073 
00075 #define PB_DD_VERBOSE(text) if (ddMgr->verbose) \
00076   std::cout << text << " for node " << node <<  \
00077   " ref = " << refCount() << std::endl;
00078 
00091 template <class DiagramType>
00092 class CCuddDDBase {
00093 
00094 public:
00096   typedef DiagramType diagram_type;
00097   typedef CCuddDDBase self;
00098   PB_DECLARE_CUDD_TYPES(CCuddCore)
00099 
00100   
00101   typedef typename CCuddCore::mgrcore_ptr mgrcore_ptr;
00102 
00104   CCuddDDBase(mgrcore_ptr ddManager, node_type ddNode): 
00105     ddMgr(ddManager), node(ddNode) {
00106     if (node) Cudd_Ref(node);
00107     PB_DD_VERBOSE("Standard DD constructor");
00108   }
00109 
00111   CCuddDDBase(const self& from): 
00112     ddMgr(from.ddMgr), node(from.node) {
00113     if (node) {
00114       Cudd_Ref(node);
00115       PB_DD_VERBOSE("Copy DD constructor");
00116     }
00117   } 
00118 
00120   CCuddDDBase(): ddMgr(mgrcore_ptr()), node(NULL) {}
00121 
00123   mgrcore_ptr manager() const { return ddMgr; }
00124 
00126   mgrcore_type getManager() const { return ddMgr->manager; }
00127 
00129   node_type getNode() const{  return node; }
00130 
00132   size_type NodeReadIndex() const { return Cudd_NodeReadIndex(node); }
00133 
00135   size_type nodeCount() const { return (size_type)(Cudd_DagSize(node)); }
00136 
00138   size_type refCount() const { 
00139     assert(node != NULL);
00140     return Cudd_Regular(node)->ref;
00141   }
00142 
00144   bool isZero() const { return node == Cudd_ReadZero(getManager()); }
00145 
00146 protected:
00147 
00149   void checkSameManager(const diagram_type& other) const {
00150     if (getManager() != other.getManager()) 
00151       ddMgr->errorHandler("Operands come from different manager.");
00152   }
00153 
00155   void checkReturnValue(const node_type result) const {
00156     checkReturnValue(result != NULL);
00157   }
00158 
00160   void checkReturnValue(const int result, const int expected = 1) const {
00161     if UNLIKELY(result != expected)
00162       handle_error<>(ddMgr->errorHandler)(Cudd_ReadErrorCode( getManager() ));
00163   } 
00164 
00166 
00167   diagram_type apply(binary_function func, const diagram_type& rhs) const {
00168     checkSameManager(rhs);
00169     return checkedResult(func(getManager(), getNode(), rhs.getNode()));
00170   }
00171 
00172   diagram_type apply(binary_int_function func, idx_type idx) const {
00173     return checkedResult(func(getManager(), getNode(), idx) );
00174   }
00175 
00176   diagram_type apply(ternary_function func, 
00177              const diagram_type& first, const diagram_type& second) const {
00178     checkSameManager(first);
00179     checkSameManager(second);
00180     return checkedResult(func(getManager(), getNode(), 
00181                               first.getNode(), second.getNode()) );
00182   }
00183 
00184   idx_type apply(int_unary_function func) const {
00185     return checkedResult(func(getManager(), getNode()) );
00186   }
00188 
00190 
00191   diagram_type checkedResult(node_type result) const {
00192     checkReturnValue(result);
00193     return diagram_type(manager(), result);
00194   }
00195 
00196   idx_type checkedResult(idx_type result) const {
00197     checkReturnValue(result);
00198     return result;
00199   }
00200 
00201   template <class ResultType>
00202   ResultType memApply(ResultType (*func)(DdManager *, node_type)) const {
00203     return memChecked(func(getManager(), getNode()) );
00204   }
00205 
00206   template <class ResultType>
00207   ResultType memChecked(ResultType result) const {
00208     checkReturnValue(result != (ResultType) CUDD_OUT_OF_MEM);
00209     return result;
00210   }
00211   // @}
00212 
00214   mgrcore_ptr ddMgr;
00215 
00217   node_type node;
00218 }; // CCuddDD
00219 
00220 
00221 #define PB_ZDD_APPLY(count, data, funcname) \
00222   self funcname(data rhs) const {    \
00223     return apply(BOOST_PP_CAT(Cudd_zdd, funcname), rhs); }
00224 
00225 #define PB_ZDD_OP_ASSIGN(count, data, op) \
00226   self& operator BOOST_PP_CAT(op, =)(const self& other) { \
00227     return *this = (*this op other); }
00228 
00229 #define PB_ZDD_OP(count, data, op) \
00230   self operator op(const self& other) const { return data(other); }
00231 
00232 
00245 class CCuddZDD : 
00246   public CCuddDDBase<CCuddZDD> {
00247     friend class CCuddInterface;
00248 
00249 public:
00251   typedef CCuddZDD self;
00252 
00254   typedef CCuddDDBase<self> base;
00255  
00257   CCuddZDD(mgrcore_ptr mgr, node_type bddNode): base(mgr, bddNode) {}
00258 
00260   CCuddZDD(): base() {}
00261 
00263   CCuddZDD(const self &from): base(from) {}
00264 
00266   ~CCuddZDD() { deref(); }
00267 
00269   self& operator=(const self& right); // inlined below
00270 
00272 
00273   bool operator==(const self& other) const {
00274     checkSameManager(other);
00275     return node == other.node;
00276   }
00277   bool operator!=(const self& other) const { return !(*this == other); }
00278 
00279   bool operator<=(const self& other) const {
00280     return apply(Cudd_zddDiffConst, other).isZero(); 
00281   }
00282   bool operator>=(const self& other) const {
00283     return (other <= *this); 
00284   }
00285   bool operator<(const self& rhs) const { 
00286     return (*this != rhs) && (*this <= rhs);  
00287   }
00288   bool operator>(const self& other) const { 
00289     return (*this != other) && (*this >= other); 
00290   }
00292 
00295   BOOST_PP_SEQ_FOR_EACH(PB_ZDD_OP, Intersect, (*)(&))
00296   BOOST_PP_SEQ_FOR_EACH(PB_ZDD_OP, Union, (+)(|))
00297   BOOST_PP_SEQ_FOR_EACH(PB_ZDD_OP, Diff, (-))
00298 
00299   BOOST_PP_SEQ_FOR_EACH(PB_ZDD_OP_ASSIGN, BOOST_PP_NIL, (*)(&)(+)(|)(-))
00300 
00301   BOOST_PP_SEQ_FOR_EACH(PB_ZDD_APPLY, const self&, 
00302     (Product)(UnateProduct)(WeakDiv)(Divide)(WeakDivF)(DivideF)
00303     (Union)(Intersect)(Diff)(DiffConst))
00304 
00305   BOOST_PP_SEQ_FOR_EACH(PB_ZDD_APPLY, int, (Subset1)(Subset0)(Change))
00308 
00309   self Ite(const self& g, const self& h) const { 
00310     return apply(Cudd_zddIte, g, h); 
00311   }
00312 
00314 
00315   void print(int nvars, int verbosity = 1) const { std::cout.flush(); 
00316     if UNLIKELY(!Cudd_zddPrintDebug(getManager(), node, nvars, verbosity))
00317       ddMgr->errorHandler("print failed");
00318   }
00319   void PrintMinterm() const  { apply(Cudd_zddPrintMinterm); }
00320   void PrintCover() const    { apply(Cudd_zddPrintCover); }
00322 
00324   int Count() const          { return memApply(Cudd_zddCount); }
00325 
00327   double CountDouble() const { return memApply(Cudd_zddCountDouble); }
00328 
00330   double CountMinterm(int path) const { 
00331     return memChecked(Cudd_zddCountMinterm(getManager(), getNode(), path));
00332   }
00333 
00334 protected:
00335 
00336 
00338   void deref() {
00339     if (node != 0) {
00340       Cudd_RecursiveDerefZdd(getManager(), node);
00341       PB_DD_VERBOSE("CCuddZDD dereferencing");
00342     }
00343   }
00344 }; //CCuddZDD
00345 
00346 #undef PB_ZDD_APPLY
00347 #undef PB_ZDD_OP_ASSIGN
00348 #undef PB_ZDD_OP
00349 
00350 // ---------------------------------------------------------------------------
00351 // Members of class CCuddZDD
00352 // ---------------------------------------------------------------------------
00353 
00354 inline CCuddZDD& 
00355 CCuddZDD::operator=(const CCuddZDD& right) {
00356 
00357   if UNLIKELY(this == &right) return *this;
00358   if LIKELY(right.node) Cudd_Ref(right.node);
00359   deref();
00360   
00361   node = right.node;
00362   ddMgr = right.ddMgr;
00363   if (node)
00364     PB_DD_VERBOSE("CCuddZDD assignment");
00365   
00366   return *this;
00367 }
00368 
00369 #undef PB_DD_VERBOSE
00370 
00371 END_NAMESPACE_PBORI
00372 
00373 #endif
00374 
00375