00001
00002
00003
00004
00005
00006
00007
00008
00009 #include <functional>
00010 #include "groebner_defs.h"
00011
00012 #include "LiteralFactorization.h"
00013 #include <boost/shared_ptr.hpp>
00014 #include <queue>
00015 #include <algorithm>
00016 #include <utility>
00017 #include <set>
00018 #include <vector>
00019
00020 #ifndef PB_LEXBUCKETS_H
00021 #define PB_LEXBUCKETS_H
00022
00023 BEGIN_NAMESPACE_PBORIGB
00024 Polynomial without_prior_part(Polynomial p, idx_type tail_start);
00025
00026 class LexBucket{
00027
00028 public:
00029 static const int var_group_size=1;
00030 BoolePolyRing ring;
00031 LexBucket(const BoolePolyRing& input_ring): ring(input_ring), front(input_ring) {
00032 ones=false;
00033 updateTailStart();
00034 }
00035 LexBucket& operator+=(const Polynomial& p);
00036 LexBucket(const Polynomial& p): ring(p.ring()), front(p) {
00037 ones=false;
00038 if (!(p.isConstant())){
00039 updateTailStart();
00040 Polynomial back=without_prior_part(p, tail_start);
00041 if (!(back.isZero())){
00042 if (back.isOne()){
00043 ones=(!(ones));
00044 } else{
00045 buckets.push_back(back);
00046 }
00047 }
00048 front-=back;
00049 } else {
00050 updateTailStart();
00051 front=0;
00052 if (p.isOne()) ones=true;
00053 }
00054 }
00055 void clearFront(){
00056 front=0;
00057 while((front.isZero())&& (buckets.size()>0)){
00058 increaseTailStart(tail_start+var_group_size);
00059 }
00060 }
00061 Exponent leadExp();
00062 bool isZero();
00063
00064 void updateTailStart();
00065 idx_type getTailStart();
00066 void increaseTailStart(idx_type new_start);
00067 Polynomial value();
00068 Polynomial getFront(){
00069 return front;
00070 }
00071
00072 bool isOne(){
00073 usualAssertions();
00074 if ((front.isZero()) && (ones) && (buckets.size()==0)) return true;
00075 else return false;
00076 }
00077 private:
00078 void usualAssertions(){
00079 PBORI_ASSERT((buckets.size()==0)||(!(front.isZero())));
00080 }
00081 std::vector<Polynomial> buckets;
00082 Polynomial front;
00083 idx_type tail_start;
00084 bool ones;
00085
00086 };
00087
00088 END_NAMESPACE_PBORIGB
00089
00090 #endif