00001
00002
00057
00058
00059
00060 #include "pbori_defs.h"
00061 #include "pbori_order.h"
00062 #include "pbori_algo.h"
00063 #include "pbori_traits.h"
00064
00065 #include "CRestrictedIter.h"
00066
00067 BEGIN_NAMESPACE_PBORI
00068
00069
00070
00071
00072 template <class FirstIterator, class SecondIterator, class BinaryPredicate>
00073 CTypes::comp_type
00074 lex_compare_3way(FirstIterator start, FirstIterator finish,
00075 SecondIterator rhs_start, SecondIterator rhs_finish,
00076 BinaryPredicate idx_comp) {
00077
00078 while ( (start != finish) && (rhs_start != rhs_finish) &&
00079 (*start == *rhs_start) ) {
00080 ++start; ++rhs_start;
00081 }
00082
00083 if (start == finish) {
00084 if (rhs_start == rhs_finish)
00085 return CTypes::equality;
00086
00087 return CTypes::less_than;
00088 }
00089
00090 if (rhs_start == rhs_finish)
00091 return CTypes::greater_than;
00092
00093 return (idx_comp(*start, *rhs_start)?
00094 CTypes::greater_than: CTypes::less_than);
00095 }
00096
00097
00100 template <class LhsType, class RhsType, class BinaryPredicate>
00101 CTypes::comp_type
00102 lex_compare(const LhsType& lhs, const RhsType& rhs,
00103 BinaryPredicate idx_comp, valid_tag has_easy_equality_test) {
00104
00105 if (lhs == rhs)
00106 return CTypes::equality;
00107
00108 return lex_compare_3way(lhs.begin(), lhs.end(),
00109 rhs.begin(), rhs.end(), idx_comp);
00110
00111
00112 }
00113
00114
00117 template <class LhsType, class RhsType, class BinaryPredicate>
00118 CTypes::comp_type
00119 lex_compare(const LhsType& lhs, const RhsType& rhs,
00120 BinaryPredicate idx_comp, invalid_tag has_no_easy_equality_test) {
00121
00122 return lex_compare_3way(lhs.begin(), lhs.end(),
00123 rhs.begin(), rhs.end(), idx_comp);
00124 }
00125
00128 template <class LhsType, class RhsType, class BinaryPredicate>
00129 CTypes::comp_type
00130 lex_compare(const LhsType& lhs, const RhsType& rhs, BinaryPredicate idx_comp) {
00131
00132 typedef typename pbori_binary_traits<LhsType, RhsType>::easy_equality_property
00133 equality_property;
00134
00135 return lex_compare(lhs, rhs, idx_comp, equality_property());
00136 }
00137
00140 template<class LhsType, class RhsType, class BinaryPredicate>
00141 CTypes::comp_type
00142 deg_lex_compare(const LhsType& lhs, const RhsType& rhs,
00143 BinaryPredicate idx_comp) {
00144
00145 typedef typename LhsType::size_type size_type;
00146 CTypes::comp_type result = generic_compare_3way( lhs.size(), rhs.size(),
00147 std::greater<size_type>() );
00148
00149 return (result == CTypes::equality? lex_compare(lhs, rhs, idx_comp): result);
00150 }
00151
00152
00153 template <class OrderType, class Iterator>
00154 class generic_iteration;
00155
00156 template<class DummyType>
00157 class dummy_data_type {
00158 public:
00159 dummy_data_type(const DummyType&) {}
00160 dummy_data_type(DummyType&) {}
00161 dummy_data_type() {}
00162 };
00163
00164
00165 template <class Iterator>
00166 class generic_iteration<LexOrder, Iterator> {
00167 public:
00168
00170
00171 typedef LexOrder order_type;
00172 typedef Iterator iterator;
00173 typedef typename order_type::poly_type poly_type;
00174 typedef dummy_data_type<poly_type> data_type;
00176
00178 iterator leadIterator(const poly_type& poly) const {
00179 return iterator(poly.navigation());
00180 }
00181
00183 iterator incrementIterator(iterator& iter, const data_type&) const {
00184 return ++iter;
00185 }
00186 };
00187
00188
00189 template <class Iterator>
00190 class generic_iteration<DegLexOrder, Iterator> {
00191 public:
00193
00194 typedef DegLexOrder order_type;
00195 typedef Iterator iterator;
00196 typedef typename order_type::poly_type poly_type;
00197 typedef poly_type data_type;
00198 typedef typename order_type::size_type size_type;
00200
00202 iterator leadIterator(const poly_type& poly) const {
00203 return std::max_element(iterator(poly.navigation()),
00204 iterator(poly.endOfNavigation()) );
00205 }
00206
00208 iterator& incrementIterator(iterator& iter, const data_type& poly) const {
00209 typedef CRestrictedIter<iterator> bounded_iterator;
00210
00211 iterator m_start(poly.navigation());
00212 iterator m_finish(poly.endOfNavigation());
00213
00214 if (iter != m_finish) {
00215 size_type deg = *iter;
00216 ++iter;
00217 iter = std::find(iter, m_finish, deg);
00218
00219 if(iter == m_finish) {
00220 iter = std::max_element( bounded_iterator(m_start, deg),
00221 bounded_iterator(m_finish, deg) );
00222
00223 }
00224 }
00225 return iter;
00226 }
00227 };
00228
00229
00230
00231 template <class Iterator>
00232 class generic_iteration<DegRevLexAscOrder, Iterator> {
00233 public:
00235
00236 typedef DegRevLexAscOrder order_type;
00237 typedef Iterator iterator;
00238 typedef typename order_type::poly_type poly_type;
00239 typedef poly_type data_type;
00240 typedef typename order_type::size_type size_type;
00242
00244 iterator leadIterator(const poly_type& poly) const {
00245 return std::max_element(iterator(poly.navigation()),
00246 iterator(poly.endOfNavigation()),
00247 std::less_equal<size_type>() );
00248 }
00249
00251 iterator& incrementIterator(iterator& iter, const data_type& poly) const {
00252
00253 typedef CRestrictedIter<iterator> bounded_iterator;
00254
00255 iterator m_start(poly.navigation());
00256 iterator m_finish(poly.endOfNavigation());
00257
00258 if (iter != m_finish) {
00259
00260 size_type deg = *iter;
00261 --iter;
00262 iter = std::find(reversed_iteration_adaptor<iterator>(iter),
00263 reversed_iteration_adaptor<iterator>(m_finish), deg).get();
00264
00265 if(iter == m_finish) {
00266 iter = std::max_element( bounded_iterator(m_start, deg),
00267 bounded_iterator(m_finish, deg),
00268 std::less_equal<size_type>() );
00269
00270 }
00271 }
00272 return iter;
00273 }
00274 };
00275
00276
00279 template <class StackType, class Iterator>
00280 void dummy_append(StackType& stack, Iterator start, Iterator finish) {
00281
00282 while (start != finish) {
00283 stack.push(*start);
00284 ++start;
00285 }
00286 }
00287
00288 template<class NaviType, class DescendingProperty = valid_tag>
00289 class bounded_restricted_term {
00290 public:
00291 typedef NaviType navigator;
00292 typedef DescendingProperty descending_property;
00293 typedef bounded_restricted_term<navigator, descending_property> self;
00294 typedef std::vector<navigator> stack_type;
00295 typedef unsigned size_type;
00296 typedef unsigned idx_type;
00297
00298 bounded_restricted_term ():
00299 m_stack(), m_max_idx(0), m_upperbound(0), m_next() {}
00300
00301 is_same_type<descending_property, valid_tag> descendingVariables;
00302
00303 bounded_restricted_term (navigator navi, size_type upperbound,
00304 idx_type max_idx):
00305 m_stack(), m_upperbound(upperbound), m_max_idx(max_idx), m_next(navi) {
00306
00307 m_stack.reserve(upperbound);
00308
00309 followThen();
00310
00311 while (!is_path_end() && !empty() )
00312 increment();
00313 }
00314
00315 size_type operator*() const {
00316 return m_stack.size();
00317 }
00318
00319 const navigator& next() const {
00320 return m_next;
00321 }
00322
00323 typename stack_type::const_iterator begin() const {
00324 return m_stack.begin();
00325 }
00326
00327 typename stack_type::const_iterator end() const {
00328 return m_stack.end();
00329 }
00330
00331 self& operator++() {
00332 assert(!empty());
00333
00334
00335
00336 if (descendingVariables() && (m_stack.size() == m_upperbound) )
00337 return *this = self();
00338
00339 do {
00340 increment();
00341 } while (!empty() && !is_path_end());
00342
00343 return *this;
00344 }
00345
00346 void print() const {
00347
00348 typename stack_type::const_iterator start(m_stack.begin()),
00349 finish(m_stack.end());
00350
00351 std::cout <<'(';
00352 while (start != finish) {
00353 std::cout << *(*start) << ", " ;
00354 ++start;
00355 }
00356 std::cout <<')';
00357
00358 }
00359
00360 bool operator==(const self& rhs) const {
00361 if (rhs.empty())
00362 return empty();
00363 if (empty())
00364 return rhs.empty();
00365
00366 else (m_stack == rhs.m_stack);
00367 }
00368 bool operator!=(const self& rhs) const {
00369 return !(*this == rhs);
00370 }
00371 protected:
00372
00373 void followThen() {
00374 while (within_degree() && !at_end())
00375 nextThen();
00376 }
00377
00378 void increment() {
00379 assert(!empty());
00380
00381 m_next = top();
00382 m_next.incrementElse();
00383 m_stack.pop_back();
00384
00385 followThen();
00386
00387 }
00388
00389 bool empty() const{
00390 return m_stack.empty();
00391 }
00392
00393 navigator top() const{
00394 return m_stack.back();
00395 }
00396
00397 bool is_path_end() {
00398
00399 path_end();
00400 return (!m_next.isConstant() && (*m_next >= m_max_idx)) ||
00401 m_next.terminalValue();
00402 }
00403
00404 void path_end() {
00405 while (!at_end()) {
00406 m_next.incrementElse();
00407 }
00408 }
00409
00410 void nextThen() {
00411 assert(!m_next.isConstant());
00412 m_stack.push_back(m_next);
00413 m_next.incrementThen();
00414 }
00415
00416
00417
00418 bool within_degree() const {
00419
00420 return (*(*this) < m_upperbound);
00421 }
00422
00423 bool at_end() const {
00424
00425 return m_next.isConstant() || (*m_next >= m_max_idx);
00426 }
00427
00428 private:
00429 stack_type m_stack;
00430 idx_type m_max_idx;
00431 size_type m_upperbound;
00432 navigator m_next;
00433 };
00434
00435
00436
00439 template <class DegreeCacher, class NaviType, class IdxType>
00440 typename NaviType::size_type
00441 dd_cached_block_degree(const DegreeCacher& cache, NaviType navi,
00442 IdxType nextBlock) {
00443
00444 typedef typename NaviType::size_type size_type;
00445
00446 if( navi.isConstant() || (*navi >= nextBlock) )
00447 return 0;
00448
00449
00450 typename DegreeCacher::node_type result = cache.find(navi, nextBlock);
00451 if (result.isValid())
00452 return *result;
00453
00454
00455 size_type deg = dd_cached_block_degree(cache, navi.thenBranch(), nextBlock) + 1;
00456
00457
00458 deg = std::max(deg, dd_cached_block_degree(cache, navi.elseBranch(), nextBlock) );
00459
00460
00461 cache.insert(navi, nextBlock, deg);
00462
00463 return deg;
00464 }
00465
00466
00467 template<class DegCacheMgr, class NaviType, class IdxType, class SizeType>
00468 bool max_block_degree_on_then(const DegCacheMgr& deg_mgr, NaviType navi,
00469 IdxType next_block,
00470 SizeType degree, valid_tag is_descending) {
00471 navi.incrementThen();
00472 return ((dd_cached_block_degree(deg_mgr, navi, next_block) + 1) == degree);
00473 }
00474
00475 template<class DegCacheMgr, class NaviType, class IdxType, class SizeType>
00476 bool max_block_degree_on_then(const DegCacheMgr& deg_mgr, NaviType navi,
00477 IdxType next_block,
00478 SizeType degree, invalid_tag non_descending) {
00479 navi.incrementElse();
00480 return (dd_cached_block_degree(deg_mgr, navi, next_block) != degree);
00481 }
00482
00483
00484
00485 template <class CacheType, class DegCacheMgr, class NaviType,
00486 class TermType, class Iterator, class SizeType, class DescendingProperty>
00487 TermType
00488 dd_block_degree_lead(const CacheType& cache_mgr,
00489 const DegCacheMgr& deg_mgr,
00490 NaviType navi, Iterator block_iter,
00491 TermType init, SizeType degree,
00492 DescendingProperty prop) {
00493
00494 if (navi.isConstant())
00495 return cache_mgr.generate(navi);
00496
00497 while( (*navi >= *block_iter) && (*block_iter != CUDD_MAXINDEX)) {
00498 ++block_iter;
00499 degree = dd_cached_block_degree(deg_mgr, navi, *block_iter);
00500 }
00501
00502
00503
00504 NaviType cached = cache_mgr.find(navi);
00505 if (cached.isValid())
00506 return cache_mgr.generate(cached);
00507
00508
00509 if ( max_block_degree_on_then(deg_mgr, navi, *block_iter, degree, prop) ) {
00510 init = dd_block_degree_lead(cache_mgr, deg_mgr, navi.thenBranch(),
00511 block_iter,
00512 init, degree - 1, prop).change(*navi);
00513 }
00514 else {
00515 init = dd_block_degree_lead(cache_mgr, deg_mgr, navi.elseBranch(),
00516 block_iter,
00517 init, degree, prop);
00518 }
00519
00520 NaviType resultNavi(init.navigation());
00521 cache_mgr.insert(navi, resultNavi);
00522 deg_mgr.insert(resultNavi, *block_iter, degree);
00523
00524 return init;
00525 }
00526
00527
00528 template <class CacheType, class DegCacheMgr, class NaviType, class Iterator,
00529 class TermType, class DescendingProperty>
00530 TermType
00531 dd_block_degree_lead(const CacheType& cache_mgr, const DegCacheMgr& deg_mgr,
00532 NaviType navi, Iterator block_iter, TermType init,
00533 DescendingProperty prop){
00534
00535 if (navi.isConstant())
00536 return cache_mgr.generate(navi);
00537
00538 return dd_block_degree_lead(cache_mgr, deg_mgr, navi,block_iter, init,
00539 dd_cached_block_degree(deg_mgr, navi,
00540 *block_iter), prop);
00541 }
00542
00543
00544 template <class FirstIterator, class SecondIterator, class IdxType,
00545 class BinaryPredicate>
00546 CTypes::comp_type
00547 restricted_lex_compare_3way(FirstIterator start, FirstIterator finish,
00548 SecondIterator rhs_start, SecondIterator rhs_finish,
00549 IdxType max_index,
00550 BinaryPredicate idx_comp) {
00551
00552 while ( (start != finish) && (*start < max_index) && (rhs_start != rhs_finish)
00553 && (*rhs_start < max_index) && (*start == *rhs_start) ) {
00554 ++start; ++rhs_start;
00555 }
00556
00557 if ( (start == finish) || (*start >= max_index) ) {
00558 if ( (rhs_start == rhs_finish) || (*rhs_start >= max_index) )
00559 return CTypes::equality;
00560
00561 return CTypes::less_than;
00562 }
00563
00564 if ( (rhs_start == rhs_finish) || (*rhs_start >= max_index) )
00565 return CTypes::greater_than;
00566
00567 return (idx_comp(*start, *rhs_start)?
00568 CTypes::greater_than: CTypes::less_than);
00569 }
00570
00571
00572
00573
00574 template<class LhsIterator, class RhsIterator, class Iterator,
00575 class BinaryPredicate>
00576 CTypes::comp_type
00577 block_dlex_compare(LhsIterator lhsStart, LhsIterator lhsFinish,
00578 RhsIterator rhsStart, RhsIterator rhsFinish,
00579 Iterator start, Iterator finish,
00580 BinaryPredicate idx_comp) {
00581
00582
00583
00584
00585 CTypes::comp_type result = CTypes::equality;
00586
00587 while ( (start != finish) && (result == CTypes::equality) ) {
00588 unsigned lhsdeg = 0, rhsdeg = 0;
00589 LhsIterator oldLhs(lhsStart);
00590 RhsIterator oldRhs(rhsStart);
00591
00592
00593 while( (lhsStart != lhsFinish) && (*lhsStart < *start) ) {
00594 ++lhsStart; ++lhsdeg;
00595 }
00596 while( (rhsStart != rhsFinish) && (*rhsStart < *start) ) {
00597 ++rhsStart; ++rhsdeg;
00598 }
00599 result = generic_compare_3way(lhsdeg, rhsdeg,
00600 std::greater<unsigned>() );
00601
00602 if (result == CTypes::equality) {
00603 result = restricted_lex_compare_3way(oldLhs, lhsFinish,
00604 oldRhs, rhsFinish, *start, idx_comp);
00605 }
00606
00607 ++start;
00608 }
00609
00610 return result;
00611 }
00612
00613
00615 template <class IdxType, class Iterator, class BinaryPredicate>
00616 CTypes::comp_type
00617 block_deg_lex_idx_compare(IdxType lhs, IdxType rhs,
00618 Iterator start, Iterator finish,
00619 BinaryPredicate idx_comp) {
00620
00621 if (lhs == rhs)
00622 return CTypes::equality;
00623
00624 Iterator lhsend = std::find_if(start, finish,
00625 std::bind2nd(std::greater<IdxType>(), lhs));
00626
00627
00628 Iterator rhsend = std::find_if(start, finish,
00629 std::bind2nd(std::greater<IdxType>(), rhs));
00630
00631 assert((lhsend != finish) && (rhsend != finish));
00632
00633 CTypes::comp_type result = generic_compare_3way( *lhsend, *rhsend,
00634 std::less<IdxType>() );
00635
00636 return ( result == CTypes::equality?
00637 generic_compare_3way(lhs, rhs, idx_comp): result );
00638 }
00639
00640 END_NAMESPACE_PBORI