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
This class is just a wrapper for using variables for storing indices as interim data structure for Bo...
Definition: BooleExponent.h:34
bool_type isOne() const
Check whether polynomial is constant one.
Definition: BoolePolynomial.h:297
bool isOne()
Definition: LexBucket.h:72
#define END_NAMESPACE_PBORIGB
Definition: groebner_defs.h:16
bool_type isConstant() const
Check whether polynomial is zero or one.
Definition: BoolePolynomial.h:300
BoolePolyRing ring
Definition: LexBucket.h:30
LexBucket(const Polynomial &p)
Definition: LexBucket.h:36
This class reinterprets decicion diagram managers as Boolean polynomial rings, adds an ordering and v...
Definition: BoolePolyRing.h:40
BoolePolynomial Polynomial
Definition: embed.h:51
#define BEGIN_NAMESPACE_PBORIGB
Definition: groebner_defs.h:15
LexBucket(const BoolePolyRing &input_ring)
Definition: LexBucket.h:31
This class wraps the underlying decicion diagram type and defines the necessary operations.
Definition: BoolePolynomial.h:85
Definition: LexBucket.h:26
#define PBORI_ASSERT(arg)
Definition: pbori_defs.h:118
void clearFront()
Definition: LexBucket.h:55
bool_type isZero() const
Check whether polynomial is constant zero.
Definition: BoolePolynomial.h:294
polybori::CTypes::idx_type idx_type
Definition: groebner_defs.h:44
Polynomial getFront()
Definition: LexBucket.h:68
Polynomial without_prior_part(Polynomial p, idx_type tail_start)
Definition: LexBucket.cc:23