56 #include <boost/shared_ptr.hpp>
57 #include <boost/scoped_array.hpp>
59 #include <boost/weak_ptr.hpp>
61 #include <boost/intrusive_ptr.hpp>
63 #include <boost/preprocessor/cat.hpp>
64 #include <boost/preprocessor/seq/for_each.hpp>
65 #include <boost/preprocessor/facilities/expand.hpp>
66 #include <boost/preprocessor/stringize.hpp>
75 #define PB_DD_VERBOSE(text) if (ddMgr->verbose) \
76 std::cout << text << " for node " << node << \
77 " ref = " << refCount() << std::endl;
91 template <
class DiagramType>
105 ddMgr(ddManager), node(ddNode) {
106 if (node) Cudd_Ref(node);
112 ddMgr(from.ddMgr), node(from.node) {
139 assert(node != NULL);
140 return Cudd_Regular(node)->ref;
144 bool isZero()
const {
return node == Cudd_ReadZero(getManager()); }
151 ddMgr->errorHandler(
"Operands come from different manager.");
156 checkReturnValue(result != NULL);
162 handle_error<>(ddMgr->errorHandler)(Cudd_ReadErrorCode( getManager() ));
168 checkSameManager(rhs);
169 return checkedResult(func(getManager(), getNode(), rhs.
getNode()));
173 return checkedResult(func(getManager(), getNode(), idx) );
178 checkSameManager(first);
179 checkSameManager(second);
180 return checkedResult(func(getManager(), getNode(),
185 return checkedResult(func(getManager(), getNode()) );
192 checkReturnValue(result);
197 checkReturnValue(result);
201 template <
class ResultType>
203 return memChecked(func(getManager(), getNode()) );
206 template <
class ResultType>
208 checkReturnValue(result != (ResultType) CUDD_OUT_OF_MEM);
221 #define PB_ZDD_APPLY(count, data, funcname) \
222 self funcname(data rhs) const { \
223 return apply(BOOST_PP_CAT(Cudd_zdd, funcname), rhs); }
225 #define PB_ZDD_OP_ASSIGN(count, data, op) \
226 self& operator BOOST_PP_CAT(op, =)(const self& other) { \
227 return *this = (*this op other); }
229 #define PB_ZDD_OP(count, data, op) \
230 self operator op(const self& other) const { return data(other); }
269 self& operator=(
const self& right);
274 checkSameManager(other);
275 return node == other.node;
277 bool operator!=(
const self& other)
const {
return !(*
this == other); }
280 return apply(Cudd_zddDiffConst, other).isZero();
283 return (other <= *
this);
286 return (*
this != rhs) && (*
this <= rhs);
289 return (*
this != other) && (*
this >= other);
295 BOOST_PP_SEQ_FOR_EACH(
PB_ZDD_OP, Intersect, (*)(&))
296 BOOST_PP_SEQ_FOR_EACH(
PB_ZDD_OP, Union, (+)(|))
297 BOOST_PP_SEQ_FOR_EACH(PB_ZDD_OP, Diff, (-))
302 (Product)(UnateProduct)(WeakDiv)(Divide)(WeakDivF)(DivideF)
303 (Union)(Intersect)(Diff)(DiffConst))
305 BOOST_PP_SEQ_FOR_EACH(PB_ZDD_APPLY,
int, (Subset1)(Subset0)(Change))
309 self Ite(const self& g, const self& h)
const {
310 return apply(Cudd_zddIte, g, h);
315 void print(
int nvars,
int verbosity = 1)
const { std::cout.flush();
316 if UNLIKELY(!Cudd_zddPrintDebug(getManager(), node, nvars, verbosity))
317 ddMgr->errorHandler(
"print failed");
324 int Count()
const {
return memApply(Cudd_zddCount); }
327 double CountDouble()
const {
return memApply(Cudd_zddCountDouble); }
331 return memChecked(Cudd_zddCountMinterm(getManager(), getNode(), path));
340 Cudd_RecursiveDerefZdd(getManager(), node);
347 #undef PB_ZDD_OP_ASSIGN
357 if UNLIKELY(
this == &right)
return *
this;