PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00014 //***************************************************************************** 00015 00016 // include basic definitions 00017 #include "pbori_defs.h" 00018 #include "pbori_algo.h" 00019 #include "pbori_traits.h" 00020 00021 #include "CRestrictedIter.h" 00022 00023 BEGIN_NAMESPACE_PBORI 00024 00025 template <class FirstIterator, class SecondIterator, class BinaryPredicate> 00026 CTypes::comp_type 00027 lex_compare_3way(FirstIterator start, FirstIterator finish, 00028 SecondIterator rhs_start, SecondIterator rhs_finish, 00029 BinaryPredicate idx_comp) { 00030 00031 while ( (start != finish) && (rhs_start != rhs_finish) && 00032 (*start == *rhs_start) ) { 00033 ++start; ++rhs_start; 00034 } 00035 00036 if (start == finish) { 00037 if (rhs_start == rhs_finish) 00038 return CTypes::equality; 00039 00040 return CTypes::less_than; 00041 } 00042 00043 if (rhs_start == rhs_finish) 00044 return CTypes::greater_than; 00045 00046 return (idx_comp(*start, *rhs_start)? 00047 CTypes::greater_than: CTypes::less_than); 00048 } 00049 00050 00052 template <class LhsType, class RhsType, class BinaryPredicate> 00053 CTypes::comp_type 00054 lex_compare(const LhsType& lhs, const RhsType& rhs, 00055 BinaryPredicate idx_comp, valid_tag has_easy_equality_test) { 00056 00057 if (lhs == rhs) 00058 return CTypes::equality; 00059 00060 return lex_compare_3way(lhs.begin(), lhs.end(), 00061 rhs.begin(), rhs.end(), idx_comp); 00062 //typedef lex_compare_predicate<LhsType, RhsType, BinaryPredicate> comp_type; 00063 //return generic_compare_3way(lhs, rhs, comp_type(idx_comp)); 00064 } 00065 00066 00068 template <class LhsType, class RhsType, class BinaryPredicate> 00069 CTypes::comp_type 00070 lex_compare(const LhsType& lhs, const RhsType& rhs, 00071 BinaryPredicate idx_comp, invalid_tag has_no_easy_equality_test) { 00072 00073 return lex_compare_3way(lhs.begin(), lhs.end(), 00074 rhs.begin(), rhs.end(), idx_comp); 00075 } 00076 00078 template <class LhsType, class RhsType, class BinaryPredicate> 00079 CTypes::comp_type 00080 lex_compare(const LhsType& lhs, const RhsType& rhs, BinaryPredicate idx_comp) { 00081 00082 typedef typename pbori_binary_traits<LhsType, RhsType>::easy_equality_property 00083 equality_property; 00084 00085 return lex_compare(lhs, rhs, idx_comp, equality_property()); 00086 } 00087 00089 template<class LhsType, class RhsType, class BinaryPredicate> 00090 CTypes::comp_type 00091 deg_lex_compare(const LhsType& lhs, const RhsType& rhs, 00092 BinaryPredicate idx_comp) { 00093 00094 typedef typename LhsType::size_type size_type; 00095 CTypes::comp_type result = generic_compare_3way( lhs.size(), rhs.size(), 00096 std::greater<size_type>() ); 00097 00098 return (result == CTypes::equality? lex_compare(lhs, rhs, idx_comp): result); 00099 } 00100 00101 00102 template <class OrderType, class Iterator> 00103 class generic_iteration; 00104 00105 template<class DummyType> 00106 class dummy_data_type { 00107 public: 00108 dummy_data_type(const DummyType&) {} 00109 dummy_data_type(DummyType&) {} 00110 dummy_data_type() {} 00111 }; 00112 00114 template <class StackType, class Iterator> 00115 void dummy_append(StackType& stack, Iterator start, Iterator finish) { 00116 00117 while (start != finish) { 00118 stack.push(*start); 00119 ++start; 00120 } 00121 } 00122 00123 template<class NaviType, class DescendingProperty = valid_tag> 00124 class bounded_restricted_term { 00125 public: 00126 typedef NaviType navigator; 00127 typedef DescendingProperty descending_property; 00128 typedef bounded_restricted_term<navigator, descending_property> self; 00129 typedef std::vector<navigator> stack_type; 00130 typedef unsigned size_type; 00131 typedef unsigned idx_type; 00132 00133 bounded_restricted_term (): 00134 m_stack(), m_max_idx(0), m_upperbound(0), m_next() {} 00135 00136 is_same_type<descending_property, valid_tag> descendingVariables; 00137 00138 bounded_restricted_term (navigator navi, size_type upperbound, 00139 idx_type max_idx): 00140 m_stack(), m_upperbound(upperbound), m_max_idx(max_idx), m_next(navi) { 00141 00142 m_stack.reserve(upperbound); 00143 00144 followThen(); 00145 00146 while (!is_path_end() && !empty() ) 00147 increment(); 00148 } 00149 00150 size_type operator*() const { 00151 return m_stack.size(); 00152 } 00153 00154 const navigator& next() const { 00155 return m_next; 00156 } 00157 00158 typename stack_type::const_iterator begin() const { 00159 return m_stack.begin(); 00160 } 00161 00162 typename stack_type::const_iterator end() const { 00163 return m_stack.end(); 00164 } 00165 00166 self& operator++() { 00167 assert(!empty()); 00168 00169 // if upperbound was already found we're done 00170 // (should be optimized away for ascending variables) 00171 if (descendingVariables() && (m_stack.size() == m_upperbound) ) 00172 return *this = self(); 00173 00174 do { 00175 increment(); 00176 } while (!empty() && !is_path_end()); 00177 00178 return *this; 00179 } 00180 00181 void print() const { 00182 00183 typename stack_type::const_iterator start(m_stack.begin()), 00184 finish(m_stack.end()); 00185 00186 std::cout <<'('; 00187 while (start != finish) { 00188 std::cout << *(*start) << ", " ; 00189 ++start; 00190 } 00191 std::cout <<')'; 00192 00193 } 00194 00195 bool operator==(const self& rhs) const { 00196 if (rhs.empty()) 00197 return empty(); 00198 if (empty()) 00199 return rhs.empty(); 00200 00201 else (m_stack == rhs.m_stack); 00202 } 00203 bool operator!=(const self& rhs) const { 00204 return !(*this == rhs); 00205 } 00206 protected: 00207 00208 void followThen() { 00209 while (within_degree() && !at_end()) 00210 nextThen(); 00211 } 00212 00213 void increment() { 00214 assert(!empty()); 00215 00216 m_next = top(); 00217 m_next.incrementElse(); 00218 m_stack.pop_back(); 00219 00220 followThen(); 00221 00222 } 00223 00224 bool empty() const{ 00225 return m_stack.empty(); 00226 } 00227 00228 navigator top() const{ 00229 return m_stack.back(); 00230 } 00231 00232 bool is_path_end() { 00233 00234 path_end(); 00235 return (!m_next.isConstant() && (*m_next >= m_max_idx)) || 00236 m_next.terminalValue(); 00237 } 00238 00239 void path_end() { 00240 while (!at_end()) { 00241 m_next.incrementElse(); 00242 } 00243 } 00244 00245 void nextThen() { 00246 assert(!m_next.isConstant()); 00247 m_stack.push_back(m_next); 00248 m_next.incrementThen(); 00249 } 00250 00251 00252 00253 bool within_degree() const { 00254 00255 return (*(*this) < m_upperbound); 00256 } 00257 00258 bool at_end() const { 00259 00260 return m_next.isConstant() || (*m_next >= m_max_idx); 00261 } 00262 00263 private: 00264 stack_type m_stack; 00265 idx_type m_max_idx; 00266 size_type m_upperbound; 00267 navigator m_next; 00268 }; 00269 00270 00271 00274 template <class DegreeCacher, class NaviType, class IdxType> 00275 typename NaviType::deg_type 00276 dd_cached_block_degree(const DegreeCacher& cache, NaviType navi, 00277 IdxType nextBlock) { 00278 00279 typedef typename NaviType::deg_type deg_type; 00280 00281 if( navi.isConstant() || (*navi >= nextBlock) ) // end of block reached 00282 return 0; 00283 00284 // Look whether result was cached before 00285 typename DegreeCacher::node_type result = cache.find(navi, nextBlock); 00286 if (result.isValid()) 00287 return *result; 00288 00289 // Get degree of then branch (contains at least one valid path)... 00290 deg_type deg = dd_cached_block_degree(cache, navi.thenBranch(), nextBlock) + 1; 00291 00292 // ... combine with degree of else branch 00293 deg = std::max(deg, dd_cached_block_degree(cache, navi.elseBranch(), nextBlock) ); 00294 00295 // Write result to cache 00296 cache.insert(navi, nextBlock, deg); 00297 00298 return deg; 00299 } 00300 00301 00302 template<class DegCacheMgr, class NaviType, class IdxType, class SizeType> 00303 bool max_block_degree_on_then(const DegCacheMgr& deg_mgr, NaviType navi, 00304 IdxType next_block, 00305 SizeType degree, valid_tag is_descending) { 00306 navi.incrementThen(); 00307 return ((dd_cached_block_degree(deg_mgr, navi, next_block/*,degree - 1*/) + 1) == degree); 00308 } 00309 00310 template<class DegCacheMgr, class NaviType, class IdxType, class SizeType> 00311 bool max_block_degree_on_then(const DegCacheMgr& deg_mgr, NaviType navi, 00312 IdxType next_block, 00313 SizeType degree, invalid_tag non_descending) { 00314 navi.incrementElse(); 00315 return (dd_cached_block_degree(deg_mgr, navi, next_block/*, degree*/) != degree); 00316 } 00317 00318 00319 // with degree bound 00320 template <class CacheType, class DegCacheMgr, class NaviType, 00321 class TermType, class Iterator, class SizeType, class DescendingProperty> 00322 TermType 00323 dd_block_degree_lead(const CacheType& cache_mgr, 00324 const DegCacheMgr& deg_mgr, 00325 NaviType navi, Iterator block_iter, 00326 TermType init, SizeType degree, 00327 DescendingProperty prop) { 00328 00329 if (navi.isConstant()) 00330 return cache_mgr.generate(navi); 00331 00332 while( (*navi >= *block_iter) && (*block_iter != CUDD_MAXINDEX)) { 00333 ++block_iter; 00334 degree = dd_cached_block_degree(deg_mgr, navi, *block_iter); 00335 } 00336 00337 00338 // Check cache for previous results - Wrong in general, bounds may have changed! 00339 // NaviType cached = cache_mgr.find(navi); 00340 // if (cached.isValid()) 00341 // return cache_mgr.generate(cached); 00342 00343 // Go to next branch 00344 if ( max_block_degree_on_then(deg_mgr, navi, *block_iter, degree, prop) ) { 00345 init = dd_block_degree_lead(cache_mgr, deg_mgr, navi.thenBranch(), 00346 block_iter, 00347 init, degree - 1, prop).change(*navi); 00348 } 00349 else { 00350 init = dd_block_degree_lead(cache_mgr, deg_mgr, navi.elseBranch(), 00351 block_iter, 00352 init, degree, prop); 00353 } 00354 00355 NaviType resultNavi(init.navigation()); 00356 // cache_mgr.insert(navi, resultNavi); 00357 deg_mgr.insert(resultNavi, *block_iter, degree); 00358 00359 return init; 00360 } 00361 00362 00363 template <class CacheType, class DegCacheMgr, class NaviType, class Iterator, 00364 class TermType, class DescendingProperty> 00365 TermType 00366 dd_block_degree_lead(const CacheType& cache_mgr, const DegCacheMgr& deg_mgr, 00367 NaviType navi, Iterator block_iter, TermType init, 00368 DescendingProperty prop){ 00369 00370 if (navi.isConstant()) 00371 return cache_mgr.generate(navi); 00372 00373 return dd_block_degree_lead(cache_mgr, deg_mgr, navi,block_iter, init, 00374 dd_cached_block_degree(deg_mgr, navi, 00375 *block_iter), prop); 00376 } 00377 00378 00379 template <class FirstIterator, class SecondIterator, class IdxType, 00380 class BinaryPredicate> 00381 CTypes::comp_type 00382 restricted_lex_compare_3way(FirstIterator start, FirstIterator finish, 00383 SecondIterator rhs_start, SecondIterator rhs_finish, 00384 IdxType max_index, 00385 BinaryPredicate idx_comp) { 00386 00387 while ( (start != finish) && (*start < max_index) && (rhs_start != rhs_finish) 00388 && (*rhs_start < max_index) && (*start == *rhs_start) ) { 00389 ++start; ++rhs_start; 00390 } 00391 00392 if ( (start == finish) || (*start >= max_index) ) { 00393 if ( (rhs_start == rhs_finish) || (*rhs_start >= max_index) ) 00394 return CTypes::equality; 00395 00396 return CTypes::less_than; 00397 } 00398 00399 if ( (rhs_start == rhs_finish) || (*rhs_start >= max_index) ) 00400 return CTypes::greater_than; 00401 00402 return (idx_comp(*start, *rhs_start)? 00403 CTypes::greater_than: CTypes::less_than); 00404 } 00405 00406 00407 00408 00409 template<class LhsIterator, class RhsIterator, class Iterator, 00410 class BinaryPredicate> 00411 CTypes::comp_type 00412 block_dlex_compare(LhsIterator lhsStart, LhsIterator lhsFinish, 00413 RhsIterator rhsStart, RhsIterator rhsFinish, 00414 Iterator start, Iterator finish, 00415 BinaryPredicate idx_comp) { 00416 00417 // unsigned lhsdeg = 0, rhsdeg = 0; 00418 00419 00420 CTypes::comp_type result = CTypes::equality; 00421 00422 while ( (start != finish) && (result == CTypes::equality) ) { 00423 CTypes::deg_type lhsdeg = 0, rhsdeg = 0; 00424 LhsIterator oldLhs(lhsStart); // maybe one can save this and do both 00425 RhsIterator oldRhs(rhsStart); // comparisons at once. 00426 00427 // maybe one can save 00428 while( (lhsStart != lhsFinish) && (*lhsStart < *start) ) { 00429 ++lhsStart; ++lhsdeg; 00430 } 00431 while( (rhsStart != rhsFinish) && (*rhsStart < *start) ) { 00432 ++rhsStart; ++rhsdeg; 00433 } 00434 result = generic_compare_3way(lhsdeg, rhsdeg, 00435 std::greater<unsigned>() ); 00436 00437 if (result == CTypes::equality) { 00438 result = restricted_lex_compare_3way(oldLhs, lhsFinish, 00439 oldRhs, rhsFinish, *start, idx_comp); 00440 } 00441 00442 ++start; 00443 } 00444 00445 return result; 00446 } 00447 00448 00450 template <class IdxType, class Iterator, class BinaryPredicate> 00451 CTypes::comp_type 00452 block_deg_lex_idx_compare(IdxType lhs, IdxType rhs, 00453 Iterator start, Iterator finish, 00454 BinaryPredicate idx_comp) { 00455 00456 if (lhs == rhs) 00457 return CTypes::equality; 00458 00459 Iterator lhsend = std::find_if(start, finish, 00460 std::bind2nd(std::greater<IdxType>(), lhs)); 00461 00462 00463 Iterator rhsend = std::find_if(start, finish, 00464 std::bind2nd(std::greater<IdxType>(), rhs)); 00465 00466 CTypes::comp_type result = CTypes::equality; 00467 00468 if UNLIKELY( (rhsend == finish) && (lhsend != finish) ) 00469 result = CTypes::less_than; 00470 else if UNLIKELY(lhsend == finish) 00471 result = CTypes::greater_than; 00472 else { 00473 assert((lhsend != finish) && (rhsend != finish)); 00474 result = generic_compare_3way( *lhsend, *rhsend, std::less<IdxType>() ); 00475 } 00476 00477 return ( result == CTypes::equality? 00478 generic_compare_3way(lhs, rhs, idx_comp): result ); 00479 } 00480 00481 END_NAMESPACE_PBORI