16 #ifndef polybori_groebner_PolynomialSugar_h_
17 #define polybori_groebner_PolynomialSugar_h_
33 this->lm=p.boundedLead(sugar);
42 lm(poly.ring()), p(poly), exp() {
52 this->lm=p.boundedLead(sugar);
78 this->sugar=std::max(sugar2,this->sugar);
81 this->lm=this->p.boundedLead(sugar);
82 this->exp=this->lm.exp();
89 if (p2.ring().ordering().isTotalDegreeOrder()) this->sugar=this->lm.deg();
106 if (isZero())
return 0;
107 res=res+(sugar-exp.deg()+1)*(length-1);
108 PBORI_ASSERT(res>=p.eliminationLengthWithDegBound(sugar));
113 this->lm=this->p.lead();
This class is just a wrapper for using variables for storing indices as interim data structure for Bo...
Definition: BooleExponent.h:34
deg_type getSugar() const
Definition: PolynomialSugar.h:64
polybori::BooleExponent Exponent
Definition: groebner_defs.h:33
#define END_NAMESPACE_PBORIGB
Definition: groebner_defs.h:16
Polynomial p
Definition: PolynomialSugar.h:122
int deg_type
Definition: groebner_defs.h:42
wlen_type eliminationLength() const
Definition: PolynomialSugar.h:103
long len_type
Definition: groebner_defs.h:41
const BooleMonomial & lead() const
Definition: PolynomialSugar.h:58
Polynomial value() const
Definition: PolynomialSugar.h:100
len_type length
Definition: PolynomialSugar.h:120
bool isOne()
Definition: PolynomialSugar.h:97
#define BEGIN_NAMESPACE_PBORIGB
Definition: groebner_defs.h:15
void adjustSugar()
Definition: PolynomialSugar.h:94
bool isZero() const
Definition: PolynomialSugar.h:70
This class wraps the underlying decicion diagram type and defines the necessary operations.
Definition: BoolePolynomial.h:85
deg_type sugar
Definition: PolynomialSugar.h:121
void add(const Polynomial p2, deg_type sugar2, wlen_type length)
Definition: PolynomialSugar.h:73
Exponent exp
Definition: PolynomialSugar.h:123
PolynomialSugar(const Polynomial &poly, int sugar, len_type length)
Definition: PolynomialSugar.h:41
exp_type leadExp() const
Get leading term.
Definition: BoolePolynomial.cc:258
#define PBORI_ASSERT(arg)
Definition: pbori_defs.h:118
Monomial lm
Definition: PolynomialSugar.h:119
long wlen_type
Definition: groebner_defs.h:39
size_type length() const
Returns number of terms.
Definition: BoolePolynomial.cc:414
This class defines PolynomialSugar.
Definition: PolynomialSugar.h:28
const Exponent & leadExp() const
Definition: PolynomialSugar.h:61
void adjustLm()
Definition: PolynomialSugar.h:112
This class is just a wrapper for using variables from cudd's decicion diagram.
Definition: BooleMonomial.h:50
BooleMonomial Monomial
Definition: embed.h:53
wlen_type getLengthEstimation() const
Definition: PolynomialSugar.h:67
PolynomialSugar(const Polynomial &poly)
Definition: PolynomialSugar.h:30