• Main Page
  • Related Pages
  • Namespaces
  • Classes
  • Files
  • File List
  • File Members

pbori_routines_order.h

Go to the documentation of this file.
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

Generated on Thu Oct 21 2010 06:56:31 for PolyBoRi by  doxygen 1.7.1