PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00328 //***************************************************************************** 00329 00330 #ifndef BoolePolynomial_h_ 00331 #define BoolePolynomial_h_ 00332 00333 // include standard definitions 00334 #include <vector> 00335 00336 // get standard map functionality 00337 #include <map> 00338 00339 // get standard algorithmic functionalites 00340 #include <algorithm> 00341 00342 #include "BooleRing.h" 00343 // include basic definitions and decision diagram interface 00344 #include "CDDInterface.h" 00345 00346 // include definition of sets of Boolean variables 00347 #include "CTermIter.h" 00348 #include "CBidirectTermIter.h" 00349 00350 #include "pbori_func.h" 00351 #include "pbori_tags.h" 00352 #include "BooleSet.h" 00353 00354 #include "CTermIter.h" 00355 #include "BooleConstant.h" 00356 00357 BEGIN_NAMESPACE_PBORI 00358 00359 00360 // forward declarations 00361 class LexOrder; 00362 class DegLexOrder; 00363 class DegRevLexAscOrder; 00364 class BlockDegLexOrder; 00365 class BlockDegRevLexAscOrder; 00366 00367 class BooleMonomial; 00368 class BooleVariable; 00369 class BooleExponent; 00370 00371 00372 template <class IteratorType, class MonomType> 00373 class CIndirectIter; 00374 00375 template <class IteratorType, class MonomType> 00376 class COrderedIter; 00377 00378 00379 //template<class, class, class, class> class CGenericIter; 00380 template<class, class, class, class> class CDelayedTermIter; 00381 00382 template<class OrderType, class NavigatorType, class MonomType> 00383 class CGenericIter; 00384 00385 template<class NavigatorType, class ExpType> 00386 class CExpIter; 00387 00388 00394 class BoolePolynomial; 00395 BoolePolynomial 00396 operator+(const BoolePolynomial& lhs, const BoolePolynomial& rhs); 00397 00398 class BoolePolynomial { 00399 00400 public: 00401 00403 friend class BooleMonomial; 00404 00405 //------------------------------------------------------------------------- 00406 // types definitions 00407 //------------------------------------------------------------------------- 00408 00410 typedef BoolePolynomial self; 00411 00413 00414 typedef CTypes::manager_type manager_type; 00415 typedef CTypes::manager_reference manager_reference; 00416 typedef CTypes::manager_ptr manager_ptr; 00417 typedef CTypes::dd_type dd_type; 00418 typedef CTypes::size_type size_type; 00419 typedef CTypes::deg_type deg_type; 00420 typedef CTypes::idx_type idx_type; 00421 typedef CTypes::bool_type bool_type; 00422 typedef CTypes::ostream_type ostream_type; 00423 typedef CTypes::hash_type hash_type; 00425 00427 typedef dd_type::first_iterator first_iterator; 00428 00430 typedef dd_type::navigator navigator; 00431 00433 typedef dd_type::pretty_out_type pretty_out_type; 00434 00436 typedef dd_type::filename_type filename_type; 00437 00439 00441 typedef BooleMonomial monom_type; 00442 00444 typedef BooleVariable var_type; 00445 00447 typedef BooleExponent exp_type; 00448 00450 typedef BooleConstant constant_type; 00451 00453 typedef BooleRing ring_type; 00454 00456 typedef 00457 binary_composition< std::plus<size_type>, 00458 project_ith<1>, integral_constant<size_type, 1> > 00459 increment_type; 00460 00462 typedef 00463 binary_composition< std::minus<size_type>, 00464 project_ith<1>, integral_constant<size_type, 1> > 00465 decrement_type; 00466 00467 00468 00470 // typedef COrderedIter<exp_type> ordered_exp_iterator; 00471 typedef COrderedIter<navigator, exp_type> ordered_exp_iterator; 00472 00474 // typedef COrderedIter<monom_type> ordered_iterator; 00475 typedef COrderedIter<navigator, monom_type> ordered_iterator; 00476 00478 00479 typedef CGenericIter<LexOrder, navigator, monom_type> lex_iterator; 00481 typedef CGenericIter<DegLexOrder, navigator, monom_type> dlex_iterator; 00482 typedef CGenericIter<DegRevLexAscOrder, navigator, monom_type> 00483 dp_asc_iterator; 00484 00485 typedef CGenericIter<BlockDegLexOrder, navigator, monom_type> 00486 block_dlex_iterator; 00487 typedef CGenericIter<BlockDegRevLexAscOrder, navigator, monom_type> 00488 block_dp_asc_iterator; 00489 00490 typedef CGenericIter<LexOrder, navigator, exp_type> lex_exp_iterator; 00491 typedef CGenericIter<DegLexOrder, navigator, exp_type> dlex_exp_iterator; 00492 typedef CGenericIter<DegRevLexAscOrder, navigator, exp_type> 00493 dp_asc_exp_iterator; 00494 typedef CGenericIter<BlockDegLexOrder, navigator, exp_type> 00495 block_dlex_exp_iterator; 00496 typedef CGenericIter<BlockDegRevLexAscOrder, navigator, exp_type> 00497 block_dp_asc_exp_iterator; 00499 00501 typedef lex_iterator const_iterator; 00502 00504 typedef CExpIter<navigator, exp_type> exp_iterator; 00505 00507 typedef CGenericIter<LexOrder, navigator, deg_type> deg_iterator; 00508 00510 typedef std::vector<monom_type> termlist_type; 00511 00513 typedef dd_type::easy_equality_property easy_equality_property; 00514 00516 typedef BooleSet set_type; 00517 00519 typedef std::map<self, idx_type, symmetric_composition< 00520 std::less<navigator>, navigates<self> > > idx_map_type; 00521 typedef std::map<self, std::vector<self>, symmetric_composition< 00522 std::less<navigator>, navigates<self> > > poly_vec_map_type; 00523 00524 //------------------------------------------------------------------------- 00525 // constructors and destructor 00526 //------------------------------------------------------------------------- 00527 00529 BoolePolynomial(); 00530 00532 explicit BoolePolynomial(constant_type); 00533 00535 BoolePolynomial(constant_type isOne, const ring_type& ring): 00536 m_dd(isOne? ring.one(): ring.zero() ) { } 00537 00539 BoolePolynomial(const dd_type& rhs): m_dd(rhs) {} 00540 00542 BoolePolynomial(const set_type& rhs): m_dd(rhs.diagram()) {} 00543 00545 BoolePolynomial(const exp_type&, const ring_type&); 00546 00548 BoolePolynomial(const navigator& rhs, const ring_type& ring): 00549 m_dd(ring.manager().manager(), rhs) { 00550 assert(rhs.isValid()); 00551 } 00552 00554 ~BoolePolynomial() {} 00555 00556 //------------------------------------------------------------------------- 00557 // operators and member functions 00558 //------------------------------------------------------------------------- 00559 00560 // self& operator=(const self& rhs) { 00561 // return m_dd = rhs.m_dd; 00562 // } 00563 00564 self& operator=(constant_type rhs) { 00565 return (*this) = self(rhs);//rhs.generate(*this); 00566 } 00568 00569 const self& operator-() const { return *this; } 00570 self& operator+=(const self&); 00571 self& operator+=(constant_type rhs) { 00572 00573 //return *this = (self(*this) + (rhs).generate(*this)); 00574 if (rhs) (*this) = (*this + ring().one()); 00575 return *this; 00576 } 00577 template <class RHSType> 00578 self& operator-=(const RHSType& rhs) { return operator+=(rhs); } 00579 self& operator*=(const monom_type&); 00580 self& operator*=(const exp_type&); 00581 self& operator*=(const self&); 00582 self& operator*=(constant_type rhs) { 00583 if (!rhs) *this = ring().zero(); 00584 return *this; 00585 } 00586 self& operator/=(const monom_type&); 00587 self& operator/=(const exp_type&); 00588 self& operator/=(const self& rhs); 00589 self& operator/=(constant_type rhs); 00590 self& operator%=(const monom_type&); 00591 self& operator%=(const self& rhs) { 00592 return (*this) -= (self(rhs) *= (self(*this) /= rhs)); 00593 } 00594 self& operator%=(constant_type rhs) { return (*this) /= (!rhs); } 00596 00598 00599 bool_type operator==(const self& rhs) const { return (m_dd == rhs.m_dd); } 00600 bool_type operator!=(const self& rhs) const { return (m_dd != rhs.m_dd); } 00601 bool_type operator==(constant_type rhs) const { 00602 return ( rhs? isOne(): isZero() ); 00603 } 00604 bool_type operator!=(constant_type rhs) const { 00605 //return ( rhs? (!(isOne())): (!(isZero())) ); 00606 return (!(*this==rhs)); 00607 } 00609 00611 bool_type isZero() const { return m_dd.emptiness(); } 00612 00614 bool_type isOne() const { return m_dd.blankness(); } 00615 00617 bool_type isConstant() const { return m_dd.isConstant(); } 00618 00620 bool_type hasConstantPart() const { return m_dd.ownsOne(); } 00621 00623 bool_type reducibleBy(const self&) const; 00624 00626 monom_type lead() const; 00627 00629 monom_type lexLead() const; 00630 00632 monom_type boundedLead(size_type bound) const; 00633 00635 exp_type leadExp() const; 00636 00638 exp_type boundedLeadExp(size_type bound) const; 00639 00641 set_type lmDivisors() const { return leadFirst().firstDivisors(); }; 00642 00644 hash_type hash() const { return m_dd.hash(); } 00645 00647 hash_type stableHash() const { return m_dd.stableHash(); } 00648 00650 hash_type lmStableHash() const; 00651 00653 deg_type deg() const; 00654 00656 deg_type lmDeg() const; 00657 00659 deg_type lexLmDeg() const; 00660 00662 deg_type totalDeg() const; 00663 00665 deg_type lmTotalDeg() const; 00666 00668 self gradedPart(deg_type deg) const; 00669 00671 size_type nNodes() const; 00672 00674 size_type nUsedVariables() const; 00675 00677 monom_type usedVariables() const; 00678 00680 exp_type usedVariablesExp() const; 00681 00683 size_type length() const; 00684 00686 ostream_type& print(ostream_type&) const; 00687 00689 void prettyPrint() const; 00690 00692 void prettyPrint(filename_type filename) const; 00693 00695 const_iterator begin() const; 00696 00698 const_iterator end() const; 00699 00701 exp_iterator expBegin() const; 00702 00704 exp_iterator expEnd() const; 00705 00707 first_iterator firstBegin() const; 00708 00710 first_iterator firstEnd() const; 00711 00713 monom_type firstTerm() const; 00714 00716 deg_iterator degBegin() const; 00717 00719 deg_iterator degEnd() const; 00720 00722 ordered_iterator orderedBegin() const; 00723 00725 ordered_iterator orderedEnd() const; 00726 00728 ordered_exp_iterator orderedExpBegin() const; 00729 00731 ordered_exp_iterator orderedExpEnd() const; 00732 00734 00735 lex_iterator genericBegin(lex_tag) const; 00736 lex_iterator genericEnd(lex_tag) const; 00737 dlex_iterator genericBegin(dlex_tag) const; 00738 dlex_iterator genericEnd(dlex_tag) const; 00739 dp_asc_iterator genericBegin(dp_asc_tag) const; 00740 dp_asc_iterator genericEnd(dp_asc_tag) const; 00741 block_dlex_iterator genericBegin(block_dlex_tag) const; 00742 block_dlex_iterator genericEnd(block_dlex_tag) const; 00743 block_dp_asc_iterator genericBegin(block_dp_asc_tag) const; 00744 block_dp_asc_iterator genericEnd(block_dp_asc_tag) const; 00745 00746 00747 lex_exp_iterator genericExpBegin(lex_tag) const; 00748 lex_exp_iterator genericExpEnd(lex_tag) const; 00749 dlex_exp_iterator genericExpBegin(dlex_tag) const; 00750 dlex_exp_iterator genericExpEnd(dlex_tag) const; 00751 dp_asc_exp_iterator genericExpBegin(dp_asc_tag) const; 00752 dp_asc_exp_iterator genericExpEnd(dp_asc_tag) const; 00753 block_dlex_exp_iterator genericExpBegin(block_dlex_tag) const; 00754 block_dlex_exp_iterator genericExpEnd(block_dlex_tag) const; 00755 block_dp_asc_exp_iterator genericExpBegin(block_dp_asc_tag) const; 00756 block_dp_asc_exp_iterator genericExpEnd(block_dp_asc_tag) const; 00758 00760 navigator navigation() const { return m_dd.navigation(); } 00761 00763 navigator endOfNavigation() const { return navigator(); } 00764 00766 dd_type copyDiagram(){ return diagram(); } 00767 00769 operator set_type() const { return set(); }; 00770 00771 size_type eliminationLength() const; 00772 size_type eliminationLengthWithDegBound(deg_type garantied_deg_bound) const; 00774 void fetchTerms(termlist_type&) const; 00775 00777 termlist_type terms() const; 00778 00780 const dd_type& diagram() const { return m_dd; } 00781 00783 set_type set() const { return m_dd; } 00784 00786 bool_type isSingleton() const { return dd_is_singleton(navigation()); } 00787 00789 bool_type isSingletonOrPair() const { 00790 return dd_is_singleton_or_pair(navigation()); 00791 } 00792 00794 bool_type isPair() const { return dd_is_pair(navigation()); } 00795 00797 ring_type ring() const { return ring_type(m_dd.manager()); } 00798 00799 protected: 00800 00802 dd_type& internalDiagram() { return m_dd; } 00803 00805 self leadFirst() const; 00806 00808 set_type firstDivisors() const; 00809 00810 00811 private: 00813 dd_type m_dd; 00814 }; 00815 00816 00818 inline BoolePolynomial 00819 operator+(const BoolePolynomial& lhs, const BoolePolynomial& rhs) { 00820 00821 return BoolePolynomial(lhs) += rhs; 00822 } 00824 inline BoolePolynomial 00825 operator+(const BoolePolynomial& lhs, BooleConstant rhs) { 00826 return BoolePolynomial(lhs) += (rhs); 00827 //return BoolePolynomial(lhs) += BoolePolynomial(rhs); 00828 } 00829 00831 inline BoolePolynomial 00832 operator+(BooleConstant lhs, const BoolePolynomial& rhs) { 00833 00834 return BoolePolynomial(rhs) += (lhs); 00835 } 00836 00837 00839 template <class RHSType> 00840 inline BoolePolynomial 00841 operator-(const BoolePolynomial& lhs, const RHSType& rhs) { 00842 00843 return BoolePolynomial(lhs) -= rhs; 00844 } 00846 inline BoolePolynomial 00847 operator-(const BooleConstant& lhs, const BoolePolynomial& rhs) { 00848 00849 return -(BoolePolynomial(rhs) -= lhs); 00850 } 00851 00852 00854 #define PBORI_RHS_MULT(type) inline BoolePolynomial \ 00855 operator*(const BoolePolynomial& lhs, const type& rhs) { \ 00856 return BoolePolynomial(lhs) *= rhs; } 00857 00858 PBORI_RHS_MULT(BoolePolynomial) 00859 PBORI_RHS_MULT(BooleMonomial) 00860 PBORI_RHS_MULT(BooleExponent) 00861 PBORI_RHS_MULT(BooleConstant) 00862 00863 00864 #undef PBORI_RHS_MULT 00865 00867 #define PBORI_LHS_MULT(type) inline BoolePolynomial \ 00868 operator*(const type& lhs, const BoolePolynomial& rhs) { return rhs * lhs; } 00869 00870 PBORI_LHS_MULT(BooleMonomial) 00871 PBORI_LHS_MULT(BooleExponent) 00872 PBORI_LHS_MULT(BooleConstant) 00873 00874 #undef PBORI_LHS_MULT 00875 00876 00878 template <class RHSType> 00879 inline BoolePolynomial 00880 operator/(const BoolePolynomial& lhs, const RHSType& rhs){ 00881 return BoolePolynomial(lhs) /= rhs; 00882 } 00883 00885 template <class RHSType> 00886 inline BoolePolynomial 00887 operator%(const BoolePolynomial& lhs, const RHSType& rhs){ 00888 00889 return BoolePolynomial(lhs) %= rhs; 00890 } 00891 00893 inline BoolePolynomial::bool_type 00894 operator==(BoolePolynomial::bool_type lhs, const BoolePolynomial& rhs) { 00895 00896 return (rhs == lhs); 00897 } 00898 00900 inline BoolePolynomial::bool_type 00901 operator!=(BoolePolynomial::bool_type lhs, const BoolePolynomial& rhs) { 00902 00903 return (rhs != lhs); 00904 } 00905 00907 BoolePolynomial::ostream_type& 00908 operator<<(BoolePolynomial::ostream_type&, const BoolePolynomial&); 00909 00910 // tests whether polynomial can be reduced by rhs 00911 inline BoolePolynomial::bool_type 00912 BoolePolynomial::reducibleBy(const self& rhs) const { 00913 00914 PBORI_TRACE_FUNC( "BoolePolynomial::reducibleBy(const self&) const" ); 00915 00916 if( rhs.isOne() ) 00917 return true; 00918 00919 if( isZero() ) 00920 return rhs.isZero(); 00921 00922 return std::includes(firstBegin(), firstEnd(), 00923 rhs.firstBegin(), rhs.firstEnd()); 00924 00925 } 00926 00927 00928 END_NAMESPACE_PBORI 00929 00930 #endif // of BoolePolynomial_h_