LexBucket.h
Go to the documentation of this file.
/*
* pairs.h
* PolyBoRi
*
* Created by Michael Brickenstein on 19.04.06.
* Copyright 2006 The PolyBoRi Team. See LICENSE file.
*
*/
#include <functional>
#include "groebner_defs.h"
#include "LiteralFactorization.h"
#include <boost/shared_ptr.hpp>
#include <queue>
#include <algorithm>
#include <utility>
#include <set>
#include <vector>
#ifndef PB_LEXBUCKETS_H
#define PB_LEXBUCKETS_H
BEGIN_NAMESPACE_PBORIGB
Polynomial without_prior_part(Polynomial p, idx_type tail_start);
class LexBucket{
//typedef CTypes::idx_type idx_type;
public:
static const int var_group_size=1;
BoolePolyRing ring;
LexBucket(const BoolePolyRing& input_ring): ring(input_ring), front(input_ring) {
ones=false;
updateTailStart();
}
LexBucket& operator+=(const Polynomial& p);
LexBucket(const Polynomial& p): ring(p.ring()), front(p) {
ones=false;
if (!(p.isConstant())){
updateTailStart();
Polynomial back=without_prior_part(p, tail_start);
if (!(back.isZero())){
if (back.isOne()){
ones=(!(ones));
} else{
buckets.push_back(back);
}
}
front-=back;
} else {
updateTailStart();
front=0;
if (p.isOne()) ones=true;
}
}
void clearFront(){
front=0;
while((front.isZero())&& (buckets.size()>0)){
increaseTailStart(tail_start+var_group_size);
}
}
Exponent leadExp();
bool isZero();
//we assume that p has smaller/equal terms than the bucket, or the bucket is zero
void updateTailStart();
idx_type getTailStart();
void increaseTailStart(idx_type new_start);
Polynomial value();
Polynomial getFront(){
return front;
}
bool isOne(){
usualAssertions();
if ((front.isZero()) && (ones) && (buckets.size()==0)) return true;
else return false;
}
private:
void usualAssertions(){
PBORI_ASSERT((buckets.size()==0)||(!(front.isZero())));
}
std::vector<Polynomial> buckets;
Polynomial front;
idx_type tail_start;
bool ones;
};
END_NAMESPACE_PBORIGB
#endif
polybori::BooleExponent
This class is just a wrapper for using variables for storing indices as interim data structure for Bo...
Definition: BooleExponent.h:34
polybori::BoolePolynomial::isOne
bool_type isOne() const
Check whether polynomial is constant one.
Definition: BoolePolynomial.h:297
polybori::groebner::LexBucket::isOne
bool isOne()
Definition: LexBucket.h:72
END_NAMESPACE_PBORIGB
#define END_NAMESPACE_PBORIGB
Definition: groebner_defs.h:16
polybori::BoolePolynomial::isConstant
bool_type isConstant() const
Check whether polynomial is zero or one.
Definition: BoolePolynomial.h:300
polybori::groebner::LexBucket::ring
BoolePolyRing ring
Definition: LexBucket.h:30
polybori::groebner::LexBucket::LexBucket
LexBucket(const Polynomial &p)
Definition: LexBucket.h:36
polybori::BoolePolyRing
This class reinterprets decicion diagram managers as Boolean polynomial rings, adds an ordering and v...
Definition: BoolePolyRing.h:40
polybori::Polynomial
BoolePolynomial Polynomial
Definition: embed.h:51
BEGIN_NAMESPACE_PBORIGB
#define BEGIN_NAMESPACE_PBORIGB
Definition: groebner_defs.h:15
polybori::groebner::LexBucket::LexBucket
LexBucket(const BoolePolyRing &input_ring)
Definition: LexBucket.h:31
polybori::BoolePolynomial
This class wraps the underlying decicion diagram type and defines the necessary operations.
Definition: BoolePolynomial.h:85
groebner_defs.h
polybori::groebner::LexBucket
Definition: LexBucket.h:26
PBORI_ASSERT
#define PBORI_ASSERT(arg)
Definition: pbori_defs.h:118
polybori::groebner::LexBucket::clearFront
void clearFront()
Definition: LexBucket.h:55
polybori::BoolePolynomial::isZero
bool_type isZero() const
Check whether polynomial is constant zero.
Definition: BoolePolynomial.h:294
polybori::groebner::idx_type
polybori::CTypes::idx_type idx_type
Definition: groebner_defs.h:44
LiteralFactorization.h
polybori::groebner::LexBucket::getFront
Polynomial getFront()
Definition: LexBucket.h:68
polybori::groebner::without_prior_part
Polynomial without_prior_part(Polynomial p, idx_type tail_start)
Definition: LexBucket.cc:23