PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00066 //***************************************************************************** 00067 00068 // include basic definitions 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 //typedef lex_compare_predicate<LhsType, RhsType, BinaryPredicate> comp_type; 00115 //return generic_compare_3way(lhs, rhs, comp_type(idx_comp)); 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 // if upperbound was already found we're done 00222 // (should be optimized away for ascending variables) 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) ) // end of block reached 00334 return 0; 00335 00336 // Look whether result was cached before 00337 typename DegreeCacher::node_type result = cache.find(navi, nextBlock); 00338 if (result.isValid()) 00339 return *result; 00340 00341 // Get degree of then branch (contains at least one valid path)... 00342 deg_type deg = dd_cached_block_degree(cache, navi.thenBranch(), nextBlock) + 1; 00343 00344 // ... combine with degree of else branch 00345 deg = std::max(deg, dd_cached_block_degree(cache, navi.elseBranch(), nextBlock) ); 00346 00347 // Write result to cache 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/*,degree - 1*/) + 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*/) != degree); 00368 } 00369 00370 00371 // with degree bound 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 // Check cache for previous results 00391 NaviType cached = cache_mgr.find(navi); 00392 if (cached.isValid()) 00393 return cache_mgr.generate(cached); 00394 00395 // Go to next branch 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 // unsigned lhsdeg = 0, rhsdeg = 0; 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); // maybe one can save this and do both 00477 RhsIterator oldRhs(rhsStart); // comparisons at once. 00478 00479 // maybe one can save 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