PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00057 //***************************************************************************** 00058 00059 // include basic definitions 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 //typedef lex_compare_predicate<LhsType, RhsType, BinaryPredicate> comp_type; 00111 //return generic_compare_3way(lhs, rhs, comp_type(idx_comp)); 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 // LexOrder 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 // DegLexOrder 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 // DegRevLexAscOrder 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 // if upperbound was already found we're done 00335 // (should be optimized away for ascending variables) 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) ) // end of block reached 00447 return 0; 00448 00449 // Look whether result was cached before 00450 typename DegreeCacher::node_type result = cache.find(navi, nextBlock); 00451 if (result.isValid()) 00452 return *result; 00453 00454 // Get degree of then branch (contains at least one valid path)... 00455 size_type deg = dd_cached_block_degree(cache, navi.thenBranch(), nextBlock) + 1; 00456 00457 // ... combine with degree of else branch 00458 deg = std::max(deg, dd_cached_block_degree(cache, navi.elseBranch(), nextBlock) ); 00459 00460 // Write result to cache 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/*,degree - 1*/) + 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*/) != degree); 00481 } 00482 00483 00484 // with degree bound 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 // Check cache for previous results 00504 NaviType cached = cache_mgr.find(navi); 00505 if (cached.isValid()) 00506 return cache_mgr.generate(cached); 00507 00508 // Go to next branch 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 // unsigned lhsdeg = 0, rhsdeg = 0; 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); // maybe one can save this and do both 00590 RhsIterator oldRhs(rhsStart); // comparisons at once. 00591 00592 // maybe one can save 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