PolyBoRi
PolynomialSugar.h
Go to the documentation of this file.
1 // -*- c++ -*-
2 //*****************************************************************************
14 //*****************************************************************************
15 
16 #ifndef polybori_groebner_PolynomialSugar_h_
17 #define polybori_groebner_PolynomialSugar_h_
18 
19 // include basic definitions
20 #include "groebner_defs.h"
21 
23 
29 public:
30  PolynomialSugar(const Polynomial& poly): lm(poly.ring()), p(poly), exp(){
31  sugar=p.deg();
32  if (!(p.isZero())){
33  this->lm=p.boundedLead(sugar);
34  this->exp=lm.exp();
35  PBORI_ASSERT(lm==p.lead());
36  PBORI_ASSERT(exp==p.leadExp());
37  }
38 
39  length=p.length();
40  }
41  PolynomialSugar(const Polynomial& poly, int sugar, len_type length):
42  lm(poly.ring()), p(poly), exp() {
43 
44  PBORI_ASSERT(length>=0);
45 
46  //sugar=p.deg();
47  this->sugar=sugar;
48  this->length=length;
49  PBORI_ASSERT(sugar>=p.deg());
50  PBORI_ASSERT(length>=p.length());
51  if (!(p.isZero())){
52  this->lm=p.boundedLead(sugar);
53  this->exp=lm.exp();
54  PBORI_ASSERT(lm==p.lead());
55  PBORI_ASSERT(exp==p.leadExp());
56  }
57  }
58  const BooleMonomial& lead() const{
59  return this->lm;
60  }
61  const Exponent& leadExp() const{
62  return this->exp;
63  }
64  deg_type getSugar() const{
65  return sugar;
66  }
68  return length;
69  }
70  bool isZero() const{
71  return p.isZero();
72  }
73  void add(const Polynomial p2, deg_type sugar2, wlen_type length){
74  PBORI_ASSERT(p2.leadExp()==exp);
75  PBORI_ASSERT(length>=0);
76  PBORI_ASSERT(length>=p2.length());
77  this->p=p+p2;
78  this->sugar=std::max(sugar2,this->sugar);
79 
80  if (!(p.isZero())){
81  this->lm=this->p.boundedLead(sugar);
82  this->exp=this->lm.exp();
83  } else {
84  lm=Monomial(p2.ring());
85  exp=Exponent();
86  }
87  this->length+=length;
88  this->length-=2;
89  if (p2.ring().ordering().isTotalDegreeOrder()) this->sugar=this->lm.deg();
90 
91  PBORI_ASSERT((p.isZero())|| (lm==p.lead()));
92  PBORI_ASSERT((p.isZero())||(exp==p.leadExp()));
93  }
94  void adjustSugar(){
95  sugar=p.deg();
96  }
97  bool isOne(){
98  return p.isOne();
99  }
100  Polynomial value() const{
101  return p;
102  }
105  wlen_type res=1;
106  if (isZero()) return 0;
107  res=res+(sugar-exp.deg()+1)*(length-1);
108  PBORI_ASSERT(res>=p.eliminationLengthWithDegBound(sugar));
109  return res;
110  //return p.eliminationLengthWithDegBound(sugar);
111  }
112  void adjustLm(){
113  this->lm=this->p.lead();
114  exp=lm.exp();
115  PBORI_ASSERT(lm==p.lead());
116  PBORI_ASSERT(exp==p.leadExp());
117  }
118 protected:
124 };
125 
127 
128 #endif /* polybori_PolynomialSugar_h_ */
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