158 template<
class Iterator>
159 typename Iterator::value_type
162 typedef typename Iterator::value_type value_type;
167 while (start != finish){
169 sum += ((*start)+1) * ((*start)+1);
177 template <
class DegreeCacher,
class NaviType>
178 typename NaviType::size_type
181 typedef typename NaviType::size_type size_type;
183 if (navi.isConstant())
187 typename DegreeCacher::node_type result = cache.find(navi);
188 if (result.isValid())
198 cache.insert(navi, deg);
207 template <
class DegreeCacher,
class NaviType,
class SizeType>
208 typename NaviType::size_type
211 typedef typename NaviType::size_type size_type;
214 if (bound == 0 || navi.isConstant())
218 typename DegreeCacher::node_type result = cache.find(navi);
219 if (result.isValid())
230 cache.insert(navi, deg);
235 template <
class Iterator,
class NameGenerator,
236 class Separator,
class EmptySetType,
239 dd_print_term(Iterator start, Iterator finish,
const NameGenerator& get_name,
240 const Separator& sep,
const EmptySetType& emptyset,
243 if (start != finish){
244 os << get_name(*start);
250 while (start != finish){
251 os << sep() << get_name(*start);
256 template <
class TermType,
class NameGenerator,
257 class Separator,
class EmptySetType,
261 const Separator& sep,
const EmptySetType& emptyset,
263 dd_print_term(term.begin(), term.end(), get_name, sep, emptyset, os);
267 template <
class Iterator,
class NameGenerator,
268 class Separator,
class InnerSeparator,
269 class EmptySetType,
class OStreamType>
272 const Separator& sep,
const InnerSeparator& innersep,
273 const EmptySetType& emptyset, OStreamType& os) {
275 if (start != finish){
280 while (start != finish){
289 template <
class CacheType,
class NaviType,
class PolyType>
292 NaviType firstNavi, NaviType secondNavi, PolyType init){
294 typedef typename PolyType::dd_type dd_type;
296 typedef NaviType navigator;
298 if (firstNavi.isConstant()) {
299 if(firstNavi.terminalValue())
300 return cache_mgr.generate(secondNavi);
302 return cache_mgr.zero();
305 if (secondNavi.isConstant()) {
306 if(secondNavi.terminalValue())
307 return cache_mgr.generate(firstNavi);
309 return cache_mgr.zero();
311 if (firstNavi == secondNavi)
312 return cache_mgr.generate(firstNavi);
315 navigator cached = cache_mgr.find(firstNavi, secondNavi);
316 PolyType result = cache_mgr.zero();
318 if (cached.isValid()) {
319 return cache_mgr.generate(cached);
324 if (*secondNavi < *firstNavi)
325 std::swap(firstNavi, secondNavi);
327 idx_type index = *firstNavi;
330 navigator as0 = firstNavi.elseBranch();
331 navigator as1 = firstNavi.thenBranch();
336 if (*secondNavi == index) {
337 bs0 = secondNavi.elseBranch();
338 bs1 = secondNavi.thenBranch();
342 bs1 = result.navigation();
346 #ifdef PBORI_FAST_MULTIPLICATION
347 if (*firstNavi == *secondNavi) {
351 PolyType res10 = PolyType(cache_mgr.generate(as1)) +
352 PolyType(cache_mgr.generate(as0));
353 PolyType res01 = PolyType(cache_mgr.generate(bs0)) +
354 PolyType(cache_mgr.generate(bs1));
358 res10.navigation(), res01.navigation(),
361 result = dd_type(index, res11.diagram(), res00.diagram());
367 bs1 = result.navigation();
368 else if (bs0 == bs1){
369 as1 = result.navigation();
373 NaviType zero_ptr = result.navigation();
376 result = dd_type(index,
382 PolyType bs01 = PolyType(cache_mgr.generate(bs0)) +
383 PolyType(cache_mgr.generate(bs1));
384 result = dd_type(index,
398 cache_mgr.insert(firstNavi, secondNavi, result.navigation());
405 template <
class CacheType,
class NaviType,
class PolyType,
409 NaviType monomNavi, NaviType navi, PolyType init,
410 MonomTag monom_tag ){
413 typedef typename PolyType::dd_type dd_type;
415 typedef NaviType navigator;
417 if (monomNavi.isConstant()) {
418 if(monomNavi.terminalValue())
419 return cache_mgr.generate(navi);
421 return cache_mgr.zero();
424 assert(monomNavi.elseBranch().isEmpty());
426 if (navi.isConstant()) {
427 if(navi.terminalValue())
428 return cache_mgr.generate(monomNavi);
430 return cache_mgr.zero();
432 if (monomNavi == navi)
433 return cache_mgr.generate(monomNavi);
436 navigator cached = cache_mgr.find(monomNavi, navi);
438 if (cached.isValid()) {
439 return cache_mgr.generate(cached);
445 idx_type index = *navi;
446 idx_type monomIndex = *monomNavi;
448 if (monomIndex < index) {
450 init, monom_tag).diagram().change(monomIndex);
452 else if (monomIndex == index) {
455 navigator monomThen = monomNavi.thenBranch();
456 navigator naviThen = navi.thenBranch();
457 navigator naviElse = navi.elseBranch();
459 if (naviThen != naviElse)
463 monom_tag)).diagram().change(index);
470 init, monom_tag).diagram(),
472 init, monom_tag).diagram() );
476 cache_mgr.insert(monomNavi, navi, init.navigation());
482 template <
class DDGenerator,
class Iterator,
class NaviType,
class PolyType>
485 Iterator start, Iterator finish,
486 NaviType navi, PolyType init){
489 typedef typename PolyType::dd_type dd_type;
490 typedef NaviType navigator;
493 return ddgen.generate(navi);
496 if (navi.isConstant()) {
497 if(navi.terminalValue()) {
499 std::reverse_iterator<Iterator> rstart(finish), rfinish(start);
500 result = ddgen.generate(navi);
501 while (rstart != rfinish) {
502 result = result.diagram().change(*rstart);
515 idx_type index = *navi;
516 idx_type monomIndex = *start;
518 if (monomIndex < index) {
520 Iterator next(start);
521 while( (next != finish) && (*next < index) )
526 std::reverse_iterator<Iterator> rstart(next), rfinish(start);
527 while (rstart != rfinish) {
528 result = result.diagram().change(*rstart);
532 else if (monomIndex == index) {
537 navigator naviThen = navi.thenBranch();
538 navigator naviElse = navi.elseBranch();
540 if (naviThen != naviElse)
543 init)).diagram().change(index);
550 navi.thenBranch(), init).diagram(),
552 navi.elseBranch(), init).diagram() );
558 template<
class DegCacheMgr,
class NaviType,
class SizeType>
560 SizeType degree,
valid_tag is_descending) {
561 navi.incrementThen();
565 template<
class DegCacheMgr,
class NaviType,
class SizeType>
568 navi.incrementElse();
574 template <
class CacheType,
class DegCacheMgr,
class NaviType,
575 class TermType,
class SizeType,
class DescendingProperty>
579 NaviType navi, TermType init, SizeType degree,
580 DescendingProperty prop) {
582 if ((degree == 0) || navi.isConstant())
583 return cache_mgr.generate(navi);
586 NaviType cached = cache_mgr.find(navi);
587 if (cached.isValid())
588 return cache_mgr.generate(cached);
592 NaviType then_branch = navi.thenBranch();
594 init, degree - 1, prop);
595 if ((navi.elseBranch().isEmpty()) && (init.navigation()==then_branch))
596 init = cache_mgr.generate(navi);
598 init = init.change(*navi);
606 NaviType resultNavi(init.navigation());
607 cache_mgr.insert(navi, resultNavi);
608 deg_mgr.insert(resultNavi, degree);
613 template <
class CacheType,
class DegCacheMgr,
class NaviType,
614 class TermType,
class DescendingProperty>
617 NaviType navi, TermType init, DescendingProperty prop){
619 if (navi.isConstant())
620 return cache_mgr.generate(navi);
626 template <
class CacheType,
class DegCacheMgr,
class NaviType,
627 class TermType,
class SizeType,
class DescendingProperty>
630 const DegCacheMgr& deg_mgr,
631 NaviType navi, TermType& result,
633 DescendingProperty prop) {
635 if ((degree == 0) || navi.isConstant())
639 NaviType cached = cache_mgr.find(navi);
640 if (cached.isValid())
641 return result = result.multiplyFirst(cache_mgr.generate(cached));
645 result.push_back(*navi);
646 navi.incrementThen();
650 navi.incrementElse();
656 template <
class CacheType,
class DegCacheMgr,
class NaviType,
657 class TermType,
class DescendingProperty>
660 const DegCacheMgr& deg_mgr,
661 NaviType navi, TermType& result,
662 DescendingProperty prop) {
664 if (navi.isConstant())
677 template <
class CacheType,
class NaviType,
class TermType>
680 NaviType varsNavi, NaviType navi, TermType init){
682 typedef typename TermType::dd_type dd_type;
685 if (navi.isConstant())
686 return cache_mgr.generate(navi);
688 idx_type index(*navi);
689 while (!varsNavi.isConstant() && ((*varsNavi) < index))
690 varsNavi.incrementThen();
692 if (varsNavi.isConstant())
693 return cache_mgr.generate(navi);
696 NaviType cached = cache_mgr.find(varsNavi, navi);
697 if (cached.isValid())
698 return cache_mgr.generate(cached);
700 NaviType thenNavi(navi.thenBranch()), elseNavi(navi.elseBranch());
702 TermType thenResult =
705 TermType elseResult =
708 if ((*varsNavi) == index)
709 init = thenResult.unite(elseResult);
710 else if ( (thenResult.navigation() == thenNavi) &&
711 (elseResult.navigation() == elseNavi) )
712 init = cache_mgr.generate(navi);
714 init = dd_type(index, thenResult, elseResult);
717 cache_mgr.insert(varsNavi, navi, init.navigation());
724 template <
class CacheType,
class NaviType,
class PolyType>
727 NaviType navi, NaviType monomNavi, PolyType init){
731 typedef NaviType navigator;
732 typedef typename PolyType::dd_type dd_type;
734 if (monomNavi.isConstant()) {
735 if(monomNavi.terminalValue())
736 return cache_mgr.generate(navi);
738 return cache_mgr.zero();
741 assert(monomNavi.elseBranch().isEmpty());
743 if (navi.isConstant())
744 return cache_mgr.zero();
746 if (monomNavi == navi)
747 return cache_mgr.one();
750 navigator cached = cache_mgr.find(navi, monomNavi);
752 if (cached.isValid()) {
753 return cache_mgr.generate(cached);
759 idx_type index = *navi;
760 idx_type monomIndex = *monomNavi;
762 if (monomIndex == index) {
765 navigator monomThen = monomNavi.thenBranch();
766 navigator naviThen = navi.thenBranch();
770 else if (monomIndex > index) {
781 cache_mgr.insert(navi, monomNavi, init.navigation());
788 template <
class DDGenerator,
class Iterator,
class NaviType,
class PolyType>
791 NaviType navi, Iterator start, Iterator finish,
796 typedef typename PolyType::dd_type dd_type;
797 typedef NaviType navigator;
800 return ddgen.generate(navi);
802 if (navi.isConstant())
809 idx_type index = *navi;
810 idx_type monomIndex = *start;
813 if (monomIndex == index) {
817 navigator naviThen = navi.thenBranch();
821 else if (monomIndex > index) {
831 result = ddgen.zero();
838 template <
class CacheType,
class NaviType,
class MonomType>
842 if (navi.isConstant())
846 NaviType cached_result = cache.find(navi);
848 typedef typename MonomType::poly_type poly_type;
849 if (cached_result.isValid())
851 MonomType>().
getMonomial(cache.generate(cached_result));
856 result.changeAssign(*navi);
859 cache.insert(navi, result.diagram().navigation());
864 template <
class NaviType,
class Iterator>
866 dd_owns(NaviType navi, Iterator start, Iterator finish) {
868 if (start == finish) {
869 while(!navi.isConstant())
870 navi.incrementElse();
871 return navi.terminalValue();
874 while(!navi.isConstant() && (*start > *navi) )
875 navi.incrementElse();
877 if (navi.isConstant() || (*start != *navi))
880 return dd_owns(navi.thenBranch(), ++start, finish);
884 template <
class CacheType,
class NaviType,
class DegType,
class SetType>
891 while(!navi.isConstant())
892 navi.incrementElse();
893 return cache.generate(navi);
896 if(navi.isConstant())
900 NaviType cached = cache.find(navi, deg);
902 if (cached.isValid())
903 return cache.generate(cached);
912 cache.insert(navi, deg, result.navigation());
922 template <
class CacheManager,
class NaviType,
class SetType>
925 NaviType rhsNavi, SetType init ) {
927 typedef typename SetType::dd_type dd_type;
928 while( (!navi.isConstant()) && (*rhsNavi != *navi) ) {
930 if ( (*rhsNavi < *navi) && (!rhsNavi.isConstant()) )
931 rhsNavi.incrementThen();
933 navi.incrementElse();
936 if (navi.isConstant())
937 return cache_mgr.generate(navi);
940 NaviType result = cache_mgr.find(navi, rhsNavi);
942 if (result.isValid())
943 return cache_mgr.generate(result);
945 assert(*rhsNavi == *navi);
948 init = dd_type(*rhsNavi,
954 cache_mgr.insert(navi, rhsNavi, init.navigation());
959 template <
class CacheType,
class NaviType,
class SetType>
962 NaviType navi, NaviType rhsNavi, SetType init){
964 typedef typename SetType::dd_type dd_type;
966 if(rhsNavi.isConstant())
967 if(rhsNavi.terminalValue())
968 return cache_mgr.generate(navi);
970 return cache_mgr.generate(rhsNavi);
972 if (navi.isConstant() || (*navi > *rhsNavi))
973 return cache_mgr.zero();
975 if (*navi == *rhsNavi)
977 rhsNavi.thenBranch(), init).
change(*navi);
980 NaviType result = cache_mgr.find(navi, rhsNavi);
982 if (result.isValid())
983 return cache_mgr.generate(result);
986 init = dd_type(*navi,
988 rhsNavi, init).diagram(),
990 rhsNavi, init).diagram() );
993 cache_mgr.insert(navi, rhsNavi, init.navigation());