PolyBoRi
MinimalLeadingTerms.h
Go to the documentation of this file.
1 // -*- c++ -*-
2 //*****************************************************************************
14 //*****************************************************************************
15 
16 #ifndef polybori_groebner_MinimalLeadingTerms_h_
17 #define polybori_groebner_MinimalLeadingTerms_h_
18 
19 // include basic definitions
20 #include "groebner_defs.h"
21 
23 
30  public MonomialSet {
31 
32  typedef MonomialSet base;
33  typedef MinimalLeadingTerms self;
34 
35 public:
36  template <class Type>
37  MinimalLeadingTerms(const Type& value): base(value) { }
38 
41 
42  MonomialSet divisors(divisorsOf(lm));
43  if(divisors.isZero())
44  return cleanup(lm);
45 
46  return (divisors == lm.set()? lm.ring().zero(): lm.set());
47  }
48 
49 private:
50  self& operator=(const self& rhs) {
51  return static_cast<self&>(static_cast<base&>(*this) = rhs);
52  }
53 
54  MonomialSet cleanup(const Monomial& lm) {
55  MonomialSet removed(multiplesOf(lm).diff(lm.set()));
56 
57  PBORI_ASSERT(removed.intersect(*this).intersect(lm.set()).isZero());
58  PBORI_ASSERT(assertion(lm, removed.expBegin(),removed.expEnd()));
59 
60  *this = diff(removed).unite(lm.set());
61  return removed;
62  }
63 
64  bool assertion(const Monomial& lm,
65  MonomialSet::exp_iterator start,
66  MonomialSet::exp_iterator finish) const {
67  while (start != finish) {
68  if ( (*start) == lm.exp() || !start->reducibleBy(lm.exp()) )
69  return false;
70  ++start;
71  }
72  return true;
73  }
74 };
75 
77 
78 #endif /* polybori_groebner_MinimalLeadingTerms_h_ */
set_type set() const
Get corresponding subset of of the powerset over all variables.
Definition: BooleMonomial.h:216
#define END_NAMESPACE_PBORIGB
Definition: groebner_defs.h:16
dd_type zero() const
Get empty decision diagram.
Definition: BoolePolyRing.cc:42
#define BEGIN_NAMESPACE_PBORIGB
Definition: groebner_defs.h:15
polybori::BooleSet MonomialSet
Definition: groebner_defs.h:45
bool isZero() const
Test whether diagram represents the empty set.
Definition: CCuddDDFacade.h:244
#define PBORI_ASSERT(arg)
Definition: pbori_defs.h:118
const ring_type & ring() const
Access ring, where this belongs to.
Definition: BooleMonomial.h:235
This class defines MinimalLeadingTerms.
Definition: MinimalLeadingTerms.h:29
MonomialSet update(const Monomial &lm)
Insert leading term and return monomials, that are not minimal (any more)
Definition: MinimalLeadingTerms.h:40
MinimalLeadingTerms(const Type &value)
Definition: MinimalLeadingTerms.h:37
Definition: BooleSet.h:57
This class is just a wrapper for using variables from cudd's decicion diagram.
Definition: BooleMonomial.h:50
BooleMonomial Monomial
Definition: embed.h:53