PolyBoRi
CCuddZDD.h
Go to the documentation of this file.
1 // -*- c++ -*-
2 //*****************************************************************************
46 //*****************************************************************************
47 
48 #ifndef CCuddZDD_h
49 #define CCuddZDD_h
50 
51 // include basic definitions
52 #include "pbori_defs.h"
53 
54 #include <algorithm>
55 
56 #include <boost/shared_ptr.hpp>
57 #include <boost/scoped_array.hpp>
58 
59 #include <boost/weak_ptr.hpp>
60 
61 #include <boost/intrusive_ptr.hpp>
62 
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>
67 
68 #include "pbori_func.h"
69 #include "pbori_traits.h"
70 #include "CCuddCore.h"
71 
73 
75 #define PB_DD_VERBOSE(text) if (ddMgr->verbose) \
76  std::cout << text << " for node " << node << \
77  " ref = " << refCount() << std::endl;
78 
91 template <class DiagramType>
92 class CCuddDDBase {
93 
94 public:
96  typedef DiagramType diagram_type;
97  typedef CCuddDDBase self;
99 
100 
101  typedef typename CCuddCore::mgrcore_ptr mgrcore_ptr;
102 
104  CCuddDDBase(mgrcore_ptr ddManager, node_type ddNode):
105  ddMgr(ddManager), node(ddNode) {
106  if (node) Cudd_Ref(node);
107  PB_DD_VERBOSE("Standard DD constructor");
108  }
109 
111  CCuddDDBase(const self& from):
112  ddMgr(from.ddMgr), node(from.node) {
113  if (node) {
114  Cudd_Ref(node);
115  PB_DD_VERBOSE("Copy DD constructor");
116  }
117  }
118 
120  CCuddDDBase(): ddMgr(mgrcore_ptr()), node(NULL) {}
121 
123  mgrcore_ptr manager() const { return ddMgr; }
124 
126  mgrcore_type getManager() const { return ddMgr->manager; }
127 
129  node_type getNode() const{ return node; }
130 
132  size_type NodeReadIndex() const { return Cudd_NodeReadIndex(node); }
133 
135  size_type nodeCount() const { return (size_type)(Cudd_DagSize(node)); }
136 
138  size_type refCount() const {
139  assert(node != NULL);
140  return Cudd_Regular(node)->ref;
141  }
142 
144  bool isZero() const { return node == Cudd_ReadZero(getManager()); }
145 
146 protected:
147 
149  void checkSameManager(const diagram_type& other) const {
150  if (getManager() != other.getManager())
151  ddMgr->errorHandler("Operands come from different manager.");
152  }
153 
155  void checkReturnValue(const node_type result) const {
156  checkReturnValue(result != NULL);
157  }
158 
160  void checkReturnValue(const int result, const int expected = 1) const {
161  if UNLIKELY(result != expected)
162  handle_error<>(ddMgr->errorHandler)(Cudd_ReadErrorCode( getManager() ));
163  }
164 
166 
167  diagram_type apply(binary_function func, const diagram_type& rhs) const {
168  checkSameManager(rhs);
169  return checkedResult(func(getManager(), getNode(), rhs.getNode()));
170  }
171 
173  return checkedResult(func(getManager(), getNode(), idx) );
174  }
175 
177  const diagram_type& first, const diagram_type& second) const {
178  checkSameManager(first);
179  checkSameManager(second);
180  return checkedResult(func(getManager(), getNode(),
181  first.getNode(), second.getNode()) );
182  }
183 
185  return checkedResult(func(getManager(), getNode()) );
186  }
188 
190 
192  checkReturnValue(result);
193  return diagram_type(manager(), result);
194  }
195 
197  checkReturnValue(result);
198  return result;
199  }
200 
201  template <class ResultType>
202  ResultType memApply(ResultType (*func)(DdManager *, node_type)) const {
203  return memChecked(func(getManager(), getNode()) );
204  }
205 
206  template <class ResultType>
207  ResultType memChecked(ResultType result) const {
208  checkReturnValue(result != (ResultType) CUDD_OUT_OF_MEM);
209  return result;
210  }
211  // @}
212 
215 
218 }; // CCuddDD
219 
220 
221 #define PB_ZDD_APPLY(count, data, funcname) \
222  self funcname(data rhs) const { \
223  return apply(BOOST_PP_CAT(Cudd_zdd, funcname), rhs); }
224 
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); }
228 
229 #define PB_ZDD_OP(count, data, op) \
230  self operator op(const self& other) const { return data(other); }
231 
232 
245 class CCuddZDD :
246  public CCuddDDBase<CCuddZDD> {
247  friend class CCuddInterface;
248 
249 public:
251  typedef CCuddZDD self;
252 
255 
257  CCuddZDD(mgrcore_ptr mgr, node_type bddNode): base(mgr, bddNode) {}
258 
260  CCuddZDD(): base() {}
261 
263  CCuddZDD(const self &from): base(from) {}
264 
266  ~CCuddZDD() { deref(); }
267 
269  self& operator=(const self& right); // inlined below
270 
272 
273  bool operator==(const self& other) const {
274  checkSameManager(other);
275  return node == other.node;
276  }
277  bool operator!=(const self& other) const { return !(*this == other); }
278 
279  bool operator<=(const self& other) const {
280  return apply(Cudd_zddDiffConst, other).isZero();
281  }
282  bool operator>=(const self& other) const {
283  return (other <= *this);
284  }
285  bool operator<(const self& rhs) const {
286  return (*this != rhs) && (*this <= rhs);
287  }
288  bool operator>(const self& other) const {
289  return (*this != other) && (*this >= other);
290  }
292 
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, (-))
298 
299  BOOST_PP_SEQ_FOR_EACH(PB_ZDD_OP_ASSIGN, BOOST_PP_NIL, (*)(&)(+)(|)(-))
300 
301  BOOST_PP_SEQ_FOR_EACH(PB_ZDD_APPLY, const self&,
302  (Product)(UnateProduct)(WeakDiv)(Divide)(WeakDivF)(DivideF)
303  (Union)(Intersect)(Diff)(DiffConst))
304 
305  BOOST_PP_SEQ_FOR_EACH(PB_ZDD_APPLY, int, (Subset1)(Subset0)(Change))
308 
309  self Ite(const self& g, const self& h) const {
310  return apply(Cudd_zddIte, g, h);
311  }
312 
314 
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");
318  }
319  void PrintMinterm() const { apply(Cudd_zddPrintMinterm); }
320  void PrintCover() const { apply(Cudd_zddPrintCover); }
322 
324  int Count() const { return memApply(Cudd_zddCount); }
325 
327  double CountDouble() const { return memApply(Cudd_zddCountDouble); }
328 
330  double CountMinterm(int path) const {
331  return memChecked(Cudd_zddCountMinterm(getManager(), getNode(), path));
332  }
333 
334 protected:
335 
336 
338  void deref() {
339  if (node != 0) {
340  Cudd_RecursiveDerefZdd(getManager(), node);
341  PB_DD_VERBOSE("CCuddZDD dereferencing");
342  }
343  }
344 }; //CCuddZDD
345 
346 #undef PB_ZDD_APPLY
347 #undef PB_ZDD_OP_ASSIGN
348 #undef PB_ZDD_OP
349 
350 // ---------------------------------------------------------------------------
351 // Members of class CCuddZDD
352 // ---------------------------------------------------------------------------
353 
354 inline CCuddZDD&
355 CCuddZDD::operator=(const CCuddZDD& right) {
356 
357  if UNLIKELY(this == &right) return *this;
358  if LIKELY(right.node) Cudd_Ref(right.node);
359  deref();
360 
361  node = right.node;
362  ddMgr = right.ddMgr;
363  if (node)
364  PB_DD_VERBOSE("CCuddZDD assignment");
365 
366  return *this;
367 }
368 
369 #undef PB_DD_VERBOSE
370 
372 
373 #endif
374 
375