16 #ifndef polybori_routines_pbori_algo_int_h_
17 #define polybori_routines_pbori_algo_int_h_
36 template<
class NaviType>
47 template<
class NaviType>
58 template<
class NaviType>
61 return navi.getNode();
64 template <
class MgrType>
70 template <
class MgrType,
class NaviType>
73 navi.recursiveDecRef(mgr);
126 template<
class NaviType,
class ReverseIterator,
class DDOperations>
129 ReverseIterator idxStart, ReverseIterator idxFinish,
130 const DDOperations& apply){
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;
137 vector_type indices(apply.nSupport(navi));
138 iterator iter(indices.begin());
140 NaviType multiples = navi;
142 while(!multiples.isConstant()) {
144 multiples.incrementThen();
148 const_reverse_iterator start(indices.rbegin()),
149 finish(indices.rend());
154 while(start != finish){
156 while( (idxStart != idxFinish) && (*idxStart > *start) ) {
157 apply.multiplesAssign(multiples, *idxStart);
160 apply.productAssign(multiples, *start);
161 if(idxStart != idxFinish)
171 template <
class NaviType>
175 while(!second.isConstant()){
176 while( (!first.isConstant()) && (*first < *second))
177 first.incrementThen();
178 if(*first != *second)
180 second.incrementThen();
185 template<
class NaviType,
class ReverseIterator,
class DDOperations>
188 ReverseIterator idxStart, ReverseIterator idxFinish,
189 const DDOperations& apply){
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;
200 size_type nmax = apply.nSupport(navi);
201 vector_type thenIdx(nmax), elseIdx(nmax);
206 NaviType thenNavi = navi;
207 NaviType elseNavi = navi;
210 NaviType tmp(elseNavi);
211 elseNavi.incrementElse();
213 while(!elseNavi.isConstant()){
215 elseNavi.incrementElse();
217 if(elseNavi.isEmpty())
222 bool isReducible =
true;
223 while (isReducible && !thenNavi.isConstant() && !elseNavi.isConstant()){
225 while( !thenNavi.isConstant() && (*thenNavi < *elseNavi)) {
230 thenIdx.push_back(*thenNavi);
231 thenNavi.incrementThen();
234 if(!thenNavi.isConstant() && (*thenNavi == *elseNavi) ){
235 thenIdx.push_back(*thenNavi);
236 thenNavi.incrementThen();
242 elseIdx.push_back(*elseNavi);
245 elseNavi.incrementThen();
246 if( !elseNavi.isConstant() ) {
249 elseNavi.incrementElse();
252 if( elseNavi.isEmpty() )
259 NaviType elseTail, elseMult;
260 apply.assign(elseTail, elseNavi);
265 if (!elseNavi.isConstant()) {
275 apply.assign(elseMult, elseTail);
279 idxStart, idxFinish, apply);
286 NaviType thenTail, thenMult;
292 apply.assign(thenTail, thenNavi);
295 if (!thenNavi.isConstant()){
306 apply.assign(thenMult, thenTail);
311 ReverseIterator idxIter = idxStart;
312 const_reverse_iterator start(elseIdx.rbegin()), finish(elseIdx.rend());
317 if(!elseMult.isConstant())
318 while((idxIter != idxFinish) && (*idxIter >= *elseMult) )
321 while(start != finish){
323 while((idxIter != idxFinish) && (*idxIter > *start) ) {
325 apply.multiplesAssign(elseMult, *idxIter);
328 apply.productAssign(elseMult, *start);
331 apply.productAssign(elseTail, *start);
333 if(idxIter != idxFinish)
339 multiples = elseMult;
353 const_reverse_iterator start2(thenIdx.rbegin()), finish2(thenIdx.rend());
354 ReverseIterator idxIter = idxStart;
362 if(!thenMult.isConstant())
363 while((idxIter != idxFinish) && (*idxIter >= *thenMult) )
370 while(start2 != finish2){
372 while((idxIter != idxFinish) && (*idxIter > *start2) ) {
374 apply.multiplesAssign(thenMult, *idxIter);
377 apply.productAssign(thenMult, *start2);
379 if(idxIter != idxFinish)
385 apply.replacingUnite(multiples, elseMult, thenMult);
401 apply.kill(elseTail);
402 apply.kill(thenTail);
405 return apply.newNode(navi);
438 template <
class NaviType,
class SizeType,
class ReverseIterator,
442 ReverseIterator start, ReverseIterator finish,
443 const DDOperations& apply) {
445 if (navi.isConstant()){
446 if (!navi.terminalValue())
450 while ( (start != finish) && (*start >= *navi) )
453 while( (start != finish) && (*start > minIdx) ){
454 apply.multiplesAssign(navi, *start);
460 template<
class FunctionType,
class ManagerType,
class NodeType>
462 NodeType& first,
const NodeType& second) {
472 template<
class FunctionType,
class ManagerType,
class ResultType,
476 const NodeType& first,
477 const NodeType& second) {
485 template<
class FunctionType,
class ManagerType,
class NodeType>
487 const NodeType& first,
const NodeType& second) {
495 template <
class DDType>
544 newNodeAssign(idx, node, node);
549 newNodeAssign(idx, node, emptyset);
584 template <
class NaviType,
class DDType2,
class ReverseIterator,
589 ReverseIterator idxStart, ReverseIterator idxEnd,
590 const DDOperations& apply) {
594 if (!navi.isConstant()) {
596 int nlen = apply.length(navi);
598 if(
false&&(nlen == 2)) {
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;
618 while( is_reducible&&(!multiples.isConstant())) {
622 thenBr = multiples.thenBranch();
623 elseBr = multiples.elseBranch();
625 if((elseBr.isConstant() && elseBr.terminalValue())) {
630 else if (elseBr.isConstant() && !elseBr.terminalValue())
633 if (!reducible_tested){
634 reducible_tested ==
true;
652 indices.resize(used);
656 std::vector<int>::const_reverse_iterator start(indices.rbegin()),
657 finish(indices.rend());
664 NaviType tmp,tmpnavi;
666 apply.assign(tmpnavi, multiples);
668 ReverseIterator idxIter = idxStart;
669 while(start != finish){
671 while((idxIter != idxEnd) && (*idxIter > *start) ) {
673 apply.multiplesAssign(multiples, *idxIter);
676 apply.productAssign(multiples, *start);
677 apply.productAssign(tmpnavi, *start);
678 if(idxIter != idxEnd)
700 return apply.newNode(navi);
707 elseMult, idxStart, idxEnd, apply);
709 idxStart, idxEnd, apply);
712 if( (navi.elseBranch() == navi.thenBranch()) ||
713 (elsedd.isConstant() && elsedd.terminalValue()) ){
714 multiples = elseMult;
719 NaviType thenNavi(apply.diff(navi.thenBranch(), elseMult));
724 idxStart, idxEnd, apply));
726 idxStart, idxEnd, apply);
729 apply.uniteAssign(thenMult, elseMult);
730 apply.replacingNode(multiples, *navi, thenMult, elseMult);
734 apply.replacingNode(result, *navi, thenNavi, elsedd);
740 apply.assign(multiples, navi);
742 return apply.newNode(navi);