15 #ifndef polybori_routines_pbori_routines_misc_h_
16 #define polybori_routines_pbori_routines_misc_h_
28 template<
class Iterator>
29 typename Iterator::value_type
32 typedef typename Iterator::value_type value_type;
37 while (start != finish){
39 sum += ((*start)+1) * ((*start)+1);
47 template <
class DegreeCacher,
class NaviType>
53 if (navi.isConstant()){
54 if (navi.terminalValue())
61 typename DegreeCacher::node_type result = cache.find(navi);
72 cache.insert(navi, deg);
81 template <
class DegreeCacher,
class NaviType,
class SizeType>
93 while(!navi.isConstant())
96 if (navi.isConstant())
97 return (navi.terminalValue()? 0: -1);
100 typename DegreeCacher::node_type result = cache.find(navi, bound);
101 if (result.isValid())
115 cache.insert(navi, bound, deg);
121 template <
class Iterator,
class NameGenerator,
122 class Separator,
class EmptySetType,
125 dd_print_term(Iterator start, Iterator finish,
const NameGenerator& get_name,
126 const Separator& sep,
const EmptySetType& emptyset,
129 if (start != finish){
130 os << get_name(*start);
136 while (start != finish){
137 os << sep() << get_name(*start);
142 template <
class TermType,
class NameGenerator,
143 class Separator,
class EmptySetType,
147 const Separator& sep,
const EmptySetType& emptyset,
149 dd_print_term(term.begin(), term.end(), get_name, sep, emptyset, os);
153 template <
class Iterator,
class NameGenerator,
154 class Separator,
class InnerSeparator,
155 class EmptySetType,
class OStreamType>
158 const Separator& sep,
const InnerSeparator& innersep,
159 const EmptySetType& emptyset, OStreamType& os) {
161 if (start != finish){
166 while (start != finish){
175 template <
bool use_fast,
176 class CacheType,
class NaviType,
class PolyType>
179 NaviType firstNavi, NaviType secondNavi, PolyType init){
182 typedef typename PolyType::dd_type dd_type;
184 typedef NaviType navigator;
186 if (firstNavi.isConstant()) {
187 if(firstNavi.terminalValue())
188 return cache_mgr.generate(secondNavi);
190 return cache_mgr.zero();
193 if (secondNavi.isConstant()) {
194 if(secondNavi.terminalValue())
195 return cache_mgr.generate(firstNavi);
197 return cache_mgr.zero();
199 if (firstNavi == secondNavi)
200 return cache_mgr.generate(firstNavi);
203 navigator cached = cache_mgr.find(firstNavi, secondNavi);
204 PolyType result(cache_mgr.zero());
206 if (cached.isValid()) {
207 return cache_mgr.generate(cached);
212 if (*secondNavi < *firstNavi)
213 std::swap(firstNavi, secondNavi);
215 idx_type index = *firstNavi;
218 navigator as0 = firstNavi.elseBranch();
219 navigator as1 = firstNavi.thenBranch();
224 if (*secondNavi == index) {
225 bs0 = secondNavi.elseBranch();
226 bs1 = secondNavi.thenBranch();
230 bs1 = cache_mgr.zero().navigation();
232 PolyType result0 = dd_multiply<use_fast>(cache_mgr, as0, bs0, init);
233 PolyType result1(cache_mgr.zero());
236 if (use_fast && (*firstNavi == *secondNavi)) {
238 PolyType res10 = PolyType(cache_mgr.generate(as1)) +
239 PolyType(cache_mgr.generate(as0));
240 PolyType res01 = PolyType(cache_mgr.generate(bs0)) +
241 PolyType(cache_mgr.generate(bs1));
243 result1 = dd_multiply<use_fast>(cache_mgr, res10.navigation(),
244 res01.navigation(), init) - result0;
247 else if (as0 == as1) {
248 result1 = dd_multiply<use_fast>(cache_mgr, bs0, as1, init);
252 result1 = dd_multiply<use_fast>(cache_mgr, as0, bs1, init);
254 PolyType bs01 = PolyType(cache_mgr.generate(bs0)) +
255 PolyType(cache_mgr.generate(bs1));
258 dd_multiply<use_fast>(cache_mgr, bs01.navigation(), as1, init);
261 result = dd_type(index, result1.diagram(), result0.diagram());
264 cache_mgr.insert(firstNavi, secondNavi, result.navigation());
270 template <
class CacheType,
class NaviType,
class PolyType>
273 NaviType firstNavi, NaviType secondNavi, PolyType init){
276 #ifdef PBORI_FAST_MULTIPLICATION
283 return dd_multiply<use_fast>(cache_mgr, firstNavi, secondNavi, init);
286 template <
class CacheType,
class NaviType,
class PolyType>
289 NaviType monomNavi, NaviType navi, PolyType init){
292 typedef typename PolyType::dd_type dd_type;
294 typedef NaviType navigator;
296 if (monomNavi.isConstant()) {
297 if(monomNavi.terminalValue())
298 return cache_mgr.generate(navi);
300 return cache_mgr.zero();
305 if (navi.isConstant()) {
306 if(navi.terminalValue())
307 return cache_mgr.generate(monomNavi);
309 return cache_mgr.zero();
311 if (monomNavi == navi)
312 return cache_mgr.generate(monomNavi);
315 navigator cached = cache_mgr.find(monomNavi, navi);
317 if (cached.isValid()) {
318 return cache_mgr.generate(cached);
324 idx_type index = *navi;
325 idx_type monomIndex = *monomNavi;
327 if (monomIndex < index) {
329 init).diagram().change(monomIndex);
331 else if (monomIndex == index) {
334 navigator monomThen = monomNavi.thenBranch();
335 navigator naviThen = navi.thenBranch();
336 navigator naviElse = navi.elseBranch();
338 if (naviThen != naviElse)
341 init)).diagram().change(index);
354 cache_mgr.insert(monomNavi, navi, init.navigation());
360 template <
class DDGenerator,
class Iterator,
class NaviType,
class PolyType>
363 Iterator start, Iterator finish,
364 NaviType navi, PolyType init){
367 typedef typename PolyType::dd_type dd_type;
368 typedef NaviType navigator;
371 return ddgen.generate(navi);
373 PolyType result(ddgen.zero());
374 if (navi.isConstant()) {
375 if(navi.terminalValue()) {
377 std::reverse_iterator<Iterator> rstart(finish), rfinish(start);
378 result = ddgen.generate(navi);
379 while (rstart != rfinish) {
380 result = result.diagram().change(*rstart);
393 idx_type index = *navi;
394 idx_type monomIndex = *start;
396 if (monomIndex < index) {
398 Iterator next(start);
399 while( (next != finish) && (*next < index) )
404 std::reverse_iterator<Iterator> rstart(next), rfinish(start);
405 while (rstart != rfinish) {
406 result = result.diagram().change(*rstart);
410 else if (monomIndex == index) {
415 navigator naviThen = navi.thenBranch();
416 navigator naviElse = navi.elseBranch();
418 if (naviThen != naviElse)
421 init)).diagram().change(index);
428 navi.thenBranch(), init).diagram(),
430 navi.elseBranch(), init).diagram() );
436 template<
class DegCacheMgr,
class NaviType,
class SizeType>
438 SizeType degree,
valid_tag is_descending) {
440 navi.incrementThen();
444 template<
class DegCacheMgr,
class NaviType,
class SizeType>
448 navi.incrementElse();
452 template <
class NaviType>
454 while(!navi.isConstant()) {
455 navi.incrementElse();
461 template <
class T>
class CIndexCacheHandle;
463 template <
class CacheType,
class DegCacheMgr,
class NaviType,
464 class TermType,
class SizeType,
class DescendingProperty>
468 NaviType navi, TermType init, SizeType degree,
469 DescendingProperty prop) {
475 return cache_mgr.zero();
477 if (navi.isConstant())
478 return cache_mgr.generate(navi);
484 NaviType cached = cache_mgr.find(navi, deg2node(degree, cache_mgr.manager()));
485 if (cached.isValid())
486 return cache_mgr.generate(cached);
490 NaviType then_branch = navi.thenBranch();
492 init, degree - 1, prop);
494 if ((navi.elseBranch().isEmpty()) && (init.navigation()==then_branch))
495 init = cache_mgr.generate(navi);
497 init = init.change(*navi);
505 NaviType resultNavi(init.navigation());
506 cache_mgr.insert(navi, deg2node(degree, cache_mgr.manager()), resultNavi);
513 template <
class CacheType,
class DegCacheMgr,
class NaviType,
514 class TermType,
class DescendingProperty>
517 NaviType navi, TermType init, DescendingProperty prop){
526 template <
class CacheType,
class DegCacheMgr,
class NaviType,
527 class TermType,
class SizeType,
class DescendingProperty>
530 const DegCacheMgr& deg_mgr,
531 NaviType navi, TermType& result,
533 DescendingProperty prop) {
539 if (navi.isConstant())
543 while (!navi.isConstant())
544 navi.incrementElse();
545 if (!navi.terminalValue())
552 NaviType cached = cache_mgr.find(navi, deg2node(degree, cache_mgr.manager()));
553 if (cached.isValid())
554 return result = result.multiplyFirst(cache_mgr.generate(cached));
558 result.push_back(*navi);
559 navi.incrementThen();
563 navi.incrementElse();
569 template <
class CacheType,
class DegCacheMgr,
class NaviType,
570 class TermType,
class DescendingProperty>
573 const DegCacheMgr& deg_mgr,
574 NaviType navi, TermType& result,
575 DescendingProperty prop) {
577 if (navi.isConstant())
590 template <
class CacheType,
class NaviType,
class TermType>
593 NaviType varsNavi, NaviType navi, TermType init){
595 typedef typename TermType::dd_type dd_type;
598 if (navi.isConstant())
599 return cache_mgr.generate(navi);
601 idx_type index(*navi);
602 while (!varsNavi.isConstant() && ((*varsNavi) < index))
603 varsNavi.incrementThen();
605 if (varsNavi.isConstant())
606 return cache_mgr.generate(navi);
609 NaviType cached = cache_mgr.find(varsNavi, navi);
610 if (cached.isValid())
611 return cache_mgr.generate(cached);
613 NaviType thenNavi(navi.thenBranch()), elseNavi(navi.elseBranch());
615 TermType thenResult =
618 TermType elseResult =
621 if ((*varsNavi) == index)
622 init = thenResult.unite(elseResult);
623 else if ( (thenResult.navigation() == thenNavi) &&
624 (elseResult.navigation() == elseNavi) )
625 init = cache_mgr.generate(navi);
627 init = dd_type(index, thenResult, elseResult);
630 cache_mgr.insert(varsNavi, navi, init.navigation());
637 template <
class CacheType,
class NaviType,
class PolyType>
640 NaviType navi, NaviType monomNavi, PolyType init){
644 typedef NaviType navigator;
645 typedef typename PolyType::dd_type dd_type;
647 if (monomNavi.isConstant()) {
649 return cache_mgr.generate(navi);
654 if (navi.isConstant())
655 return cache_mgr.zero();
657 if (monomNavi == navi)
658 return cache_mgr.one();
661 navigator cached = cache_mgr.find(navi, monomNavi);
663 if (cached.isValid()) {
664 return cache_mgr.generate(cached);
670 idx_type index = *navi;
671 idx_type monomIndex = *monomNavi;
673 if (monomIndex == index) {
676 navigator monomThen = monomNavi.thenBranch();
677 navigator naviThen = navi.thenBranch();
681 else if (monomIndex > index) {
692 cache_mgr.insert(navi, monomNavi, init.navigation());
699 template <
class DDGenerator,
class Iterator,
class NaviType,
class PolyType>
702 NaviType navi, Iterator start, Iterator finish,
707 typedef typename PolyType::dd_type dd_type;
708 typedef NaviType navigator;
711 return ddgen.generate(navi);
713 if (navi.isConstant())
720 idx_type index = *navi;
721 idx_type monomIndex = *start;
723 PolyType result(ddgen.zero());
724 if (monomIndex == index) {
728 navigator naviThen = navi.thenBranch();
732 else if (monomIndex > index) {
742 result = ddgen.zero();
749 template <
class CacheType,
class NaviType,
class MonomType>
753 if (navi.isConstant())
757 NaviType cached_result = cache.find(navi);
759 typedef typename MonomType::poly_type poly_type;
760 if (cached_result.isValid())
762 MonomType>().
getMonomial(cache.generate(cached_result));
767 result = result.change(*navi);
770 cache.insert(navi, result.diagram().navigation());
775 template <
class NaviType,
class Iterator>
777 dd_owns(NaviType navi, Iterator start, Iterator finish) {
779 if (start == finish) {
780 while(!navi.isConstant())
781 navi.incrementElse();
782 return navi.terminalValue();
785 while(!navi.isConstant() && (*start > *navi) )
786 navi.incrementElse();
788 if (navi.isConstant() || (*start != *navi))
791 return dd_owns(navi.thenBranch(), ++start, finish);
796 template <
class NaviType,
class MonomIterator>
799 MonomIterator start, MonomIterator finish) {
807 if (navi.isConstant()) {
808 if (navi.terminalValue())
809 return (++start == finish);
821 if (*navi > *start) {
822 if (++start == finish)
830 return dd_owns(navi.elseBranch(), start, finish) &&
837 template <
class CacheType,
class NaviType,
class DegType,
class SetType>
844 while(!navi.isConstant())
845 navi.incrementElse();
846 return cache.generate(navi);
849 if(navi.isConstant())
853 NaviType cached = cache.find(navi, deg);
855 if (cached.isValid())
856 return cache.generate(cached);
865 cache.insert(navi, deg, result.navigation());
874 template <
class CacheManager,
class NaviType,
class SetType>
877 NaviType rhsNavi, SetType init ) {
879 typedef typename SetType::dd_type dd_type;
880 while( (!navi.isConstant()) && (*rhsNavi != *navi) ) {
882 if ( (*rhsNavi < *navi) && (!rhsNavi.isConstant()) )
883 rhsNavi.incrementThen();
885 navi.incrementElse();
888 if (navi.isConstant())
889 return cache_mgr.generate(navi);
892 NaviType result = cache_mgr.find(navi, rhsNavi);
894 if (result.isValid())
895 return cache_mgr.generate(result);
900 init = dd_type(*rhsNavi,
906 cache_mgr.insert(navi, rhsNavi, init.navigation());
911 template <
class CacheType,
class NaviType,
class SetType>
914 NaviType navi, NaviType rhsNavi, SetType init){
916 typedef typename SetType::dd_type dd_type;
918 if(rhsNavi.isConstant()) {
920 return cache_mgr.generate(navi);
923 if (navi.isConstant() || (*navi > *rhsNavi))
924 return cache_mgr.zero();
926 if (*navi == *rhsNavi)
928 rhsNavi.thenBranch(), init).
change(*navi);
931 NaviType result = cache_mgr.find(navi, rhsNavi);
933 if (result.isValid())
934 return cache_mgr.generate(result);
937 init = dd_type(*navi,
939 rhsNavi, init).diagram(),
941 rhsNavi, init).diagram() );
944 cache_mgr.insert(navi, rhsNavi, init.navigation());
952 template <
class PolyType,
class RingType,
class MapType,
class NaviType>
956 if (navi.isConstant())
957 return ring.constant(navi.terminalValue());
961 return (idx2poly[*navi] *
962 substitute_variables__<PolyType>(ring, idx2poly, navi.thenBranch())) +
963 substitute_variables__<PolyType>(ring, idx2poly, navi.elseBranch());
968 template <
class RingType,
class MapType,
class PolyType>
971 const MapType& idx2poly,
const PolyType& poly) {
973 return substitute_variables__<PolyType>(ring, idx2poly, poly.navigation());