63 #ifndef pbori_algo_int_h_
64 #define pbori_algo_int_h_
75 template<
class NaviType>
86 template<
class NaviType>
97 template<
class NaviType>
100 return navi.getNode();
103 template <
class MgrType>
106 Cudd_RecursiveDerefZdd(mgr, node);
109 template <
class MgrType,
class NaviType>
112 navi.recursiveDecRef(mgr);
165 template<
class NaviType,
class ReverseIterator,
class DDOperations>
168 ReverseIterator idxStart, ReverseIterator idxFinish,
169 const DDOperations& apply){
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;
176 vector_type indices(apply.nSupport(navi));
177 iterator iter(indices.begin());
179 NaviType multiples = navi;
181 while(!multiples.isConstant()) {
183 multiples.incrementThen();
187 const_reverse_iterator start(indices.rbegin()),
188 finish(indices.rend());
193 while(start != finish){
195 while( (idxStart != idxFinish) && (*idxStart > *start) ) {
196 apply.multiplesAssign(multiples, *idxStart);
199 apply.productAssign(multiples, *start);
200 if(idxStart != idxFinish)
210 template <
class NaviType>
214 while(!second.isConstant()){
215 while( (!first.isConstant()) && (*first < *second))
216 first.incrementThen();
217 if(*first != *second)
219 second.incrementThen();
224 template<
class NaviType,
class ReverseIterator,
class DDOperations>
227 ReverseIterator idxStart, ReverseIterator idxFinish,
228 const DDOperations& apply){
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;
239 size_type nmax = apply.nSupport(navi);
240 vector_type thenIdx(nmax), elseIdx(nmax);
245 NaviType thenNavi = navi;
246 NaviType elseNavi = navi;
249 NaviType tmp(elseNavi);
250 elseNavi.incrementElse();
252 while(!elseNavi.isConstant()){
254 elseNavi.incrementElse();
256 if(elseNavi.isEmpty())
261 bool isReducible =
true;
262 while (isReducible && !thenNavi.isConstant() && !elseNavi.isConstant()){
264 while( !thenNavi.isConstant() && (*thenNavi < *elseNavi)) {
269 thenIdx.push_back(*thenNavi);
270 thenNavi.incrementThen();
273 if(!thenNavi.isConstant() && (*thenNavi == *elseNavi) ){
274 thenIdx.push_back(*thenNavi);
275 thenNavi.incrementThen();
281 elseIdx.push_back(*elseNavi);
284 elseNavi.incrementThen();
285 if( !elseNavi.isConstant() ) {
288 elseNavi.incrementElse();
291 if( elseNavi.isEmpty() )
298 NaviType elseTail, elseMult;
299 apply.assign(elseTail, elseNavi);
304 if (!elseNavi.isConstant()) {
314 apply.assign(elseMult, elseTail);
318 idxStart, idxFinish, apply);
325 NaviType thenTail, thenMult;
331 apply.assign(thenTail, thenNavi);
334 if (!thenNavi.isConstant()){
345 apply.assign(thenMult, thenTail);
350 ReverseIterator idxIter = idxStart;
351 const_reverse_iterator start(elseIdx.rbegin()), finish(elseIdx.rend());
356 if(!elseMult.isConstant())
357 while((idxIter != idxFinish) && (*idxIter >= *elseMult) )
360 while(start != finish){
362 while((idxIter != idxFinish) && (*idxIter > *start) ) {
364 apply.multiplesAssign(elseMult, *idxIter);
367 apply.productAssign(elseMult, *start);
370 apply.productAssign(elseTail, *start);
372 if(idxIter != idxFinish)
378 multiples = elseMult;
392 const_reverse_iterator start2(thenIdx.rbegin()), finish2(thenIdx.rend());
393 ReverseIterator idxIter = idxStart;
401 if(!thenMult.isConstant())
402 while((idxIter != idxFinish) && (*idxIter >= *thenMult) )
409 while(start2 != finish2){
411 while((idxIter != idxFinish) && (*idxIter > *start2) ) {
413 apply.multiplesAssign(thenMult, *idxIter);
416 apply.productAssign(thenMult, *start2);
418 if(idxIter != idxFinish)
424 apply.replacingUnite(multiples, elseMult, thenMult);
440 apply.kill(elseTail);
441 apply.kill(thenTail);
444 return apply.newNode(navi);
477 template <
class NaviType,
class SizeType,
class ReverseIterator,
481 ReverseIterator start, ReverseIterator finish,
482 const DDOperations& apply) {
484 if (navi.isConstant()){
485 if (!navi.terminalValue())
489 while ( (start != finish) && (*start >= *navi) )
492 while( (start != finish) && (*start > minIdx) ){
493 apply.multiplesAssign(navi, *start);
499 template<
class FunctionType,
class ManagerType,
class NodeType>
501 NodeType& first,
const NodeType& second) {
511 template<
class FunctionType,
class ManagerType,
class ResultType,
515 const NodeType& first,
516 const NodeType& second) {
524 template<
class FunctionType,
class ManagerType,
class NodeType>
526 const NodeType& first,
const NodeType& second) {
534 template <
class DDType>
584 newNodeAssign(idx, node, node);
589 newNodeAssign(idx, node, emptyset);
603 return Cudd_SupportSize(mgr, node.
getNode());
606 return Cudd_zddCount(mgr, node.
getNode());
624 template <
class NaviType,
class DDType2,
class ReverseIterator,
629 ReverseIterator idxStart, ReverseIterator idxEnd,
630 const DDOperations& apply) {
634 if (!navi.isConstant()) {
636 int nlen = apply.length(navi);
638 if(
false&&(nlen == 2)) {
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;
658 while( is_reducible&&(!multiples.isConstant())) {
662 thenBr = multiples.thenBranch();
663 elseBr = multiples.elseBranch();
665 if((elseBr.isConstant() && elseBr.terminalValue())) {
670 else if (elseBr.isConstant() && !elseBr.terminalValue())
673 if (!reducible_tested){
674 reducible_tested ==
true;
692 indices.resize(used);
696 std::vector<int>::const_reverse_iterator start(indices.rbegin()),
697 finish(indices.rend());
704 NaviType tmp,tmpnavi;
706 apply.assign(tmpnavi, multiples);
708 ReverseIterator idxIter = idxStart;
709 while(start != finish){
711 while((idxIter != idxEnd) && (*idxIter > *start) ) {
713 apply.multiplesAssign(multiples, *idxIter);
716 apply.productAssign(multiples, *start);
717 apply.productAssign(tmpnavi, *start);
718 if(idxIter != idxEnd)
740 return apply.newNode(navi);
747 elseMult, idxStart, idxEnd, apply);
749 idxStart, idxEnd, apply);
752 if( (navi.elseBranch() == navi.thenBranch()) ||
753 (elsedd.isConstant() && elsedd.terminalValue()) ){
754 multiples = elseMult;
759 NaviType thenNavi(apply.diff(navi.thenBranch(), elseMult));
764 idxStart, idxEnd, apply));
766 idxStart, idxEnd, apply);
769 apply.uniteAssign(thenMult, elseMult);
770 apply.replacingNode(multiples, *navi, thenMult, elseMult);
774 apply.replacingNode(result, *navi, thenNavi, elsedd);
780 apply.assign(multiples, navi);
782 return apply.newNode(navi);