PolyBoRi
CCuddDDFacade.h
Go to the documentation of this file.
1 // -*- c++ -*-
2 //*****************************************************************************
14 //*****************************************************************************
15 
16 #ifndef polybori_diagram_CCuddDDFacade_h
17 #define polybori_diagram_CCuddDDFacade_h
18 
19 // include basic definitions
20 #include <polybori/pbori_defs.h>
21 
22 #include <polybori/cudd/cudd.h>
23 #include <polybori/cudd/prefix.h>
24 #include "CApplyNodeFacade.h"
25 #include "CNodeCounter.h"
26 
29 
30 // Getting iterator type for navigating through Cudd's ZDDs structure
32 
33 // Getting iterator type for retrieving first term from Cudd's ZDDs
35 
36 // Getting iterator type for retrieving last term from Cudd's ZDDs
38 
39 // Getting output iterator functionality
41 
42 // Getting error coe functionality
44 
45 // test input idx_type
47 
49 #include <polybori/common/tags.h>
51 
52 #include <boost/preprocessor/cat.hpp>
53 #include <boost/preprocessor/seq/for_each.hpp>
54 #include <boost/preprocessor/facilities/expand.hpp>
55 #include <boost/preprocessor/stringize.hpp>
56 #include <stdexcept>
57 #include <algorithm>
58 #include <numeric>
59 
61 
62 
64 template <class DataType>
65 inline void
66 extrusive_ptr_release(const DataType& data, DdNode* ptr) {
67  if (ptr != NULL) {
68  PBORI_PREFIX(Cudd_RecursiveDerefZdd)(data.getManager(), ptr);
69  }
70 }
71 
73 template <class DataType>
74 inline void
75 extrusive_ptr_add_ref(const DataType&, DdNode* ptr) {
76  if (ptr) PBORI_PREFIX(Cudd_Ref)(ptr);
77 }
78 
84 #define PBORI_NAME_Product product
85 #define PBORI_NAME_UnateProduct unateProduct
86 #define PBORI_NAME_WeakDiv weakDivide
87 #define PBORI_NAME_Divide divide
88 #define PBORI_NAME_WeakDivF weakDivF
89 #define PBORI_NAME_DivideF divideF
90 #define PBORI_NAME_Union unite
91 #define PBORI_NAME_Intersect intersect
92 #define PBORI_NAME_Diff diff
93 #define PBORI_NAME_Subset1 subset1
94 #define PBORI_NAME_Subset0 subset0
95 #define PBORI_NAME_Change change
96 
97 #define PB_ZDD_APPLY(count, data, funcname) \
98  diagram_type BOOST_PP_CAT(PBORI_NAME_, funcname)(data rhs) const { \
99  return apply(BOOST_PP_CAT(PBORI_PREFIX(Cudd_zdd), funcname), \
100  rhs); }
101 
102 template <class RingType, class DiagramType>
104  public CApplyNodeFacade<DiagramType, DdNode*>,
105  public CAuxTypes {
106 
108  typedef CCuddDDFacade self;
109 public:
110 
113 
115  typedef RingType ring_type;
116 
118  typedef DiagramType diagram_type;
119 
121  typedef DdNode node_type;
122 
124  typedef node_type* node_ptr;
125 
128 
131 
134 
137 
140 
142  typedef typename ring_type::mgr_type mgr_type;
143 
145  typedef int cudd_idx_type;
146 
149 
151  CCuddDDFacade(const ring_type& ring, node_ptr node):
152  p_node(ring, node) {
153  checkAssumption(node != NULL);
154  }
155 
157  CCuddDDFacade(const ring_type& ring, const navigator& navi):
158  p_node(ring, navi.getNode()) {
159  checkAssumption(navi.isValid());
160  }
162  CCuddDDFacade(const ring_type& ring,
163  idx_type idx, navigator thenNavi, navigator elseNavi):
164  p_node(ring, getNewNode(ring, idx, thenNavi, elseNavi)) { }
165 
168  CCuddDDFacade(const ring_type& ring,
169  idx_type idx, navigator navi):
170  p_node(ring, getNewNode(ring, idx, navi, navi)) { }
171 
173  CCuddDDFacade(idx_type idx, const self& thenDD, const self& elseDD):
174  p_node(thenDD.ring(), getNewNode(idx, thenDD, elseDD)) { }
175 
177  private: CCuddDDFacade(): p_node() {}
178  public:
180  CCuddDDFacade(const self &from): p_node(from.p_node) {}
181 
184 
187  p_node = rhs.p_node;
188  return static_cast<diagram_type&>(*this);
189  }
190 
193  BOOST_PP_SEQ_FOR_EACH(PB_ZDD_APPLY, const diagram_type&,
194  (Product)(UnateProduct)(WeakDiv)(Divide)(WeakDivF)(DivideF)
195  (Union)(Intersect)(Diff))
196 
197  BOOST_PP_SEQ_FOR_EACH(PB_ZDD_APPLY, int, (Subset1)(Subset0)(Change))
200 
201  bool implies(const self& rhs) const {
202  return PBORI_PREFIX(Cudd_zddDiffConst)(getManager(), getNode(), rhs.getNode()) ==
203  PBORI_PREFIX(Cudd_ReadZero)(getManager());
204  }
205 
206 
208 
209  std::ostream& printIntern(std::ostream& os) const {
210  os << getNode() <<": ";
211 
212  if (isZero())
213  os << "empty";
214  else
215  os << nNodes() << " nodes " << count() << "terms";
216 
217  return os;
218 
219  }
220  void PrintMinterm() const {
221  checkAssumption(apply(PBORI_PREFIX(Cudd_zddPrintMinterm)) == 1);
222  }
224 
226  size_type count() const { return dd_long_count<size_type>(navigation()); }
227 
229  double countDouble() const { return dd_long_count<double>(navigation()); }
230 
232  size_type rootIndex() const { return PBORI_PREFIX(Cudd_NodeReadIndex)(getNode()); }
233 
235  size_type nNodes() const { return CNodeCounter<navigator>()(navigation()); }
236 
238  size_type refCount() const {
239  PBORI_ASSERT(getNode() != NULL);
240  return PBORI_PREFIX(Cudd_Regular)(getNode())->ref;
241  }
242 
244  bool isZero() const { return getNode() == PBORI_PREFIX(Cudd_ReadZero)(getManager()); }
245 
247  bool isOne() const { return getNode() == DD_ONE(getManager()); }
248 
250  const ring_type& ring() const { return p_node.data(); }
251 
253  node_ptr getNode() const { return p_node.get(); }
254 
256  mgr_type* getManager() const { return p_node.data().getManager(); }
257 
258 protected:
259 
261  using base::apply;
262 
263 
264  template <class ResultType>
265  ResultType memApply(ResultType (*func)(mgr_type *, node_ptr)) const {
266  ResultType result = apply(func);
267  checkAssumption(result != (ResultType) CUDD_OUT_OF_MEM);
268  return result;
269  }
270 
272  void checkAssumption(bool isValid) const {
273  if PBORI_UNLIKELY(!isValid)
274  throw std::runtime_error(error_text(getManager()));
275  }
276 
278  template<class ManagerType, class ReverseIterator, class MultReverseIterator>
279  diagram_type
280  cudd_generate_multiples(const ManagerType& mgr,
281  ReverseIterator start, ReverseIterator finish,
282  MultReverseIterator multStart,
283  MultReverseIterator multFinish) const {
284 
285  // signed case
286  while ((multStart != multFinish) && (*multStart > CTypes::max_idx))
287  ++multStart;
288  // unsigned case
289  while ((multStart != multFinish) && (*multStart < 0))
290  --multFinish;
291 
292  DdNode* prev( (getManager())->one );
293 
294  DdNode* zeroNode( (getManager())->zero );
295 
296  PBORI_PREFIX(Cudd_Ref)(prev);
297  while(start != finish) {
298 
299  while((multStart != multFinish) && (*start < *multStart)) {
300 
301  DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( getManager(), *multStart,
302  prev, prev );
303 
304  PBORI_PREFIX(Cudd_Ref)(result);
305  PBORI_PREFIX(Cudd_RecursiveDerefZdd)(getManager(), prev);
306 
307  prev = result;
308  ++multStart;
309 
310  };
311 
312  DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( getManager(), *start,
313  prev, zeroNode );
314 
315  PBORI_PREFIX(Cudd_Ref)(result);
316  PBORI_PREFIX(Cudd_RecursiveDerefZdd)(getManager(), prev);
317 
318  prev = result;
319 
320 
321  if((multStart != multFinish) && (*start == *multStart))
322  ++multStart;
323 
324 
325  ++start;
326  }
327 
328  while(multStart != multFinish) {
329 
330  DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( getManager(), *multStart,
331  prev, prev );
332 
333  PBORI_PREFIX(Cudd_Ref)(result);
334  PBORI_PREFIX(Cudd_RecursiveDerefZdd)(getManager(), prev);
335 
336  prev = result;
337  ++multStart;
338 
339  };
340 
341  PBORI_PREFIX(Cudd_Deref)(prev);
342 
343 
344  return diagram_type(mgr, prev);
345  }
346 
348  template<class ManagerType, class ReverseIterator>
349  diagram_type
350  cudd_generate_divisors(const ManagerType& mgr,
351  ReverseIterator start, ReverseIterator finish) const {
352 
353 
354  DdNode* prev= (getManager())->one;
355 
356  PBORI_PREFIX(Cudd_Ref)(prev);
357  while(start != finish) {
358 
359  DdNode* result = PBORI_PREFIX(cuddUniqueInterZdd)( getManager(),
360  *start, prev, prev);
361 
362  PBORI_PREFIX(Cudd_Ref)(result);
363  PBORI_PREFIX(Cudd_RecursiveDerefZdd)(getManager(), prev);
364 
365  prev = result;
366  ++start;
367  }
368 
369  PBORI_PREFIX(Cudd_Deref)(prev);
371  return diagram_type(mgr, prev);
372 
373 }
374 public:
375 
377  diagram_type Xor(const diagram_type& rhs) const {
378  if (rhs.isZero())
379  return *this;
380 
381  // return apply(pboriPBORI_PREFIX(Cudd_zddUnionXor), rhs);
382  base::checkSameManager(rhs);
383  return diagram_type(ring(), pboriCudd_zddUnionXor(getManager(), getNode(), rhs.getNode()) );
384  }
385 
388 
389  diagram_type result(*this);
391  std::copy(rhs.firstBegin(), rhs.firstEnd(), outiter);
392 
393  return result;
394  }
395 
396 
399 
400  printIntern(os) << std::endl;;
401  PrintMinterm();
402 
403  return os;
404  }
405 
406 
408  // size_type nSupport() const { return apply(PBORI_PREFIX(PBORI_PREFIX(Cudd_SupportSize));) }
409 
412  return first_iterator(navigation());
413  }
414 
417  return first_iterator();
418  }
419 
422  return last_iterator(getNode());
423  }
424 
427  return last_iterator();
428  }
429 
431  diagram_type firstMultiples(const std::vector<idx_type>& input_multipliers) const {
432 
433  std::set<idx_type> multipliers(input_multipliers.begin(), input_multipliers.end());
434  std::vector<idx_type> indices( std::distance(firstBegin(), firstEnd()) );
435 
436  std::copy( firstBegin(), firstEnd(), indices.begin() );
437 
438  return cudd_generate_multiples( ring(),
439  indices.rbegin(), indices.rend(),
440  multipliers.rbegin(),
441  multipliers.rend() );
442  }
443 
446 
447  std::vector<idx_type> indices( std::distance(firstBegin(), firstEnd()) );
448 
449  std::copy( firstBegin(), firstEnd(), indices.begin() );
450 
451  return cudd_generate_divisors(ring(), indices.rbegin(), indices.rend());
452  }
453 
456  return navigator(getNode());
457  }
458 
461  return (getNode()) && PBORI_PREFIX(Cudd_IsConstant)(getNode());
462  }
463 
464 
465 
466 private:
467 
469  static node_ptr
470  getNewNode(const ring_type& ring, checked_idx_type idx,
471  navigator thenNavi, navigator elseNavi) {
472 
473  if ((idx >= *thenNavi) || (idx >= *elseNavi))
475 
476  return PBORI_PREFIX(cuddZddGetNode)(ring.getManager(), idx,
477  thenNavi.getNode(), elseNavi.getNode());
478  }
479 
481  static node_ptr
482  getNewNode(idx_type idx, const self& thenDD, const self& elseDD) {
483  thenDD.checkSameManager(elseDD);
484  return getNewNode(thenDD.ring(),
485  idx, thenDD.navigation(), elseDD.navigation());
486  }
487 
488 private:
490  CExtrusivePtr<ring_type, node_type> p_node;
491 };
492 
493 
494 #undef PB_ZDD_APPLY
495 
497 
498 #endif