72 template <
class FirstIterator,
class SecondIterator,
class BinaryPredicate>
75 SecondIterator rhs_start, SecondIterator rhs_finish,
76 BinaryPredicate idx_comp) {
78 while ( (start != finish) && (rhs_start != rhs_finish) &&
79 (*start == *rhs_start) ) {
83 if (start == finish) {
84 if (rhs_start == rhs_finish)
85 return CTypes::equality;
87 return CTypes::less_than;
90 if (rhs_start == rhs_finish)
91 return CTypes::greater_than;
93 return (idx_comp(*start, *rhs_start)?
94 CTypes::greater_than: CTypes::less_than);
100 template <
class LhsType,
class RhsType,
class BinaryPredicate>
103 BinaryPredicate idx_comp,
valid_tag has_easy_equality_test) {
106 return CTypes::equality;
109 rhs.begin(), rhs.end(), idx_comp);
117 template <
class LhsType,
class RhsType,
class BinaryPredicate>
120 BinaryPredicate idx_comp,
invalid_tag has_no_easy_equality_test) {
123 rhs.begin(), rhs.end(), idx_comp);
128 template <
class LhsType,
class RhsType,
class BinaryPredicate>
130 lex_compare(
const LhsType& lhs,
const RhsType& rhs, BinaryPredicate idx_comp) {
135 return lex_compare(lhs, rhs, idx_comp, equality_property());
140 template<
class LhsType,
class RhsType,
class BinaryPredicate>
143 BinaryPredicate idx_comp) {
145 typedef typename LhsType::size_type size_type;
147 std::greater<size_type>() );
149 return (result == CTypes::equality?
lex_compare(lhs, rhs, idx_comp): result);
153 template <
class OrderType,
class Iterator>
154 class generic_iteration;
156 template<
class DummyType>
165 template <
class Iterator>
189 template <
class Iterator>
203 return std::max_element(
iterator(poly.navigation()),
211 iterator m_start(poly.navigation());
212 iterator m_finish(poly.endOfNavigation());
214 if (iter != m_finish) {
217 iter = std::find(iter, m_finish, deg);
219 if(iter == m_finish) {
220 iter = std::max_element( bounded_iterator(m_start, deg),
221 bounded_iterator(m_finish, deg) );
231 template <
class Iterator>
245 return std::max_element(
iterator(poly.navigation()),
247 std::less_equal<size_type>() );
255 iterator m_start(poly.navigation());
256 iterator m_finish(poly.endOfNavigation());
258 if (iter != m_finish) {
265 if(iter == m_finish) {
266 iter = std::max_element( bounded_iterator(m_start, deg),
267 bounded_iterator(m_finish, deg),
268 std::less_equal<size_type>() );
279 template <
class StackType,
class Iterator>
282 while (start != finish) {
288 template<
class NaviType,
class DescendingProperty = val
id_tag>
299 m_stack(), m_max_idx(0), m_upperbound(0), m_next() {}
305 m_stack(), m_upperbound(upperbound), m_max_idx(max_idx), m_next(navi) {
307 m_stack.reserve(upperbound);
311 while (!is_path_end() && !empty() )
316 return m_stack.size();
323 typename stack_type::const_iterator
begin()
const {
324 return m_stack.begin();
327 typename stack_type::const_iterator
end()
const {
328 return m_stack.end();
336 if (descendingVariables() && (m_stack.size() == m_upperbound) )
337 return *
this =
self();
341 }
while (!empty() && !is_path_end());
348 typename stack_type::const_iterator start(m_stack.begin()),
349 finish(m_stack.end());
352 while (start != finish) {
353 std::cout << *(*start) <<
", " ;
366 else (m_stack == rhs.m_stack);
369 return !(*
this == rhs);
374 while (within_degree() && !at_end())
382 m_next.incrementElse();
390 return m_stack.empty();
394 return m_stack.back();
400 return (!m_next.isConstant() && (*m_next >= m_max_idx)) ||
401 m_next.terminalValue();
406 m_next.incrementElse();
411 assert(!m_next.isConstant());
412 m_stack.push_back(m_next);
413 m_next.incrementThen();
420 return (*(*
this) < m_upperbound);
425 return m_next.isConstant() || (*m_next >= m_max_idx);
431 size_type m_upperbound;
439 template <
class DegreeCacher,
class NaviType,
class IdxType>
440 typename NaviType::size_type
444 typedef typename NaviType::size_type size_type;
446 if( navi.isConstant() || (*navi >= nextBlock) )
450 typename DegreeCacher::node_type result = cache.find(navi, nextBlock);
451 if (result.isValid())
461 cache.insert(navi, nextBlock, deg);
467 template<
class DegCacheMgr,
class NaviType,
class IdxType,
class SizeType>
470 SizeType degree,
valid_tag is_descending) {
471 navi.incrementThen();
475 template<
class DegCacheMgr,
class NaviType,
class IdxType,
class SizeType>
479 navi.incrementElse();
485 template <
class CacheType,
class DegCacheMgr,
class NaviType,
486 class TermType,
class Iterator,
class SizeType,
class DescendingProperty>
489 const DegCacheMgr& deg_mgr,
490 NaviType navi, Iterator block_iter,
491 TermType init, SizeType degree,
492 DescendingProperty prop) {
494 if (navi.isConstant())
495 return cache_mgr.generate(navi);
497 while( (*navi >= *block_iter) && (*block_iter != CUDD_MAXINDEX)) {
504 NaviType cached = cache_mgr.find(navi);
505 if (cached.isValid())
506 return cache_mgr.generate(cached);
512 init, degree - 1, prop).
change(*navi);
520 NaviType resultNavi(init.navigation());
521 cache_mgr.insert(navi, resultNavi);
522 deg_mgr.insert(resultNavi, *block_iter, degree);
528 template <
class CacheType,
class DegCacheMgr,
class NaviType,
class Iterator,
529 class TermType,
class DescendingProperty>
532 NaviType navi, Iterator block_iter, TermType init,
533 DescendingProperty prop){
535 if (navi.isConstant())
536 return cache_mgr.generate(navi);
544 template <
class FirstIterator,
class SecondIterator,
class IdxType,
545 class BinaryPredicate>
548 SecondIterator rhs_start, SecondIterator rhs_finish,
550 BinaryPredicate idx_comp) {
552 while ( (start != finish) && (*start < max_index) && (rhs_start != rhs_finish)
553 && (*rhs_start < max_index) && (*start == *rhs_start) ) {
554 ++start; ++rhs_start;
557 if ( (start == finish) || (*start >= max_index) ) {
558 if ( (rhs_start == rhs_finish) || (*rhs_start >= max_index) )
559 return CTypes::equality;
561 return CTypes::less_than;
564 if ( (rhs_start == rhs_finish) || (*rhs_start >= max_index) )
565 return CTypes::greater_than;
567 return (idx_comp(*start, *rhs_start)?
568 CTypes::greater_than: CTypes::less_than);
574 template<
class LhsIterator,
class RhsIterator,
class Iterator,
575 class BinaryPredicate>
578 RhsIterator rhsStart, RhsIterator rhsFinish,
579 Iterator start, Iterator finish,
580 BinaryPredicate idx_comp) {
587 while ( (start != finish) && (result == CTypes::equality) ) {
588 unsigned lhsdeg = 0, rhsdeg = 0;
589 LhsIterator oldLhs(lhsStart);
590 RhsIterator oldRhs(rhsStart);
593 while( (lhsStart != lhsFinish) && (*lhsStart < *start) ) {
594 ++lhsStart; ++lhsdeg;
596 while( (rhsStart != rhsFinish) && (*rhsStart < *start) ) {
597 ++rhsStart; ++rhsdeg;
600 std::greater<unsigned>() );
602 if (result == CTypes::equality) {
604 oldRhs, rhsFinish, *start, idx_comp);
615 template <
class IdxType,
class Iterator,
class BinaryPredicate>
618 Iterator start, Iterator finish,
619 BinaryPredicate idx_comp) {
622 return CTypes::equality;
624 Iterator lhsend = std::find_if(start, finish,
625 std::bind2nd(std::greater<IdxType>(), lhs));
628 Iterator rhsend = std::find_if(start, finish,
629 std::bind2nd(std::greater<IdxType>(), rhs));
631 assert((lhsend != finish) && (rhsend != finish));
634 std::less<IdxType>() );
636 return ( result == CTypes::equality?