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