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