00001
00002
00328
00329
00330 #ifndef BoolePolynomial_h_
00331 #define BoolePolynomial_h_
00332
00333
00334 #include <vector>
00335
00336
00337 #include <map>
00338
00339
00340 #include <algorithm>
00341
00342 #include "BooleRing.h"
00343
00344 #include "CDDInterface.h"
00345
00346
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
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
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
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
00471 typedef COrderedIter<navigator, exp_type> ordered_exp_iterator;
00472
00474
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
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
00558
00559
00560
00561
00562
00563
00564 self& operator=(constant_type rhs) {
00565 return (*this) = self(rhs);
00566 }
00568
00569 const self& operator-() const { return *this; }
00570 self& operator+=(const self&);
00571 self& operator+=(constant_type rhs) {
00572
00573
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
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 leadDivisors() 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 leadStableHash() const;
00651
00653 deg_type deg() const;
00654
00656 deg_type leadDeg() const;
00657
00659 deg_type lexLeadDeg() const;
00660
00662 deg_type totalDeg() const;
00663
00665 deg_type leadTotalDeg() 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
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
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_