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 
186  diagram_type& operator=(const diagram_type& rhs) {
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  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 
387  diagram_type divideFirst(const diagram_type& rhs) const {
388 
389  diagram_type result(*this);
391  std::copy(rhs.firstBegin(), rhs.firstEnd(), outiter);
392 
393  return result;
394  }
395 
396 
398  ostream_type& print(ostream_type& os) const {
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 
411  first_iterator firstBegin() const {
412  return first_iterator(navigation());
413  }
414 
416  first_iterator firstEnd() const {
417  return first_iterator();
418  }
419 
421  last_iterator lastBegin() const {
422  return last_iterator(getNode());
423  }
424 
426  last_iterator lastEnd() const {
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 
445  diagram_type firstDivisors() const {
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 
455  navigator navigation() const {
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
#define PBORI_PREFIX(name)
Definition: prefix.h:27
bool_type isConstant() const
Checks whether the the diagram corresponds to {} or {{}} (polynomial 0 or 1)
Definition: CCuddDDFacade.h:460
~CCuddDDFacade()
Destructor.
Definition: CCuddDDFacade.h:183
node_type * node_ptr
Pointer type for nodes.
Definition: CCuddDDFacade.h:124
#define END_NAMESPACE_PBORI
Finish project's namespace.
Definition: pbori_defs.h:77
DdNode node_type
Type for C-style struct.
Definition: CCuddDDFacade.h:121
first_iterator firstEnd() const
Finish of first term.
Definition: CCuddDDFacade.h:416
diagram_type cudd_generate_divisors(const ManagerType &mgr, ReverseIterator start, ReverseIterator finish) const
temporarily (needs to be more generic) (similar fct in pbori_algo.h)
Definition: CCuddDDFacade.h:350
#define BEGIN_NAMESPACE_PBORI
Start project's namespace.
Definition: pbori_defs.h:74
bool isOne() const
Test whether diagram represents the empty set.
Definition: CCuddDDFacade.h:247
#define Cudd_RecursiveDerefZdd
Definition: prefix_internal.h:149
void PrintMinterm() const
Definition: CCuddDDFacade.h:220
diagram_type firstMultiples(const std::vector< idx_type > &input_multipliers) const
Get decison diagram representing the multiples of the first term.
Definition: CCuddDDFacade.h:431
#define Cudd_NodeReadIndex
Definition: prefix_internal.h:91
last_iterator lastBegin() const
Start of first term.
Definition: CCuddDDFacade.h:421
NodeType pboriCudd_zddUnionXor(MgrType dd, NodeType P, NodeType Q)
Definition: pbori_algo.h:755
#define Cudd_zddDiffConst
Definition: prefix_internal.h:175
CTypes::ostream_type ostream_type
Type for output streams.
Definition: CCuddDDFacade.h:112
#define cuddUniqueInterZdd
Definition: prefix_internal.h:181
double countDouble() const
Appriximate the number of terms.
Definition: CCuddDDFacade.h:229
#define cuddZddGetNode
Definition: prefix_internal.h:231
navigator navigation() const
Navigate through ZDD by incrementThen(), incrementElse(), and terminated()
Definition: CCuddDDFacade.h:455
CCheckedIdx checked_idx_type
Cudd's index type.
Definition: CCuddDDFacade.h:148
DDBase cudd_generate_divisors(const ManagerType &mgr, ReverseIterator start, ReverseIterator finish, type_tag< DDBase >)
temporarily (needs to be more generic) (similar fct in CCuddDDFacade.h)
Definition: pbori_algo.h:582
This template class defines a facade as a C++ interface for applying C-style functions to C-style str...
Definition: CApplyNodeFacade.h:41
CCuddDDFacade(const ring_type &ring, idx_type idx, navigator navi)
Definition: CCuddDDFacade.h:168
This struct contains auxiliary type definitions.
Definition: pbori_defs.h:210
This template class is used for polybori's exception handling.
Definition: PBoRiGenericError.h:35
std::ostream ostream_type
Type for out-stream.
Definition: pbori_defs.h:246
first_iterator firstBegin() const
Get numbers of used variables.
Definition: CCuddDDFacade.h:411
const ring_type & ring() const
Get reference to ring.
Definition: CCuddDDFacade.h:250
void extrusive_ptr_add_ref(const DataType &, DdNode *ptr)
Incrememting reference counts to raw pointers to decision diagrams.
Definition: CCuddDDFacade.h:75
bool isZero() const
Test whether diagram represents the empty set.
Definition: CCuddDDFacade.h:244
CCuddDDFacade(const ring_type &ring, node_ptr node)
Construct diagram from ring and node.
Definition: CCuddDDFacade.h:151
DiagramType diagram_type
Type for diagrams.
Definition: CCuddDDFacade.h:118
This class defines an iterator over the last minimal term of a given ZDD node.
Definition: CCuddLastIter.h:32
This template class defines a facade for decision diagrams.
Definition: CCuddDDFacade.h:103
valid_tag easy_equality_property
This type has an easy equality check.
Definition: CCuddDDFacade.h:139
ResultType memApply(ResultType(*func)(mgr_type *, node_ptr)) const
Definition: CCuddDDFacade.h:265
mgr_type * getManager() const
Get raw decision diagram manager.
Definition: CCuddDDFacade.h:256
diagram_type firstDivisors() const
Get decison diagram representing the divisors of the first term.
Definition: CCuddDDFacade.h:445
size_type refCount() const
Number of references pointing here.
Definition: CCuddDDFacade.h:238
#define PBORI_ASSERT(arg)
Definition: pbori_defs.h:118
last_iterator lastEnd() const
Finish of first term.
Definition: CCuddDDFacade.h:426
int idx_type
Type for indices.
Definition: pbori_defs.h:228
CCuddFirstIter first_iterator
Iterator type for retrieving first term from Cudd's ZDDs.
Definition: CCuddDDFacade.h:130
CCuddLastIter last_iterator
Iterator type for retrieving last term from Cudd's ZDDs.
Definition: CCuddDDFacade.h:133
size_type nNodes() const
Number of nodes in the current decision diagram.
Definition: CCuddDDFacade.h:235
This class defines an iterator over the first minimal term of a given ZDD node.
Definition: CCuddFirstIter.h:35
diagram_type cudd_generate_multiples(const ManagerType &mgr, ReverseIterator start, ReverseIterator finish, MultReverseIterator multStart, MultReverseIterator multFinish) const
temporarily (needs to be more generic) (similar fct in pbori_algo.h)
Definition: CCuddDDFacade.h:280
CCuddDDFacade(const ring_type &ring, idx_type idx, navigator thenNavi, navigator elseNavi)
Construct new node from manager, index, and navigators.
Definition: CCuddDDFacade.h:162
void checkAssumption(bool isValid) const
Check whether previous decision diagram operation for validity.
Definition: CCuddDDFacade.h:272
diagram_type divideFirst(const diagram_type &rhs) const
Division with first term of right-hand side.
Definition: CCuddDDFacade.h:387
#define Cudd_ReadZero
Definition: prefix_internal.h:46
int cudd_idx_type
Cudd's index type.
Definition: CCuddDDFacade.h:145
CCuddDDFacade(const self &from)
Copy constructor.
Definition: CCuddDDFacade.h:180
ring_type::mgr_type mgr_type
Raw context.
Definition: CCuddDDFacade.h:142
diagram_type & operator=(const diagram_type &rhs)
Assignment operator.
Definition: CCuddDDFacade.h:186
size_type count() const
Determine the number of terms.
Definition: CCuddDDFacade.h:226
DDBase cudd_generate_multiples(const ManagerType &mgr, ReverseIterator start, ReverseIterator finish, MultReverseIterator multStart, MultReverseIterator multFinish, type_tag< DDBase >)
temporarily (needs to be more generic) (similar fct in CCuddDDFacade.h)
Definition: pbori_algo.h:517
CApplyNodeFacade< diagram_type, node_ptr > base
Type this is inherited from the following.
Definition: CCuddDDFacade.h:127
polybori::CTypes::idx_type idx_type
Definition: groebner_defs.h:44
#define Cudd_Deref
Definition: prefix_internal.h:160
std::ostream & printIntern(std::ostream &os) const
Definition: CCuddDDFacade.h:209
std::size_t size_type
Type for lengths, dimensions, etc.
Definition: pbori_defs.h:219
CCuddDDFacade(idx_type idx, const self &thenDD, const self &elseDD)
Construct new node.
Definition: CCuddDDFacade.h:173
bool_type isValid() const
Check whether *this is not the default iterator self() (NULL pointer)
Definition: CCuddNavigator.h:125
This class defines an iterator for navigating through then and else branches of ZDDs.
Definition: CCuddNavigator.h:36
RingType ring_type
Type for diagrams.
Definition: CCuddDDFacade.h:115
diagram_type Xor(const diagram_type &rhs) const
Union Xor.
Definition: CCuddDDFacade.h:377
CCuddNavigator navigator
Iterator type for navigation throught Cudd's ZDDs structure.
Definition: CCuddDDFacade.h:136
This template class defines an output iterator which interprets assignments of indices as a change of...
Definition: PBoRiOutIter.h:31
void extrusive_ptr_release(const DataType &data, DdNode *ptr)
Releasing raw pointers to decision diagrams here.
Definition: CCuddDDFacade.h:66
bool bool_type
Type for standard true/false statements.
Definition: pbori_defs.h:216
CCuddDDFacade(const ring_type &ring, const navigator &navi)
Construct from Manager and navigator.
Definition: CCuddDDFacade.h:157
#define PBORI_UNLIKELY(expression)
Definition: pbori_defs.h:59
DdManager mgr_type
Definition: BoolePolyRing.h:90
size_type rootIndex() const
Get index of curent node.
Definition: CCuddDDFacade.h:232
ostream_type & print(ostream_type &os) const
Get number of nodes in decision diagram.
Definition: CCuddDDFacade.h:398
This class defines CNodeCounter.
Definition: CNodeCounter.h:30
#define PB_ZDD_APPLY(count, data, funcname)
Definition: CCuddDDFacade.h:97
const char * error_text(pbori_DdManager *mgr)
Definition: CCuddInterface.h:45
This class shows, whether a property of an order is valid.
Definition: tags.h:32
node_ptr getNode() const
Get raw node structure.
Definition: CCuddDDFacade.h:253
This class defines CCheckedIdx.
Definition: CCheckedIdx.h:29
#define Cudd_Ref
Definition: prefix_internal.h:157