PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00319 //***************************************************************************** 00320 00321 #ifndef BoolePolynomial_h_ 00322 #define BoolePolynomial_h_ 00323 00324 // include standard definitions 00325 #include <vector> 00326 00327 // get standard map functionality 00328 #include <map> 00329 00330 // get standard algorithmic functionalites 00331 #include <algorithm> 00332 00333 #include "BooleRing.h" 00334 // include basic definitions and decision diagram interface 00335 #include "CDDInterface.h" 00336 00337 // include definition of sets of Boolean variables 00338 #include "CTermIter.h" 00339 #include "CBidirectTermIter.h" 00340 00341 #include "pbori_func.h" 00342 #include "pbori_tags.h" 00343 #include "BooleSet.h" 00344 00345 #include "CTermIter.h" 00346 #include "BooleConstant.h" 00347 00348 BEGIN_NAMESPACE_PBORI 00349 00350 00351 // forward declarations 00352 class LexOrder; 00353 class DegLexOrder; 00354 class DegRevLexAscOrder; 00355 class BlockDegLexOrder; 00356 class BlockDegRevLexAscOrder; 00357 00358 class BooleMonomial; 00359 class BooleVariable; 00360 class BooleExponent; 00361 00362 00363 template <class IteratorType, class MonomType> 00364 class CIndirectIter; 00365 00366 template <class IteratorType, class MonomType> 00367 class COrderedIter; 00368 00369 00370 //template<class, class, class, class> class CGenericIter; 00371 template<class, class, class, class> class CDelayedTermIter; 00372 00373 template<class OrderType, class NavigatorType, class MonomType> 00374 class CGenericIter; 00375 00376 template<class OrderType, class NavigatorType, class MonomType> 00377 class MyCGenericIter; 00378 00379 00380 template<class NavigatorType, class ExpType> 00381 class CExpIter; 00382 00383 00389 class BoolePolynomial; 00390 BoolePolynomial 00391 operator+(const BoolePolynomial& lhs, const BoolePolynomial& rhs); 00392 00393 class BoolePolynomial { 00394 00395 public: 00396 00398 friend class BooleMonomial; 00399 00400 //------------------------------------------------------------------------- 00401 // types definitions 00402 //------------------------------------------------------------------------- 00403 00405 typedef BoolePolynomial self; 00406 00408 00409 typedef CTypes::manager_type manager_type; 00410 typedef CTypes::manager_reference manager_reference; 00411 typedef CTypes::manager_ptr manager_ptr; 00412 typedef CTypes::dd_type dd_type; 00413 typedef CTypes::size_type size_type; 00414 typedef CTypes::idx_type idx_type; 00415 typedef CTypes::bool_type bool_type; 00416 typedef CTypes::ostream_type ostream_type; 00417 typedef CTypes::hash_type hash_type; 00419 00421 typedef dd_type::first_iterator first_iterator; 00422 00424 typedef dd_type::navigator navigator; 00425 00427 typedef dd_type::pretty_out_type pretty_out_type; 00428 00430 typedef dd_type::filename_type filename_type; 00431 00433 00435 typedef BooleMonomial monom_type; 00436 00438 typedef BooleVariable var_type; 00439 00441 typedef BooleExponent exp_type; 00442 00444 typedef BooleConstant constant_type; 00445 00447 typedef BooleRing ring_type; 00448 00450 typedef 00451 binary_composition< std::plus<size_type>, 00452 project_ith<1>, integral_constant<size_type, 1> > 00453 increment_type; 00454 00456 typedef 00457 binary_composition< std::minus<size_type>, 00458 project_ith<1>, integral_constant<size_type, 1> > 00459 decrement_type; 00460 00461 00462 00464 // typedef COrderedIter<exp_type> ordered_exp_iterator; 00465 typedef COrderedIter<navigator, exp_type> ordered_exp_iterator; 00466 00468 // typedef COrderedIter<monom_type> ordered_iterator; 00469 typedef COrderedIter<navigator, monom_type> ordered_iterator; 00470 00472 00473 typedef CGenericIter<LexOrder, navigator, monom_type> lex_iterator; 00475 typedef CGenericIter<DegLexOrder, navigator, monom_type> dlex_iterator; 00476 typedef CGenericIter<DegRevLexAscOrder, navigator, monom_type> 00477 dp_asc_iterator; 00478 00479 typedef CGenericIter<BlockDegLexOrder, navigator, monom_type> 00480 block_dlex_iterator; 00481 typedef CGenericIter<BlockDegRevLexAscOrder, navigator, monom_type> 00482 block_dp_asc_iterator; 00483 00484 typedef CGenericIter<LexOrder, navigator, exp_type> lex_exp_iterator; 00485 typedef CGenericIter<DegLexOrder, navigator, exp_type> dlex_exp_iterator; 00486 typedef CGenericIter<DegRevLexAscOrder, navigator, exp_type> 00487 dp_asc_exp_iterator; 00488 typedef CGenericIter<BlockDegLexOrder, navigator, exp_type> 00489 block_dlex_exp_iterator; 00490 typedef CGenericIter<BlockDegRevLexAscOrder, navigator, exp_type> 00491 block_dp_asc_exp_iterator; 00493 00495 typedef lex_iterator const_iterator; 00496 00498 typedef CExpIter<navigator, exp_type> exp_iterator; 00499 00501 typedef CGenericIter<LexOrder, navigator, size_type> deg_iterator; 00502 00504 typedef std::vector<monom_type> termlist_type; 00505 00507 typedef dd_type::easy_equality_property easy_equality_property; 00508 00510 typedef BooleSet set_type; 00511 00513 typedef std::map<self, idx_type, symmetric_composition< 00514 std::less<navigator>, navigates<self> > > idx_map_type; 00515 typedef std::map<self, std::vector<self>, symmetric_composition< 00516 std::less<navigator>, navigates<self> > > poly_vec_map_type; 00517 00518 //------------------------------------------------------------------------- 00519 // constructors and destructor 00520 //------------------------------------------------------------------------- 00521 00523 BoolePolynomial(); 00524 00526 explicit BoolePolynomial(constant_type); 00527 00529 BoolePolynomial(constant_type isOne, const ring_type& ring): 00530 m_dd(isOne? ring.one(): ring.zero() ) { } 00531 00533 BoolePolynomial(const dd_type& rhs): m_dd(rhs) {} 00534 00536 BoolePolynomial(const set_type& rhs): m_dd(rhs.diagram()) {} 00537 00539 BoolePolynomial(const exp_type&, const ring_type&); 00540 00542 BoolePolynomial(const navigator& rhs, const ring_type& ring): 00543 m_dd(ring.manager().manager(), rhs) { 00544 assert(rhs.isValid()); 00545 } 00546 00548 ~BoolePolynomial() {} 00549 00550 //------------------------------------------------------------------------- 00551 // operators and member functions 00552 //------------------------------------------------------------------------- 00553 00554 // self& operator=(const self& rhs) { 00555 // return m_dd = rhs.m_dd; 00556 // } 00557 00558 self& operator=(constant_type rhs) { 00559 return (*this) = self(rhs);//rhs.generate(*this); 00560 } 00562 00563 const self& operator-() const { return *this; } 00564 self& operator+=(const self&); 00565 self& operator+=(constant_type rhs) { 00566 00567 //return *this = (self(*this) + (rhs).generate(*this)); 00568 if (rhs) (*this) = (*this + ring().one()); 00569 return *this; 00570 } 00571 template <class RHSType> 00572 self& operator-=(const RHSType& rhs) { return operator+=(rhs); } 00573 self& operator*=(const monom_type&); 00574 self& operator*=(const exp_type&); 00575 self& operator*=(const self&); 00576 self& operator*=(constant_type rhs) { 00577 if (!rhs) *this = ring().zero(); 00578 return *this; 00579 } 00580 self& operator/=(const monom_type&); 00581 self& operator/=(const exp_type&); 00582 self& operator/=(const self& rhs); 00583 self& operator/=(constant_type rhs); 00584 self& operator%=(const monom_type&); 00585 self& operator%=(const self& rhs) { 00586 return (*this) -= (self(rhs) *= (self(*this) /= rhs)); 00587 } 00588 self& operator%=(constant_type rhs) { return (*this) /= (!rhs); } 00590 00592 00593 bool_type operator==(const self& rhs) const { return (m_dd == rhs.m_dd); } 00594 bool_type operator!=(const self& rhs) const { return (m_dd != rhs.m_dd); } 00595 bool_type operator==(constant_type rhs) const { 00596 return ( rhs? isOne(): isZero() ); 00597 } 00598 bool_type operator!=(constant_type rhs) const { 00599 return ( rhs? (!(isZero())): (!(isOne())) ); 00600 } 00602 00604 bool_type isZero() const { return m_dd.emptiness(); } 00605 00607 bool_type isOne() const { return m_dd.blankness(); } 00608 00610 bool_type isConstant() const { return m_dd.isConstant(); } 00611 00613 bool_type hasConstantPart() const { return m_dd.ownsOne(); } 00614 00616 bool_type reducibleBy(const self&) const; 00617 00619 monom_type lead() const; 00620 00622 monom_type lexLead() const; 00623 00625 monom_type boundedLead(size_type bound) const; 00626 00628 exp_type leadExp() const; 00629 00631 exp_type boundedLeadExp(size_type bound) const; 00632 00634 set_type lmDivisors() const { return leadFirst().firstDivisors(); }; 00635 00637 hash_type hash() const { return m_dd.hash(); } 00638 00640 hash_type stableHash() const { return m_dd.stableHash(); } 00641 00643 hash_type lmStableHash() const; 00644 00646 size_type deg() const; 00647 00649 size_type lmDeg() const; 00650 00652 size_type lexLmDeg() const; 00653 00655 size_type totalDeg() const; 00656 00658 size_type lmTotalDeg() const; 00659 00661 self gradedPart(size_type deg) const; 00662 00664 size_type nNodes() const; 00665 00667 size_type nUsedVariables() const; 00668 00670 monom_type usedVariables() const; 00671 00673 exp_type usedVariablesExp() const; 00674 00676 size_type length() const; 00677 00679 ostream_type& print(ostream_type&) const; 00680 00682 void prettyPrint() const; 00683 00685 void prettyPrint(const char* filename) const; 00686 00688 const_iterator begin() const; 00689 00691 const_iterator end() const; 00692 00694 exp_iterator expBegin() const; 00695 00697 exp_iterator expEnd() const; 00698 00700 first_iterator firstBegin() const; 00701 00703 first_iterator firstEnd() const; 00704 00706 monom_type firstTerm() const; 00707 00709 deg_iterator degBegin() const; 00710 00712 deg_iterator degEnd() const; 00713 00715 ordered_iterator orderedBegin() const; 00716 00718 ordered_iterator orderedEnd() const; 00719 00721 ordered_exp_iterator orderedExpBegin() const; 00722 00724 ordered_exp_iterator orderedExpEnd() const; 00725 00727 00728 lex_iterator genericBegin(lex_tag) const; 00729 lex_iterator genericEnd(lex_tag) const; 00730 dlex_iterator genericBegin(dlex_tag) const; 00731 dlex_iterator genericEnd(dlex_tag) const; 00732 dp_asc_iterator genericBegin(dp_asc_tag) const; 00733 dp_asc_iterator genericEnd(dp_asc_tag) const; 00734 block_dlex_iterator genericBegin(block_dlex_tag) const; 00735 block_dlex_iterator genericEnd(block_dlex_tag) const; 00736 block_dp_asc_iterator genericBegin(block_dp_asc_tag) const; 00737 block_dp_asc_iterator genericEnd(block_dp_asc_tag) const; 00738 00739 00740 lex_exp_iterator genericExpBegin(lex_tag) const; 00741 lex_exp_iterator genericExpEnd(lex_tag) const; 00742 dlex_exp_iterator genericExpBegin(dlex_tag) const; 00743 dlex_exp_iterator genericExpEnd(dlex_tag) const; 00744 dp_asc_exp_iterator genericExpBegin(dp_asc_tag) const; 00745 dp_asc_exp_iterator genericExpEnd(dp_asc_tag) const; 00746 block_dlex_exp_iterator genericExpBegin(block_dlex_tag) const; 00747 block_dlex_exp_iterator genericExpEnd(block_dlex_tag) const; 00748 block_dp_asc_exp_iterator genericExpBegin(block_dp_asc_tag) const; 00749 block_dp_asc_exp_iterator genericExpEnd(block_dp_asc_tag) const; 00751 00753 navigator navigation() const { return m_dd.navigation(); } 00754 00756 navigator endOfNavigation() const { return navigator(); } 00757 00759 dd_type copyDiagram(){ return diagram(); } 00760 00762 operator set_type() const { return set(); }; 00763 00764 size_type eliminationLength() const; 00765 size_type eliminationLengthWithDegBound(size_type garantied_deg_bound) const; 00767 void fetchTerms(termlist_type&) const; 00768 00770 termlist_type terms() const; 00771 00773 const dd_type& diagram() const { return m_dd; } 00774 00776 set_type set() const { return m_dd; } 00777 00779 bool_type isSingleton() const { return dd_is_singleton(navigation()); } 00780 00782 bool_type isSingletonOrPair() const { 00783 return dd_is_singleton_or_pair(navigation()); 00784 } 00785 00787 bool_type isPair() const { return dd_is_pair(navigation()); } 00788 00790 ring_type ring() const { return ring_type(m_dd.manager()); } 00791 00792 protected: 00793 00795 dd_type& internalDiagram() { return m_dd; } 00796 00798 self leadFirst() const; 00799 00801 set_type firstDivisors() const; 00802 00803 00804 private: 00806 dd_type m_dd; 00807 }; 00808 00809 00811 inline BoolePolynomial 00812 operator+(const BoolePolynomial& lhs, const BoolePolynomial& rhs) { 00813 00814 return BoolePolynomial(lhs) += rhs; 00815 } 00817 inline BoolePolynomial 00818 operator+(const BoolePolynomial& lhs, BooleConstant rhs) { 00819 return BoolePolynomial(lhs) += (rhs); 00820 //return BoolePolynomial(lhs) += BoolePolynomial(rhs); 00821 } 00822 00824 inline BoolePolynomial 00825 operator+(BooleConstant lhs, const BoolePolynomial& rhs) { 00826 00827 return BoolePolynomial(rhs) += (lhs); 00828 } 00829 00830 00832 template <class RHSType> 00833 inline BoolePolynomial 00834 operator-(const BoolePolynomial& lhs, const RHSType& rhs) { 00835 00836 return BoolePolynomial(lhs) -= rhs; 00837 } 00839 inline BoolePolynomial 00840 operator-(const BooleConstant& lhs, const BoolePolynomial& rhs) { 00841 00842 return -(BoolePolynomial(rhs) -= lhs); 00843 } 00844 00845 00847 #define PBORI_RHS_MULT(type) inline BoolePolynomial \ 00848 operator*(const BoolePolynomial& lhs, const type& rhs) { \ 00849 return BoolePolynomial(lhs) *= rhs; } 00850 00851 PBORI_RHS_MULT(BoolePolynomial) 00852 PBORI_RHS_MULT(BooleMonomial) 00853 PBORI_RHS_MULT(BooleExponent) 00854 PBORI_RHS_MULT(BooleConstant) 00855 00856 00857 #undef PBORI_RHS_MULT 00858 00860 #define PBORI_LHS_MULT(type) inline BoolePolynomial \ 00861 operator*(const type& lhs, const BoolePolynomial& rhs) { return rhs * lhs; } 00862 00863 PBORI_LHS_MULT(BooleMonomial) 00864 PBORI_LHS_MULT(BooleExponent) 00865 PBORI_LHS_MULT(BooleConstant) 00866 00867 #undef PBORI_LHS_MULT 00868 00869 00871 template <class RHSType> 00872 inline BoolePolynomial 00873 operator/(const BoolePolynomial& lhs, const RHSType& rhs){ 00874 return BoolePolynomial(lhs) /= rhs; 00875 } 00876 00878 template <class RHSType> 00879 inline BoolePolynomial 00880 operator%(const BoolePolynomial& lhs, const RHSType& rhs){ 00881 00882 return BoolePolynomial(lhs) %= rhs; 00883 } 00884 00886 inline BoolePolynomial::bool_type 00887 operator==(BoolePolynomial::bool_type lhs, const BoolePolynomial& rhs) { 00888 00889 return (rhs == lhs); 00890 } 00891 00893 inline BoolePolynomial::bool_type 00894 operator!=(BoolePolynomial::bool_type lhs, const BoolePolynomial& rhs) { 00895 00896 return (rhs != lhs); 00897 } 00898 00900 BoolePolynomial::ostream_type& 00901 operator<<(BoolePolynomial::ostream_type&, const BoolePolynomial&); 00902 00903 // tests whether polynomial can be reduced by rhs 00904 inline BoolePolynomial::bool_type 00905 BoolePolynomial::reducibleBy(const self& rhs) const { 00906 00907 PBORI_TRACE_FUNC( "BoolePolynomial::reducibleBy(const self&) const" ); 00908 00909 if( rhs.isOne() ) 00910 return true; 00911 00912 if( isZero() ) 00913 return rhs.isZero(); 00914 00915 return std::includes(firstBegin(), firstEnd(), 00916 rhs.firstBegin(), rhs.firstEnd()); 00917 00918 } 00919 00920 00921 END_NAMESPACE_PBORI 00922 00923 #endif // of BoolePolynomial_h_