PolyBoRi
lexbuckets.h
Go to the documentation of this file.
1 /*
2  * pairs.h
3  * PolyBoRi
4  *
5  * Created by Michael Brickenstein on 19.04.06.
6  * Copyright 2006 The PolyBoRi Team. See LICENSE file.
7  *
8  */
9 #include <functional>
10 #include "groebner_defs.h"
11 #include "literal_factorization.h"
12 #include <boost/shared_ptr.hpp>
13 #include <queue>
14 #include <algorithm>
15 #include <utility>
16 #include <set>
17 #include <vector>
18 #ifndef PB_LEXBUCKETS_H
19 #define PB_LEXBUCKETS_H
20 
23 class LexBucket{
24  //typedef CTypes::idx_type idx_type;
25 public:
26  static const int var_group_size=1;
28  ones=false;
29  updateTailStart();
30  }
31  LexBucket& operator+=(const Polynomial& p);
32  LexBucket(const Polynomial& p){
33  ones=false;
34  if (!(p.isConstant())){
35  front=p;
36  updateTailStart();
37  Polynomial back=without_prior_part(p, tail_start);
38  if (!(back.isZero())){
39  if (back.isOne()){
40  ones=(!(ones));
41  } else{
42  buckets.push_back(back);
43  }
44  }
45  front-=back;
46  } else {
47  updateTailStart();
48  front=0;
49  if (p.isOne()) ones=true;
50  }
51  }
52  void clearFront(){
53  front=0;
54  while((front.isZero())&& (buckets.size()>0)){
55  increaseTailStart(tail_start+var_group_size);
56  }
57  }
58  Exponent leadExp();
59  bool isZero();
60  //we assume that p has smaller/equal terms than the bucket, or the bucket is zero
61  void updateTailStart();
62  idx_type getTailStart();
63  void increaseTailStart(idx_type new_start);
64  Polynomial value();
66  return front;
67  }
68 
69  bool isOne(){
70  usualAssertions();
71  if ((front.isZero()) && (ones) && (buckets.size()==0)) return true;
72  else return false;
73  }
74 private:
75  void usualAssertions(){
76  assert((buckets.size()==0)||(!(front.isZero())));
77  }
78  std::vector<Polynomial> buckets;
79  Polynomial front;
80  idx_type tail_start;
81  bool ones;
82 
83 };
84 
86 
87 #endif