PolyBoRi
pbori_routines_order.h
Go to the documentation of this file.
1 // -*- c++ -*-
2 //*****************************************************************************
57 //*****************************************************************************
58 
59 // include basic definitions
60 #include "pbori_defs.h"
61 #include "pbori_order.h"
62 #include "pbori_algo.h"
63 #include "pbori_traits.h"
64 
65 #include "CRestrictedIter.h"
66 
68 
69 
70 
71 
72 template <class FirstIterator, class SecondIterator, class BinaryPredicate>
73 CTypes::comp_type
74 lex_compare_3way(FirstIterator start, FirstIterator finish,
75  SecondIterator rhs_start, SecondIterator rhs_finish,
76  BinaryPredicate idx_comp) {
77 
78  while ( (start != finish) && (rhs_start != rhs_finish) &&
79  (*start == *rhs_start) ) {
80  ++start; ++rhs_start;
81  }
82 
83  if (start == finish) {
84  if (rhs_start == rhs_finish)
85  return CTypes::equality;
86 
87  return CTypes::less_than;
88  }
89 
90  if (rhs_start == rhs_finish)
91  return CTypes::greater_than;
92 
93  return (idx_comp(*start, *rhs_start)?
94  CTypes::greater_than: CTypes::less_than);
95 }
96 
97 
100 template <class LhsType, class RhsType, class BinaryPredicate>
101 CTypes::comp_type
102 lex_compare(const LhsType& lhs, const RhsType& rhs,
103  BinaryPredicate idx_comp, valid_tag has_easy_equality_test) {
104 
105  if (lhs == rhs)
106  return CTypes::equality;
107 
108  return lex_compare_3way(lhs.begin(), lhs.end(),
109  rhs.begin(), rhs.end(), idx_comp);
110  //typedef lex_compare_predicate<LhsType, RhsType, BinaryPredicate> comp_type;
111  //return generic_compare_3way(lhs, rhs, comp_type(idx_comp));
112 }
113 
114 
117 template <class LhsType, class RhsType, class BinaryPredicate>
118 CTypes::comp_type
119 lex_compare(const LhsType& lhs, const RhsType& rhs,
120  BinaryPredicate idx_comp, invalid_tag has_no_easy_equality_test) {
121 
122  return lex_compare_3way(lhs.begin(), lhs.end(),
123  rhs.begin(), rhs.end(), idx_comp);
124 }
125 
128 template <class LhsType, class RhsType, class BinaryPredicate>
129 CTypes::comp_type
130 lex_compare(const LhsType& lhs, const RhsType& rhs, BinaryPredicate idx_comp) {
131 
134 
135  return lex_compare(lhs, rhs, idx_comp, equality_property());
136 }
137 
140 template<class LhsType, class RhsType, class BinaryPredicate>
141 CTypes::comp_type
142 deg_lex_compare(const LhsType& lhs, const RhsType& rhs,
143  BinaryPredicate idx_comp) {
144 
145  typedef typename LhsType::size_type size_type;
146  CTypes::comp_type result = generic_compare_3way( lhs.size(), rhs.size(),
147  std::greater<size_type>() );
148 
149  return (result == CTypes::equality? lex_compare(lhs, rhs, idx_comp): result);
150 }
151 
152 
153 template <class OrderType, class Iterator>
154 class generic_iteration;
155 
156 template<class DummyType>
158 public:
159  dummy_data_type(const DummyType&) {}
160  dummy_data_type(DummyType&) {}
162 };
163 
164 // LexOrder
165 template <class Iterator>
166 class generic_iteration<LexOrder, Iterator> {
167 public:
168 
170 
172  typedef Iterator iterator;
173  typedef typename order_type::poly_type poly_type;
176 
178  iterator leadIterator(const poly_type& poly) const {
179  return iterator(poly.navigation());
180  }
181 
184  return ++iter;
185  }
186 };
187 
188 // DegLexOrder
189 template <class Iterator>
190 class generic_iteration<DegLexOrder, Iterator> {
191 public:
193 
195  typedef Iterator iterator;
196  typedef typename order_type::poly_type poly_type;
198  typedef typename order_type::size_type size_type;
200 
202  iterator leadIterator(const poly_type& poly) const {
203  return std::max_element(iterator(poly.navigation()),
204  iterator(poly.endOfNavigation()) );
205  }
206 
208  iterator& incrementIterator(iterator& iter, const data_type& poly) const {
209  typedef CRestrictedIter<iterator> bounded_iterator;
210 
211  iterator m_start(poly.navigation());
212  iterator m_finish(poly.endOfNavigation());
213 
214  if (iter != m_finish) {
215  size_type deg = *iter;
216  ++iter;
217  iter = std::find(iter, m_finish, deg);
218 
219  if(iter == m_finish) {
220  iter = std::max_element( bounded_iterator(m_start, deg),
221  bounded_iterator(m_finish, deg) );
222 
223  }
224  }
225  return iter;
226  }
227 };
228 
229 
230 // DegRevLexAscOrder
231 template <class Iterator>
232 class generic_iteration<DegRevLexAscOrder, Iterator> {
233 public:
235 
237  typedef Iterator iterator;
238  typedef typename order_type::poly_type poly_type;
240  typedef typename order_type::size_type size_type;
242 
244  iterator leadIterator(const poly_type& poly) const {
245  return std::max_element(iterator(poly.navigation()),
246  iterator(poly.endOfNavigation()),
247  std::less_equal<size_type>() );
248  }
249 
251  iterator& incrementIterator(iterator& iter, const data_type& poly) const {
252 
253  typedef CRestrictedIter<iterator> bounded_iterator;
254 
255  iterator m_start(poly.navigation());
256  iterator m_finish(poly.endOfNavigation());
257 
258  if (iter != m_finish) {
259 
260  size_type deg = *iter;
261  --iter;
262  iter = std::find(reversed_iteration_adaptor<iterator>(iter),
263  reversed_iteration_adaptor<iterator>(m_finish), deg).get();
264 
265  if(iter == m_finish) {
266  iter = std::max_element( bounded_iterator(m_start, deg),
267  bounded_iterator(m_finish, deg),
268  std::less_equal<size_type>() );
269 
270  }
271  }
272  return iter;
273  }
274 };
275 
276 
279 template <class StackType, class Iterator>
280 void dummy_append(StackType& stack, Iterator start, Iterator finish) {
281 
282  while (start != finish) {
283  stack.push(*start);
284  ++start;
285  }
286 }
287 
288 template<class NaviType, class DescendingProperty = valid_tag>
290 public:
291  typedef NaviType navigator;
292  typedef DescendingProperty descending_property;
294  typedef std::vector<navigator> stack_type;
295  typedef unsigned size_type;
296  typedef unsigned idx_type;
297 
299  m_stack(), m_max_idx(0), m_upperbound(0), m_next() {}
300 
302 
304  idx_type max_idx):
305  m_stack(), m_upperbound(upperbound), m_max_idx(max_idx), m_next(navi) {
306 
307  m_stack.reserve(upperbound);
308 
309  followThen();
310 
311  while (!is_path_end() && !empty() )
312  increment();
313  }
314 
316  return m_stack.size();
317  }
318 
319  const navigator& next() const {
320  return m_next;
321  }
322 
323  typename stack_type::const_iterator begin() const {
324  return m_stack.begin();
325  }
326 
327  typename stack_type::const_iterator end() const {
328  return m_stack.end();
329  }
330 
331  self& operator++() {
332  assert(!empty());
333 
334  // if upperbound was already found we're done
335  // (should be optimized away for ascending variables)
336  if (descendingVariables() && (m_stack.size() == m_upperbound) )
337  return *this = self();
338 
339  do {
340  increment();
341  } while (!empty() && !is_path_end());
342 
343  return *this;
344  }
345 
346  void print() const {
347 
348  typename stack_type::const_iterator start(m_stack.begin()),
349  finish(m_stack.end());
350 
351  std::cout <<'(';
352  while (start != finish) {
353  std::cout << *(*start) << ", " ;
354  ++start;
355  }
356  std::cout <<')';
357 
358  }
359 
360  bool operator==(const self& rhs) const {
361  if (rhs.empty())
362  return empty();
363  if (empty())
364  return rhs.empty();
365 
366  else (m_stack == rhs.m_stack);
367  }
368  bool operator!=(const self& rhs) const {
369  return !(*this == rhs);
370  }
371 protected:
372 
373  void followThen() {
374  while (within_degree() && !at_end())
375  nextThen();
376  }
377 
378  void increment() {
379  assert(!empty());
380 
381  m_next = top();
382  m_next.incrementElse();
383  m_stack.pop_back();
384 
385  followThen();
386 
387  }
388 
389  bool empty() const{
390  return m_stack.empty();
391  }
392 
393  navigator top() const{
394  return m_stack.back();
395  }
396 
397  bool is_path_end() {
398 
399  path_end();
400  return (!m_next.isConstant() && (*m_next >= m_max_idx)) ||
401  m_next.terminalValue();
402  }
403 
404  void path_end() {
405  while (!at_end()) {
406  m_next.incrementElse();
407  }
408  }
409 
410  void nextThen() {
411  assert(!m_next.isConstant());
412  m_stack.push_back(m_next);
413  m_next.incrementThen();
414  }
415 
416 
417 
418  bool within_degree() const {
419 
420  return (*(*this) < m_upperbound);
421  }
422 
423  bool at_end() const {
424 
425  return m_next.isConstant() || (*m_next >= m_max_idx);
426  }
427 
428 private:
429  stack_type m_stack;
430  idx_type m_max_idx;
431  size_type m_upperbound;
432  navigator m_next;
433 };
434 
435 
436 
439 template <class DegreeCacher, class NaviType, class IdxType>
440 typename NaviType::size_type
441 dd_cached_block_degree(const DegreeCacher& cache, NaviType navi,
442  IdxType nextBlock) {
443 
444  typedef typename NaviType::size_type size_type;
445 
446  if( navi.isConstant() || (*navi >= nextBlock) ) // end of block reached
447  return 0;
448 
449  // Look whether result was cached before
450  typename DegreeCacher::node_type result = cache.find(navi, nextBlock);
451  if (result.isValid())
452  return *result;
453 
454  // Get degree of then branch (contains at least one valid path)...
455  size_type deg = dd_cached_block_degree(cache, navi.thenBranch(), nextBlock) + 1;
456 
457  // ... combine with degree of else branch
458  deg = std::max(deg, dd_cached_block_degree(cache, navi.elseBranch(), nextBlock) );
459 
460  // Write result to cache
461  cache.insert(navi, nextBlock, deg);
462 
463  return deg;
464 }
465 
466 
467 template<class DegCacheMgr, class NaviType, class IdxType, class SizeType>
468 bool max_block_degree_on_then(const DegCacheMgr& deg_mgr, NaviType navi,
469  IdxType next_block,
470  SizeType degree, valid_tag is_descending) {
471  navi.incrementThen();
472  return ((dd_cached_block_degree(deg_mgr, navi, next_block/*,degree - 1*/) + 1) == degree);
473 }
474 
475 template<class DegCacheMgr, class NaviType, class IdxType, class SizeType>
476 bool max_block_degree_on_then(const DegCacheMgr& deg_mgr, NaviType navi,
477  IdxType next_block,
478  SizeType degree, invalid_tag non_descending) {
479  navi.incrementElse();
480  return (dd_cached_block_degree(deg_mgr, navi, next_block/*, degree*/) != degree);
481 }
482 
483 
484 // with degree bound
485 template <class CacheType, class DegCacheMgr, class NaviType,
486  class TermType, class Iterator, class SizeType, class DescendingProperty>
487 TermType
488 dd_block_degree_lead(const CacheType& cache_mgr,
489  const DegCacheMgr& deg_mgr,
490  NaviType navi, Iterator block_iter,
491  TermType init, SizeType degree,
492  DescendingProperty prop) {
493 
494  if (navi.isConstant())
495  return cache_mgr.generate(navi);
496 
497  while( (*navi >= *block_iter) && (*block_iter != CUDD_MAXINDEX)) {
498  ++block_iter;
499  degree = dd_cached_block_degree(deg_mgr, navi, *block_iter);
500  }
501 
502 
503  // Check cache for previous results
504  NaviType cached = cache_mgr.find(navi);
505  if (cached.isValid())
506  return cache_mgr.generate(cached);
507 
508  // Go to next branch
509  if ( max_block_degree_on_then(deg_mgr, navi, *block_iter, degree, prop) ) {
510  init = dd_block_degree_lead(cache_mgr, deg_mgr, navi.thenBranch(),
511  block_iter,
512  init, degree - 1, prop).change(*navi);
513  }
514  else {
515  init = dd_block_degree_lead(cache_mgr, deg_mgr, navi.elseBranch(),
516  block_iter,
517  init, degree, prop);
518  }
519 
520  NaviType resultNavi(init.navigation());
521  cache_mgr.insert(navi, resultNavi);
522  deg_mgr.insert(resultNavi, *block_iter, degree);
523 
524  return init;
525 }
526 
527 
528 template <class CacheType, class DegCacheMgr, class NaviType, class Iterator,
529  class TermType, class DescendingProperty>
530 TermType
531 dd_block_degree_lead(const CacheType& cache_mgr, const DegCacheMgr& deg_mgr,
532  NaviType navi, Iterator block_iter, TermType init,
533  DescendingProperty prop){
534 
535  if (navi.isConstant())
536  return cache_mgr.generate(navi);
537 
538  return dd_block_degree_lead(cache_mgr, deg_mgr, navi,block_iter, init,
539  dd_cached_block_degree(deg_mgr, navi,
540  *block_iter), prop);
541 }
542 
543 
544 template <class FirstIterator, class SecondIterator, class IdxType,
545  class BinaryPredicate>
546 CTypes::comp_type
547 restricted_lex_compare_3way(FirstIterator start, FirstIterator finish,
548  SecondIterator rhs_start, SecondIterator rhs_finish,
549  IdxType max_index,
550  BinaryPredicate idx_comp) {
551 
552  while ( (start != finish) && (*start < max_index) && (rhs_start != rhs_finish)
553  && (*rhs_start < max_index) && (*start == *rhs_start) ) {
554  ++start; ++rhs_start;
555  }
556 
557  if ( (start == finish) || (*start >= max_index) ) {
558  if ( (rhs_start == rhs_finish) || (*rhs_start >= max_index) )
559  return CTypes::equality;
560 
561  return CTypes::less_than;
562  }
563 
564  if ( (rhs_start == rhs_finish) || (*rhs_start >= max_index) )
565  return CTypes::greater_than;
566 
567  return (idx_comp(*start, *rhs_start)?
568  CTypes::greater_than: CTypes::less_than);
569 }
570 
571 
572 
573 
574 template<class LhsIterator, class RhsIterator, class Iterator,
575  class BinaryPredicate>
576 CTypes::comp_type
577 block_dlex_compare(LhsIterator lhsStart, LhsIterator lhsFinish,
578  RhsIterator rhsStart, RhsIterator rhsFinish,
579  Iterator start, Iterator finish,
580  BinaryPredicate idx_comp) {
581 
582  // unsigned lhsdeg = 0, rhsdeg = 0;
583 
584 
585  CTypes::comp_type result = CTypes::equality;
586 
587  while ( (start != finish) && (result == CTypes::equality) ) {
588  unsigned lhsdeg = 0, rhsdeg = 0;
589  LhsIterator oldLhs(lhsStart); // maybe one can save this and do both
590  RhsIterator oldRhs(rhsStart); // comparisons at once.
591 
592  // maybe one can save
593  while( (lhsStart != lhsFinish) && (*lhsStart < *start) ) {
594  ++lhsStart; ++lhsdeg;
595  }
596  while( (rhsStart != rhsFinish) && (*rhsStart < *start) ) {
597  ++rhsStart; ++rhsdeg;
598  }
599  result = generic_compare_3way(lhsdeg, rhsdeg,
600  std::greater<unsigned>() );
601 
602  if (result == CTypes::equality) {
603  result = restricted_lex_compare_3way(oldLhs, lhsFinish,
604  oldRhs, rhsFinish, *start, idx_comp);
605  }
606 
607  ++start;
608  }
609 
610  return result;
611 }
612 
613 
615 template <class IdxType, class Iterator, class BinaryPredicate>
616 CTypes::comp_type
617 block_deg_lex_idx_compare(IdxType lhs, IdxType rhs,
618  Iterator start, Iterator finish,
619  BinaryPredicate idx_comp) {
620 
621  if (lhs == rhs)
622  return CTypes::equality;
623 
624  Iterator lhsend = std::find_if(start, finish,
625  std::bind2nd(std::greater<IdxType>(), lhs));
626 
627 
628  Iterator rhsend = std::find_if(start, finish,
629  std::bind2nd(std::greater<IdxType>(), rhs));
630 
631  assert((lhsend != finish) && (rhsend != finish));
632 
633  CTypes::comp_type result = generic_compare_3way( *lhsend, *rhsend,
634  std::less<IdxType>() );
635 
636  return ( result == CTypes::equality?
637  generic_compare_3way(lhs, rhs, idx_comp): result );
638 }
639