00001
00002
00066
00067
00068
00069 #include "pbori_defs.h"
00070 #include "pbori_algo.h"
00071 #include "pbori_traits.h"
00072
00073 #include "CRestrictedIter.h"
00074
00075 BEGIN_NAMESPACE_PBORI
00076
00077 template <class FirstIterator, class SecondIterator, class BinaryPredicate>
00078 CTypes::comp_type
00079 lex_compare_3way(FirstIterator start, FirstIterator finish,
00080 SecondIterator rhs_start, SecondIterator rhs_finish,
00081 BinaryPredicate idx_comp) {
00082
00083 while ( (start != finish) && (rhs_start != rhs_finish) &&
00084 (*start == *rhs_start) ) {
00085 ++start; ++rhs_start;
00086 }
00087
00088 if (start == finish) {
00089 if (rhs_start == rhs_finish)
00090 return CTypes::equality;
00091
00092 return CTypes::less_than;
00093 }
00094
00095 if (rhs_start == rhs_finish)
00096 return CTypes::greater_than;
00097
00098 return (idx_comp(*start, *rhs_start)?
00099 CTypes::greater_than: CTypes::less_than);
00100 }
00101
00102
00104 template <class LhsType, class RhsType, class BinaryPredicate>
00105 CTypes::comp_type
00106 lex_compare(const LhsType& lhs, const RhsType& rhs,
00107 BinaryPredicate idx_comp, valid_tag has_easy_equality_test) {
00108
00109 if (lhs == rhs)
00110 return CTypes::equality;
00111
00112 return lex_compare_3way(lhs.begin(), lhs.end(),
00113 rhs.begin(), rhs.end(), idx_comp);
00114
00115
00116 }
00117
00118
00120 template <class LhsType, class RhsType, class BinaryPredicate>
00121 CTypes::comp_type
00122 lex_compare(const LhsType& lhs, const RhsType& rhs,
00123 BinaryPredicate idx_comp, invalid_tag has_no_easy_equality_test) {
00124
00125 return lex_compare_3way(lhs.begin(), lhs.end(),
00126 rhs.begin(), rhs.end(), idx_comp);
00127 }
00128
00130 template <class LhsType, class RhsType, class BinaryPredicate>
00131 CTypes::comp_type
00132 lex_compare(const LhsType& lhs, const RhsType& rhs, BinaryPredicate idx_comp) {
00133
00134 typedef typename pbori_binary_traits<LhsType, RhsType>::easy_equality_property
00135 equality_property;
00136
00137 return lex_compare(lhs, rhs, idx_comp, equality_property());
00138 }
00139
00141 template<class LhsType, class RhsType, class BinaryPredicate>
00142 CTypes::comp_type
00143 deg_lex_compare(const LhsType& lhs, const RhsType& rhs,
00144 BinaryPredicate idx_comp) {
00145
00146 typedef typename LhsType::size_type size_type;
00147 CTypes::comp_type result = generic_compare_3way( lhs.size(), rhs.size(),
00148 std::greater<size_type>() );
00149
00150 return (result == CTypes::equality? lex_compare(lhs, rhs, idx_comp): result);
00151 }
00152
00153
00154 template <class OrderType, class Iterator>
00155 class generic_iteration;
00156
00157 template<class DummyType>
00158 class dummy_data_type {
00159 public:
00160 dummy_data_type(const DummyType&) {}
00161 dummy_data_type(DummyType&) {}
00162 dummy_data_type() {}
00163 };
00164
00166 template <class StackType, class Iterator>
00167 void dummy_append(StackType& stack, Iterator start, Iterator finish) {
00168
00169 while (start != finish) {
00170 stack.push(*start);
00171 ++start;
00172 }
00173 }
00174
00175 template<class NaviType, class DescendingProperty = valid_tag>
00176 class bounded_restricted_term {
00177 public:
00178 typedef NaviType navigator;
00179 typedef DescendingProperty descending_property;
00180 typedef bounded_restricted_term<navigator, descending_property> self;
00181 typedef std::vector<navigator> stack_type;
00182 typedef unsigned size_type;
00183 typedef unsigned idx_type;
00184
00185 bounded_restricted_term ():
00186 m_stack(), m_max_idx(0), m_upperbound(0), m_next() {}
00187
00188 is_same_type<descending_property, valid_tag> descendingVariables;
00189
00190 bounded_restricted_term (navigator navi, size_type upperbound,
00191 idx_type max_idx):
00192 m_stack(), m_upperbound(upperbound), m_max_idx(max_idx), m_next(navi) {
00193
00194 m_stack.reserve(upperbound);
00195
00196 followThen();
00197
00198 while (!is_path_end() && !empty() )
00199 increment();
00200 }
00201
00202 size_type operator*() const {
00203 return m_stack.size();
00204 }
00205
00206 const navigator& next() const {
00207 return m_next;
00208 }
00209
00210 typename stack_type::const_iterator begin() const {
00211 return m_stack.begin();
00212 }
00213
00214 typename stack_type::const_iterator end() const {
00215 return m_stack.end();
00216 }
00217
00218 self& operator++() {
00219 assert(!empty());
00220
00221
00222
00223 if (descendingVariables() && (m_stack.size() == m_upperbound) )
00224 return *this = self();
00225
00226 do {
00227 increment();
00228 } while (!empty() && !is_path_end());
00229
00230 return *this;
00231 }
00232
00233 void print() const {
00234
00235 typename stack_type::const_iterator start(m_stack.begin()),
00236 finish(m_stack.end());
00237
00238 std::cout <<'(';
00239 while (start != finish) {
00240 std::cout << *(*start) << ", " ;
00241 ++start;
00242 }
00243 std::cout <<')';
00244
00245 }
00246
00247 bool operator==(const self& rhs) const {
00248 if (rhs.empty())
00249 return empty();
00250 if (empty())
00251 return rhs.empty();
00252
00253 else (m_stack == rhs.m_stack);
00254 }
00255 bool operator!=(const self& rhs) const {
00256 return !(*this == rhs);
00257 }
00258 protected:
00259
00260 void followThen() {
00261 while (within_degree() && !at_end())
00262 nextThen();
00263 }
00264
00265 void increment() {
00266 assert(!empty());
00267
00268 m_next = top();
00269 m_next.incrementElse();
00270 m_stack.pop_back();
00271
00272 followThen();
00273
00274 }
00275
00276 bool empty() const{
00277 return m_stack.empty();
00278 }
00279
00280 navigator top() const{
00281 return m_stack.back();
00282 }
00283
00284 bool is_path_end() {
00285
00286 path_end();
00287 return (!m_next.isConstant() && (*m_next >= m_max_idx)) ||
00288 m_next.terminalValue();
00289 }
00290
00291 void path_end() {
00292 while (!at_end()) {
00293 m_next.incrementElse();
00294 }
00295 }
00296
00297 void nextThen() {
00298 assert(!m_next.isConstant());
00299 m_stack.push_back(m_next);
00300 m_next.incrementThen();
00301 }
00302
00303
00304
00305 bool within_degree() const {
00306
00307 return (*(*this) < m_upperbound);
00308 }
00309
00310 bool at_end() const {
00311
00312 return m_next.isConstant() || (*m_next >= m_max_idx);
00313 }
00314
00315 private:
00316 stack_type m_stack;
00317 idx_type m_max_idx;
00318 size_type m_upperbound;
00319 navigator m_next;
00320 };
00321
00322
00323
00326 template <class DegreeCacher, class NaviType, class IdxType>
00327 typename NaviType::deg_type
00328 dd_cached_block_degree(const DegreeCacher& cache, NaviType navi,
00329 IdxType nextBlock) {
00330
00331 typedef typename NaviType::deg_type deg_type;
00332
00333 if( navi.isConstant() || (*navi >= nextBlock) )
00334 return 0;
00335
00336
00337 typename DegreeCacher::node_type result = cache.find(navi, nextBlock);
00338 if (result.isValid())
00339 return *result;
00340
00341
00342 deg_type deg = dd_cached_block_degree(cache, navi.thenBranch(), nextBlock) + 1;
00343
00344
00345 deg = std::max(deg, dd_cached_block_degree(cache, navi.elseBranch(), nextBlock) );
00346
00347
00348 cache.insert(navi, nextBlock, deg);
00349
00350 return deg;
00351 }
00352
00353
00354 template<class DegCacheMgr, class NaviType, class IdxType, class SizeType>
00355 bool max_block_degree_on_then(const DegCacheMgr& deg_mgr, NaviType navi,
00356 IdxType next_block,
00357 SizeType degree, valid_tag is_descending) {
00358 navi.incrementThen();
00359 return ((dd_cached_block_degree(deg_mgr, navi, next_block) + 1) == degree);
00360 }
00361
00362 template<class DegCacheMgr, class NaviType, class IdxType, class SizeType>
00363 bool max_block_degree_on_then(const DegCacheMgr& deg_mgr, NaviType navi,
00364 IdxType next_block,
00365 SizeType degree, invalid_tag non_descending) {
00366 navi.incrementElse();
00367 return (dd_cached_block_degree(deg_mgr, navi, next_block) != degree);
00368 }
00369
00370
00371
00372 template <class CacheType, class DegCacheMgr, class NaviType,
00373 class TermType, class Iterator, class SizeType, class DescendingProperty>
00374 TermType
00375 dd_block_degree_lead(const CacheType& cache_mgr,
00376 const DegCacheMgr& deg_mgr,
00377 NaviType navi, Iterator block_iter,
00378 TermType init, SizeType degree,
00379 DescendingProperty prop) {
00380
00381 if (navi.isConstant())
00382 return cache_mgr.generate(navi);
00383
00384 while( (*navi >= *block_iter) && (*block_iter != CUDD_MAXINDEX)) {
00385 ++block_iter;
00386 degree = dd_cached_block_degree(deg_mgr, navi, *block_iter);
00387 }
00388
00389
00390
00391 NaviType cached = cache_mgr.find(navi);
00392 if (cached.isValid())
00393 return cache_mgr.generate(cached);
00394
00395
00396 if ( max_block_degree_on_then(deg_mgr, navi, *block_iter, degree, prop) ) {
00397 init = dd_block_degree_lead(cache_mgr, deg_mgr, navi.thenBranch(),
00398 block_iter,
00399 init, degree - 1, prop).change(*navi);
00400 }
00401 else {
00402 init = dd_block_degree_lead(cache_mgr, deg_mgr, navi.elseBranch(),
00403 block_iter,
00404 init, degree, prop);
00405 }
00406
00407 NaviType resultNavi(init.navigation());
00408 cache_mgr.insert(navi, resultNavi);
00409 deg_mgr.insert(resultNavi, *block_iter, degree);
00410
00411 return init;
00412 }
00413
00414
00415 template <class CacheType, class DegCacheMgr, class NaviType, class Iterator,
00416 class TermType, class DescendingProperty>
00417 TermType
00418 dd_block_degree_lead(const CacheType& cache_mgr, const DegCacheMgr& deg_mgr,
00419 NaviType navi, Iterator block_iter, TermType init,
00420 DescendingProperty prop){
00421
00422 if (navi.isConstant())
00423 return cache_mgr.generate(navi);
00424
00425 return dd_block_degree_lead(cache_mgr, deg_mgr, navi,block_iter, init,
00426 dd_cached_block_degree(deg_mgr, navi,
00427 *block_iter), prop);
00428 }
00429
00430
00431 template <class FirstIterator, class SecondIterator, class IdxType,
00432 class BinaryPredicate>
00433 CTypes::comp_type
00434 restricted_lex_compare_3way(FirstIterator start, FirstIterator finish,
00435 SecondIterator rhs_start, SecondIterator rhs_finish,
00436 IdxType max_index,
00437 BinaryPredicate idx_comp) {
00438
00439 while ( (start != finish) && (*start < max_index) && (rhs_start != rhs_finish)
00440 && (*rhs_start < max_index) && (*start == *rhs_start) ) {
00441 ++start; ++rhs_start;
00442 }
00443
00444 if ( (start == finish) || (*start >= max_index) ) {
00445 if ( (rhs_start == rhs_finish) || (*rhs_start >= max_index) )
00446 return CTypes::equality;
00447
00448 return CTypes::less_than;
00449 }
00450
00451 if ( (rhs_start == rhs_finish) || (*rhs_start >= max_index) )
00452 return CTypes::greater_than;
00453
00454 return (idx_comp(*start, *rhs_start)?
00455 CTypes::greater_than: CTypes::less_than);
00456 }
00457
00458
00459
00460
00461 template<class LhsIterator, class RhsIterator, class Iterator,
00462 class BinaryPredicate>
00463 CTypes::comp_type
00464 block_dlex_compare(LhsIterator lhsStart, LhsIterator lhsFinish,
00465 RhsIterator rhsStart, RhsIterator rhsFinish,
00466 Iterator start, Iterator finish,
00467 BinaryPredicate idx_comp) {
00468
00469
00470
00471
00472 CTypes::comp_type result = CTypes::equality;
00473
00474 while ( (start != finish) && (result == CTypes::equality) ) {
00475 CTypes::deg_type lhsdeg = 0, rhsdeg = 0;
00476 LhsIterator oldLhs(lhsStart);
00477 RhsIterator oldRhs(rhsStart);
00478
00479
00480 while( (lhsStart != lhsFinish) && (*lhsStart < *start) ) {
00481 ++lhsStart; ++lhsdeg;
00482 }
00483 while( (rhsStart != rhsFinish) && (*rhsStart < *start) ) {
00484 ++rhsStart; ++rhsdeg;
00485 }
00486 result = generic_compare_3way(lhsdeg, rhsdeg,
00487 std::greater<unsigned>() );
00488
00489 if (result == CTypes::equality) {
00490 result = restricted_lex_compare_3way(oldLhs, lhsFinish,
00491 oldRhs, rhsFinish, *start, idx_comp);
00492 }
00493
00494 ++start;
00495 }
00496
00497 return result;
00498 }
00499
00500
00502 template <class IdxType, class Iterator, class BinaryPredicate>
00503 CTypes::comp_type
00504 block_deg_lex_idx_compare(IdxType lhs, IdxType rhs,
00505 Iterator start, Iterator finish,
00506 BinaryPredicate idx_comp) {
00507
00508 if (lhs == rhs)
00509 return CTypes::equality;
00510
00511 Iterator lhsend = std::find_if(start, finish,
00512 std::bind2nd(std::greater<IdxType>(), lhs));
00513
00514
00515 Iterator rhsend = std::find_if(start, finish,
00516 std::bind2nd(std::greater<IdxType>(), rhs));
00517
00518 assert((lhsend != finish) && (rhsend != finish));
00519
00520 CTypes::comp_type result = generic_compare_3way( *lhsend, *rhsend,
00521 std::less<IdxType>() );
00522
00523 return ( result == CTypes::equality?
00524 generic_compare_3way(lhs, rhs, idx_comp): result );
00525 }
00526
00527 END_NAMESPACE_PBORI