PolyBoRi
pbori_algo_int.h
Go to the documentation of this file.
1 // -*- c++ -*-
2 //*****************************************************************************
14 //*****************************************************************************
15 
16 #ifndef polybori_routines_pbori_algo_int_h_
17 #define polybori_routines_pbori_algo_int_h_
18 
19 // include polybori's definitions
20 #include <polybori/pbori_defs.h>
21 
22 // get polybori's functionals
23 #include "pbori_func.h"
25 #include <polybori/cudd/cudd.h>
26 
28 
29 
30 
31 inline void
32 inc_ref(DdNode* node) {
33  PBORI_PREFIX(Cudd_Ref)(node);
34 }
35 
36 template<class NaviType>
37 inline void
38 inc_ref(const NaviType & navi) {
39  navi.incRef();
40 }
41 
42 inline void
43 dec_ref(DdNode* node) {
44  PBORI_PREFIX(Cudd_Deref)(node);
45 }
46 
47 template<class NaviType>
48 inline void
49 dec_ref(const NaviType & navi) {
50  navi.decRef();
51 }
52 
53 inline DdNode*
54 do_get_node(DdNode* node) {
55  return node;
56 }
57 
58 template<class NaviType>
59 inline DdNode*
60 do_get_node(const NaviType & navi) {
61  return navi.getNode();
62 }
63 
64 template <class MgrType>
65 inline void
66 recursive_dec_ref(const MgrType& mgr, DdNode* node) {
68 }
69 
70 template <class MgrType, class NaviType>
71 inline void
72 recursive_dec_ref(const MgrType& mgr, const NaviType & navi) {
73  navi.recursiveDecRef(mgr);
74 }
75 
76 // template<class NaviType, class SizeType, class ManagerType>
77 // NaviType
78 // multiples_of_one_term(NaviType navi, SizeType nmax, ManagerType& man){
79 
80 
81 // std::vector<int> indices (PBORI_PREFIX(Cudd_SupportSize)(man,navi));
82 // std::vector<int>::iterator iter(indices.begin());
83 
84 // NaviType multiples = navi;
85 
86 // while(!multiples.isConstant()) {
87 // *iter = *multiples;
88 // multiples.incrementThen();
89 // ++iter;
90 // }
91 
92 // std::vector<int>::const_reverse_iterator start(indices.rbegin()),
93 // finish(indices.rend());
94 
95 // // int nmax = dd.nVariables();
96 
97 // PBORI_PREFIX(Cudd_Ref)(multiples);
98 // NaviType emptyset = navi.elseBranch();
99 
100 // NaviType tmp;
101 // SizeType i = nmax-1;
102 
103 // while(start != finish){
104 
105 // while ((idxStart != idxFinish) && (*idxStart > *start))
106 // // while(i > *start) {
107 
108 // tmp = cuddZddGetNode(man, i, multiples, multiples);
109 // PBORI_PREFIX(Cudd_Ref)(tmp);
110 // PBORI_PREFIX(Cudd_Deref)(multiples);
111 // multiples = tmp;
112 // --i;
113 // }
114 // tmp = cuddZddGetNode(man, i, multiples, emptyset);
115 // PBORI_PREFIX(Cudd_Ref)(tmp);
116 // PBORI_PREFIX(Cudd_Deref)(multiples);
117 // multiples = tmp;
118 // --i;
119 // ++start;
120 // }
121 
122 // return multiples;
123 // }
124 
125 
126 template<class NaviType, class ReverseIterator, class DDOperations>
127 NaviType
128 indexed_term_multiples(NaviType navi,
129  ReverseIterator idxStart, ReverseIterator idxFinish,
130  const DDOperations& apply){
131 
132  typedef typename NaviType::value_type idx_type;
133  typedef typename std::vector<idx_type> vector_type;
134  typedef typename vector_type::iterator iterator;
135  typedef typename vector_type::const_reverse_iterator const_reverse_iterator;
136 
137  vector_type indices(apply.nSupport(navi));
138  iterator iter(indices.begin());
139 
140  NaviType multiples = navi;
141 
142  while(!multiples.isConstant()) {
143  *iter = *multiples;
144  multiples.incrementThen();
145  ++iter;
146  }
147 
148  const_reverse_iterator start(indices.rbegin()),
149  finish(indices.rend());
150 
151 
152  inc_ref(multiples);
153 
154  while(start != finish){
155 
156  while( (idxStart != idxFinish) && (*idxStart > *start) ) {
157  apply.multiplesAssign(multiples, *idxStart);
158  ++idxStart;
159  }
160  apply.productAssign(multiples, *start);
161  if(idxStart != idxFinish)
162  ++idxStart;
163 
164  ++start;
165  }
166 
167  return multiples;
168 }
169 
170 
171 template <class NaviType>
172 bool
173 is_reducible_by(NaviType first, NaviType second){
174 
175  while(!second.isConstant()){
176  while( (!first.isConstant()) && (*first < *second))
177  first.incrementThen();
178  if(*first != *second)
179  return false;
180  second.incrementThen();
181  }
182  return true;
183 }
184 
185 template<class NaviType, class ReverseIterator, class DDOperations>
186 NaviType
187 minimal_of_two_terms(NaviType navi, NaviType& multiples,
188  ReverseIterator idxStart, ReverseIterator idxFinish,
189  const DDOperations& apply){
190 
191  typedef typename NaviType::value_type idx_type;
192  typedef typename std::vector<idx_type> vector_type;
193  typedef typename vector_type::iterator iterator;
194  typedef typename vector_type::size_type size_type;
195  typedef typename vector_type::const_reverse_iterator const_reverse_iterator;
196 
197  // std::cout <<"2s ";
198 
199 
200  size_type nmax = apply.nSupport(navi);
201  vector_type thenIdx(nmax), elseIdx(nmax);
202 
203  thenIdx.resize(0);
204  elseIdx.resize(0);
205 
206  NaviType thenNavi = navi;
207  NaviType elseNavi = navi;
208 
209  // See CCuddLastIterator
210  NaviType tmp(elseNavi);
211  elseNavi.incrementElse();
212 
213  while(!elseNavi.isConstant()){
214  tmp = elseNavi;
215  elseNavi.incrementElse();
216  }
217  if(elseNavi.isEmpty())
218  elseNavi = tmp;
219 
220  // std::cout <<"TH "<<*thenNavi <<" "<<*elseNavi<< ":";
221 
222  bool isReducible = true;
223  while (isReducible && !thenNavi.isConstant() && !elseNavi.isConstant()){
224 
225  while( !thenNavi.isConstant() && (*thenNavi < *elseNavi)) {
226  // std::cout <<"th "<<*thenNavi <<" "<<*elseNavi<< ":";
227 
228 // apply.print(thenNavi);
229 // apply.print(elseNavi);
230  thenIdx.push_back(*thenNavi);
231  thenNavi.incrementThen();
232  }
233 
234  if(!thenNavi.isConstant() && (*thenNavi == *elseNavi) ){
235  thenIdx.push_back(*thenNavi);
236  thenNavi.incrementThen();
237  }
238  else
239  isReducible = false;
240  // std::cout <<""<<isReducible << thenNavi.isConstant()<<std::endl;
241 
242  elseIdx.push_back(*elseNavi);
243 
244  // next on last path
245  elseNavi.incrementThen();
246  if( !elseNavi.isConstant() ) { // if still in interior of a path
247 
248  tmp = elseNavi; // store copy of *this
249  elseNavi.incrementElse(); // go in direction of last term, if possible
250 
251  // restore previous value, of else branch was invalid
252  if( elseNavi.isEmpty() )
253  elseNavi = tmp;
254 
255  }
256  }
257 
258 
259  NaviType elseTail, elseMult;
260  apply.assign(elseTail, elseNavi);
261 
263  // int initref = ((DdNode*)elseNavi)->ref;
264  // std::cout << ((DdNode*)elseNavi)->ref <<std::endl;
265  if (!elseNavi.isConstant()) {
266  isReducible = false;
267  elseMult =
268  indexed_term_multiples(elseTail, idxStart, idxFinish, apply);
269 // if(elseMult==elseTail)
270 // PBORI_PREFIX(Cudd_Deref)(elseMult);
271  }
272  else {
275  apply.assign(elseMult, elseTail);
276  }
277 
278 NaviType tmp2 = prepend_multiples_wrt_indices(elseMult, *navi,
279  idxStart, idxFinish, apply);
280 
281 tmp2.incRef();
282 elseMult.decRef();
283  elseMult = tmp2;
284  // std::cerr<< "h1"<<std::endl;
285 
286  NaviType thenTail, thenMult;
287 
288  if(!isReducible){
289 
290 // if(!thenNavi.isConstant())
291 // std::cout << " "<<(*thenNavi)<< " "<< *idxStart<<std::endl;
292  apply.assign(thenTail, thenNavi);
294 
295  if (!thenNavi.isConstant()){
296 
297  thenMult =
298  indexed_term_multiples(thenTail, idxStart, idxFinish, apply);
299 // if(thenMult==thenTail)
300 // PBORI_PREFIX(Cudd_Deref)(thenMult);
301 //PBORI_PREFIX(Cudd_Deref)(thenTail);///
303  }
304  else{
306  apply.assign(thenMult, thenTail);
307  }
308  }
309  // std::cerr<< "h2"<<std::endl;
310  // generating elsePath and multiples
311  ReverseIterator idxIter = idxStart;
312  const_reverse_iterator start(elseIdx.rbegin()), finish(elseIdx.rend());
313 
314  // PBORI_PREFIX(Cudd_Ref)(elseMult);
315  // std::cout << "isRed"<< isReducible <<std::endl;
316 
317  if(!elseMult.isConstant())
318  while((idxIter != idxFinish) && (*idxIter >= *elseMult) )
319  ++idxIter;
320 
321  while(start != finish){
322 
323  while((idxIter != idxFinish) && (*idxIter > *start) ) {
324 
325  apply.multiplesAssign(elseMult, *idxIter);
326  ++idxIter;
327  }
328  apply.productAssign(elseMult, *start);
329 
330  if (isReducible)
331  apply.productAssign(elseTail, *start);
332 
333  if(idxIter != idxFinish)
334  ++idxIter;
335  ++start;
336  }
337  // std::cerr<< "h3"<<std::endl;
338  if (isReducible){
339  multiples = elseMult;
340 
341 
343  // PBORI_PREFIX(Cudd_Ref)(elseTail);
344  //PBORI_PREFIX(Cudd_Deref)(thenTail);
345  //PBORI_PREFIX(Cudd_Deref)(thenMult);
346 
347  // std::cerr<< "h4"<<std::endl;
348  return elseTail;
349  }
350  else {
351 
352  // std::cerr<< "h5"<<std::endl;
353  const_reverse_iterator start2(thenIdx.rbegin()), finish2(thenIdx.rend());
354  ReverseIterator idxIter = idxStart;
355 
356  // PBORI_PREFIX(Cudd_Ref)(thenMult);
357 // NaviType printer = thenMult; std::cout<< "thenMult"<<std::endl;
358 // while(!printer.isConstant()){
359 // std::cout<< *printer <<" & ";
360 // printer.incrementThen();
361 // }
362  if(!thenMult.isConstant())
363  while((idxIter != idxFinish) && (*idxIter >= *thenMult) )
364  ++idxIter;
365 
366 
367  // std::cerr<< "h6"<<std::endl;
368 
369 
370  while(start2 != finish2){
371 
372  while((idxIter != idxFinish) && (*idxIter > *start2) ) {
373  // std::cout<< *idxIter <<" ? ";
374  apply.multiplesAssign(thenMult, *idxIter);
375  ++idxIter;
376  }
377  apply.productAssign(thenMult, *start2);
378  // apply.productAssign(thenTail, *start);
379  if(idxIter != idxFinish)
380  ++idxIter;
381  ++start2;
382  }
383 
384 
385  apply.replacingUnite(multiples, elseMult, thenMult);
386 
387 
388 
389  // std::cerr<< "h7"<<std::endl;
390 // printer = multiples; std::cout<< "mu"<<std::endl;
391 // while(!printer.isConstant()){
392 // // std::cout<< *printer <<" & ";
393 // printer.incrementThen();
394 // }
395  // std::cout<< std::endl;
397  // return apply.newNode(navi);
398  // std::cout << " "<<((DdNode*)thenTail)->ref<<std::endl;
399  // std::cerr<< "h8"<<std::endl;
400 
401  apply.kill(elseTail);
402  apply.kill(thenTail);
403 
404 
405  return apply.newNode(navi);
406  }
407 
408 
409 
410 // // remainder of first term
411 // while (!thenNavi.isConstant() ){
412 // thenIdx.push_back(*thenNavi);
413 // thenIdx.incrementThen();
414 // }
415 
416 // // remainder of last term
417 // while (!elseNavi.isConstant()){
418 // elseIdx.push_back(*elseNavi);
419 
420 // elseIdx.incrementThen();
421 // if( !elseIdx.isConstant() ) { // if still in interior of a path
422 
423 // tmp = elseNavi; // store copy of *this
424 // elseNavi.incrementElse(); // go in direction of last term, if possible
425 
426 // // restore previous value, of else branch was invalid
427 // if( elseNavi.isEmpty() )
428 // elseNavi = tmp;
429 // }
430 // isReducible = false;
431 // }
432 
433 
434 
435 }
436 
437 
438 template <class NaviType, class SizeType, class ReverseIterator,
439  class DDOperations>
440 NaviType
441 prepend_multiples_wrt_indices(NaviType navi, SizeType minIdx,
442  ReverseIterator start, ReverseIterator finish,
443  const DDOperations& apply) {
444 
445  if (navi.isConstant()){
446  if (!navi.terminalValue())
447  return navi;
448  }
449  else
450  while ( (start != finish) && (*start >= *navi) )
451  ++start;
452 
453  while( (start != finish) && (*start > minIdx) ){
454  apply.multiplesAssign(navi, *start);
455  ++start;
456  }
457  return navi;
458 }
459 
460 template<class FunctionType, class ManagerType, class NodeType>
461 void apply_assign_cudd_function(FunctionType func, ManagerType& mgr,
462  NodeType& first, const NodeType& second) {
463 
464  NodeType newNode(func(mgr, do_get_node(first), do_get_node(second)));
465  inc_ref(newNode);
466  recursive_dec_ref(mgr, first);
467  first = newNode;
468 }
469 
470 
471 
472 template<class FunctionType, class ManagerType, class ResultType,
473  class NodeType>
474 void apply_replacing_cudd_function(FunctionType func, ManagerType& mgr,
475  ResultType& newNode,
476  const NodeType& first,
477  const NodeType& second) {
478 
479  newNode = NodeType(func(mgr, do_get_node(first), do_get_node(second)));
480  inc_ref(newNode);
481  recursive_dec_ref(mgr, first);
482  recursive_dec_ref(mgr, second);
483 }
484 
485 template<class FunctionType, class ManagerType, class NodeType>
486 NodeType apply_cudd_function(FunctionType func, ManagerType& mgr,
487  const NodeType& first, const NodeType& second) {
488 
489  NodeType newNode;
490  newNode = NodeType(func(mgr, do_get_node(first), do_get_node(second)));
491  inc_ref(newNode);
492  return newNode;
493 }
494 
495 template <class DDType>
497 
498 template<>
500  public CAuxTypes {
501 public:
504 
505 
506  dd_operations(manager_type man): mgr(man) {}
507  void replacingUnite(navigator& newNode,
508  const navigator& first, const navigator& second) const {
509 
510  apply_replacing_cudd_function(PBORI_PREFIX(Cudd_zddUnion), mgr, newNode, first, second);
511  }
512 
513  void uniteAssign(navigator& first, const navigator& second) const {
515  }
516  void diffAssign(navigator& first, const navigator& second) const {
518  }
519  navigator diff(const navigator& first, const navigator& second) const {
520  return apply_cudd_function(PBORI_PREFIX(Cudd_zddDiff), mgr, first, second);
521  }
522  void replacingNode(navigator& newNode, idx_type idx,
523  navigator& first, navigator& second) const {
524 
525  newNode = navigator(PBORI_PREFIX(cuddZddGetNode)(mgr, idx, first.getNode(),
526  second.getNode()));
527  newNode.incRef();
528  recursive_dec_ref(mgr, first);
529  recursive_dec_ref(mgr, second);
530  }
531 
533  navigator& thenNode, const navigator& elseNode) const {
534  navigator newNode = navigator(PBORI_PREFIX(cuddZddGetNode)(mgr, idx,
535  thenNode.getNode(),
536  elseNode.getNode()));
537  newNode.incRef();
538  //PBORI_PREFIX(Cudd_Deref)(thenNode);
539  recursive_dec_ref(mgr, thenNode);
540  thenNode = newNode;
541  }
542 
543  void multiplesAssign(navigator& node, idx_type idx) const {
544  newNodeAssign(idx, node, node);
545  }
546 
547  void productAssign(navigator& node, idx_type idx) const {
548  navigator emptyset = navigator(PBORI_PREFIX(Cudd_ReadZero)(mgr));
549  newNodeAssign(idx, node, emptyset);
550  }
551 
552  void assign(navigator& first, const navigator& second) const {
553 
554  first = second;
555  first.incRef();
556  }
557  void replace(navigator& first, const navigator& second) const {
558  recursive_dec_ref(mgr, first);
559  first = second;
560  }
561 
562  size_type nSupport(const navigator& node) const {
563  return PBORI_PREFIX(Cudd_SupportSize)(mgr, node.getNode());
564  }
565  size_type length(const navigator& node) const {
566  return PBORI_PREFIX(Cudd_zddCount)(mgr, node.getNode());
567  }
568 
569  navigator& newNode(navigator& node) const {
570  node.incRef();
571  return node;
572  }
573 
574  void kill(navigator& node) const {
575  recursive_dec_ref(mgr, node);
576  }
577 protected:
578  manager_type mgr;
579 };
580 
584 template <class NaviType, class DDType2, class ReverseIterator,
585  class DDOperations>
586 //DDType
587 NaviType
588 dd_minimal_elements(NaviType navi,DDType2& multiples,
589  ReverseIterator idxStart, ReverseIterator idxEnd,
590  const DDOperations& apply) {
591 
592 
593 
594  if (!navi.isConstant()) { // Not at end of path
595 
596  int nlen = apply.length(navi);
597 
598  if(false&&(nlen == 2)) {
599 
600  // std::cerr << "hier"<<std::endl;
601  navi = minimal_of_two_terms(navi, multiples,idxStart, idxEnd, apply);
602 
603  // std::cerr << "danach"<<std::endl;
604  return navi;
605 
606 #if 0
607  multiples = navi;
608 
609 
610  std::vector<int> indices (apply.nSupport(navi));
611  std::vector<int>::iterator iter(indices.begin()), iend(indices.end());
612  bool is_reducible = true;
613  bool reducible_tested = false;
614 
615  int used = 0;
616  NaviType thenBr;
617  NaviType elseBr;
618  while( is_reducible&&(!multiples.isConstant())) {
619  *iter = *multiples;
620  used++;
621 
622  thenBr = multiples.thenBranch();
623  elseBr = multiples.elseBranch();
624 
625  if((elseBr.isConstant() && elseBr.terminalValue())) {
626  --iter;
627  --used;
628  multiples = elseBr;
629  }
630  else if (elseBr.isConstant() && !elseBr.terminalValue())
631  multiples = thenBr;
632  else {
633  if (!reducible_tested){
634  reducible_tested == true;
635  is_reducible = is_reducible_by(thenBr, elseBr);
636  }
637  if(is_reducible){
638  --iter;
639  --used;
640  }
641 
642  multiples = elseBr;
643  }
644 
645 
646  ++iter;
647 
648  }
649 
650 
651 
652  indices.resize(used);
653 
654  if (is_reducible) {
655 
656  std::vector<int>::const_reverse_iterator start(indices.rbegin()),
657  finish(indices.rend());
658 
659  // int nmax = dd.nVariables();
660 
661  inc_ref(multiples);
662 
663 
664  NaviType tmp,tmpnavi;
665 
666  apply.assign(tmpnavi, multiples);
667 
668  ReverseIterator idxIter = idxStart;
669  while(start != finish){
670 
671  while((idxIter != idxEnd) && (*idxIter > *start) ) {
672 
673  apply.multiplesAssign(multiples, *idxIter);
674  ++idxIter;
675  }
676  apply.productAssign(multiples, *start);
677  apply.productAssign(tmpnavi, *start);
678  if(idxIter != idxEnd)
679  ++idxIter;
680  ++start;
681  }
682 
683  navi = tmpnavi;
684  return navi;
685  }
686 // else { // Subcase: two proper terms
687 
688 // thenBr = indexed_term_multiples(thenBr, idxStart, idxEnd, apply);
689 // elseBr = indexed_term_multiples(elseBr, idxStart, idxEnd, apply);
690 
691 // }
692 #endif
693  }
694 
695 
696 
697  if(nlen == 1) { // Special case of only one term
698  // PBORI_PREFIX(Cudd_Ref)(navi);
699  multiples = indexed_term_multiples(navi, idxStart, idxEnd, apply);
700  return apply.newNode(navi);
701  }
702 
703 
704  // treat else branch
705  NaviType elseMult;
706  NaviType elsedd = dd_minimal_elements(navi.elseBranch(),
707  elseMult, idxStart, idxEnd, apply);
708  elseMult = prepend_multiples_wrt_indices(elseMult, *navi,
709  idxStart, idxEnd, apply);
710 
711  // short cut for obvious inclusion
712  if( (navi.elseBranch() == navi.thenBranch()) ||
713  (elsedd.isConstant() && elsedd.terminalValue()) ){
714  multiples = elseMult;
715  return elsedd;
716  }
717 
718  // remove already treated branches
719  NaviType thenNavi(apply.diff(navi.thenBranch(), elseMult));
720 
721  // treat remaining parts of then branch
722  NaviType thenMult;
723  apply.replace(thenNavi, dd_minimal_elements(thenNavi, thenMult,
724  idxStart, idxEnd, apply));
725  thenMult = prepend_multiples_wrt_indices(thenMult, *navi,
726  idxStart, idxEnd, apply);
727 
728  // generate node consisting of all multiples
729  apply.uniteAssign(thenMult, elseMult);
730  apply.replacingNode(multiples, *navi, thenMult, elseMult);
731 
732  // generate result from minimal elements of then and else brach
733  NaviType result;
734  apply.replacingNode(result, *navi, thenNavi, elsedd);
735 
736  return result;
737 
738  }
739 
740  apply.assign(multiples, navi);
741 
742  return apply.newNode(navi);
743 }
744 
746 
747 #endif
#define PBORI_PREFIX(name)
Definition: prefix.h:27
void replacingUnite(navigator &newNode, const navigator &first, const navigator &second) const
Definition: pbori_algo_int.h:507
#define END_NAMESPACE_PBORI
Finish project's namespace.
Definition: pbori_defs.h:77
DdManager * manager_type
Definition: pbori_algo_int.h:502
#define BEGIN_NAMESPACE_PBORI
Start project's namespace.
Definition: pbori_defs.h:74
NaviType minimal_of_two_terms(NaviType navi, NaviType &multiples, ReverseIterator idxStart, ReverseIterator idxFinish, const DDOperations &apply)
Definition: pbori_algo_int.h:187
void replace(navigator &first, const navigator &second) const
Definition: pbori_algo_int.h:557
#define Cudd_RecursiveDerefZdd
Definition: prefix_internal.h:149
void replacingNode(navigator &newNode, idx_type idx, navigator &first, navigator &second) const
Definition: pbori_algo_int.h:522
void incRef() const
Force incrementation of reference count.
Definition: CCuddNavigator.h:142
NaviType prepend_multiples_wrt_indices(NaviType navi, SizeType minIdx, ReverseIterator start, ReverseIterator finish, const DDOperations &apply)
Definition: pbori_algo_int.h:441
navigator diff(const navigator &first, const navigator &second) const
Definition: pbori_algo_int.h:519
void apply_replacing_cudd_function(FunctionType func, ManagerType &mgr, ResultType &newNode, const NodeType &first, const NodeType &second)
Definition: pbori_algo_int.h:474
#define cuddZddGetNode
Definition: prefix_internal.h:231
#define Cudd_zddDiff
Definition: prefix_internal.h:172
DdNode * do_get_node(const NaviType &navi)
Definition: pbori_algo_int.h:60
This struct contains auxiliary type definitions.
Definition: pbori_defs.h:210
void assign(navigator &first, const navigator &second) const
Definition: pbori_algo_int.h:552
void recursive_dec_ref(const MgrType &mgr, const NaviType &navi)
Definition: pbori_algo_int.h:72
void productAssign(navigator &node, idx_type idx) const
Definition: pbori_algo_int.h:547
#define Cudd_zddUnion
Definition: prefix_internal.h:174
navigator & newNode(navigator &node) const
Definition: pbori_algo_int.h:569
Definition: pbori_algo_int.h:496
size_type length(const navigator &node) const
Definition: pbori_algo_int.h:565
dd_operations(manager_type man)
Definition: pbori_algo_int.h:506
size_type nSupport(const navigator &node) const
Definition: pbori_algo_int.h:562
pbori_DdManager DdManager
Definition: traits.h:33
void inc_ref(const NaviType &navi)
Definition: pbori_algo_int.h:38
int idx_type
Type for indices.
Definition: pbori_defs.h:228
void diffAssign(navigator &first, const navigator &second) const
Definition: pbori_algo_int.h:516
const_access_type getNode() const
Constant pointer access operator.
Definition: CCuddNavigator.h:107
#define Cudd_ReadZero
Definition: prefix_internal.h:46
manager_type mgr
Definition: pbori_algo_int.h:578
void kill(navigator &node) const
Definition: pbori_algo_int.h:574
NaviType indexed_term_multiples(NaviType navi, ReverseIterator idxStart, ReverseIterator idxFinish, const DDOperations &apply)
Definition: pbori_algo_int.h:128
polybori::CTypes::idx_type idx_type
Definition: groebner_defs.h:44
#define Cudd_Deref
Definition: prefix_internal.h:160
void multiplesAssign(navigator &node, idx_type idx) const
Definition: pbori_algo_int.h:543
std::size_t size_type
Type for lengths, dimensions, etc.
Definition: pbori_defs.h:219
This class defines an iterator for navigating through then and else branches of ZDDs.
Definition: CCuddNavigator.h:36
bool is_reducible_by(NaviType first, NaviType second)
Definition: pbori_algo_int.h:173
NaviType dd_minimal_elements(NaviType navi, DDType2 &multiples, ReverseIterator idxStart, ReverseIterator idxEnd, const DDOperations &apply)
Definition: pbori_algo_int.h:588
void dec_ref(const NaviType &navi)
Definition: pbori_algo_int.h:49
void apply_assign_cudd_function(FunctionType func, ManagerType &mgr, NodeType &first, const NodeType &second)
Definition: pbori_algo_int.h:461
NodeType apply_cudd_function(FunctionType func, ManagerType &mgr, const NodeType &first, const NodeType &second)
Definition: pbori_algo_int.h:486
void newNodeAssign(idx_type idx, navigator &thenNode, const navigator &elseNode) const
Definition: pbori_algo_int.h:532
CCuddNavigator navigator
Definition: pbori_algo_int.h:503
void uniteAssign(navigator &first, const navigator &second) const
Definition: pbori_algo_int.h:513
#define Cudd_Ref
Definition: prefix_internal.h:157