00001
00002
00046
00047
00048 #ifndef CCuddZDD_h
00049 #define CCuddZDD_h
00050
00051
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 };
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);
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 };
00345
00346 #undef PB_ZDD_APPLY
00347 #undef PB_ZDD_OP_ASSIGN
00348 #undef PB_ZDD_OP
00349
00350
00351
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