PolyBoRi
LexBucket.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 
12 #include "LiteralFactorization.h"
13 #include <boost/shared_ptr.hpp>
14 #include <queue>
15 #include <algorithm>
16 #include <utility>
17 #include <set>
18 #include <vector>
19 
20 #ifndef PB_LEXBUCKETS_H
21 #define PB_LEXBUCKETS_H
22 
25 
26 class LexBucket{
27  //typedef CTypes::idx_type idx_type;
28 public:
29  static const int var_group_size=1;
31  LexBucket(const BoolePolyRing& input_ring): ring(input_ring), front(input_ring) {
32  ones=false;
33  updateTailStart();
34  }
35  LexBucket& operator+=(const Polynomial& p);
36  LexBucket(const Polynomial& p): ring(p.ring()), front(p) {
37  ones=false;
38  if (!(p.isConstant())){
39  updateTailStart();
40  Polynomial back=without_prior_part(p, tail_start);
41  if (!(back.isZero())){
42  if (back.isOne()){
43  ones=(!(ones));
44  } else{
45  buckets.push_back(back);
46  }
47  }
48  front-=back;
49  } else {
50  updateTailStart();
51  front=0;
52  if (p.isOne()) ones=true;
53  }
54  }
55  void clearFront(){
56  front=0;
57  while((front.isZero())&& (buckets.size()>0)){
58  increaseTailStart(tail_start+var_group_size);
59  }
60  }
61  Exponent leadExp();
62  bool isZero();
63  //we assume that p has smaller/equal terms than the bucket, or the bucket is zero
64  void updateTailStart();
65  idx_type getTailStart();
66  void increaseTailStart(idx_type new_start);
67  Polynomial value();
69  return front;
70  }
71 
72  bool isOne(){
73  usualAssertions();
74  if ((front.isZero()) && (ones) && (buckets.size()==0)) return true;
75  else return false;
76  }
77 private:
78  void usualAssertions(){
79  PBORI_ASSERT((buckets.size()==0)||(!(front.isZero())));
80  }
81  std::vector<Polynomial> buckets;
82  Polynomial front;
83  idx_type tail_start;
84  bool ones;
85 
86 };
87 
89 
90 #endif