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