PolyBoRi

BoolePolynomial.h

Go to the documentation of this file.
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_