PolyBoRi
|
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