groebner_alg.h
Go to the documentation of this file.
/*
* groebner_alg.h
* PolyBoRi
*
* Created by Michael Brickenstein on 20.04.06.
* Copyright 2006 The PolyBoRi Team. See LICENSE file.
*
*/
#ifndef PBORI_GB_ALG_H
#define PBORI_GB_ALG_H
#include "PairStatusSet.h"
#include "PairManager.h"
#include "MonomialHasher.h"
#include "ReductionStrategy.h"
#include "GroebnerStrategy.h"
#include "LessWeightedLengthInStrat.h"
#include "LargerDegreeComparer.h"
#include "LessWeightedLengthInStratModified.h"
#include "LessEcartThenLessWeightedLengthInStrat.h"
#include "LessUsedTailVariablesThenLessWeightedLengthInStrat.h"
#include "LessCombinedManySizesInStrat.h"
#include <polybori.h>
#include "groebner_defs.h"
#include "pairs.h"
#include <boost/dynamic_bitset.hpp>
#include <vector>
#include <string>
#include <algorithm>
#include <utility>
#include <iostream>
#include "cache_manager.h"
#include "polynomial_properties.h"
BEGIN_NAMESPACE_PBORIGB
#define LL_RED_FOR_GROEBNER 1
Polynomial map_every_x_to_x_plus_one(Polynomial p);
MonomialSet mod_var_set(const MonomialSet& as, const MonomialSet& vs);
void groebner(GroebnerStrategy& strat);
Polynomial reduce_by_binom(const Polynomial& p, const Polynomial& binom);
Polynomial reduce_by_monom(const Polynomial& p, const Monomial& m);
Polynomial reduce_complete(const Polynomial& p, const Polynomial& reductor);
Polynomial mult_fast_sim(const std::vector<Polynomial>& vec,
const BoolePolyRing& ring);
std::vector<Polynomial> full_implication_gb(const Polynomial & p,CacheManager& cache,GroebnerStrategy& strat);
Polynomial reduce_complete(const Polynomial &p, const PolyEntry& reductor, wlen_type &len);
MonomialSet recursively_insert(MonomialSet::navigator p, idx_type idx, MonomialSet mset);
inline Polynomial
cancel_monomial_in_tail(const Polynomial& p, const Monomial & m){
Monomial lm=p.lead();
Polynomial res=reduce_by_monom(p,m);
if ((!res.isZero()) && (res.lead()==lm)){
return res;
} else {
return res+lm;
}
/*Polynomial tail=p-lm;
Monomial used_var=tail.usedVariables();
if (used_var.reducibleBy(m)){
tail=Polynomial(BooleSet(tail).diff(m.multiples(used_var)));
}
return tail+lm;*/
}
inline Polynomial
reduce_by_binom(const Polynomial& p, const Polynomial& binom){
PBORI_ASSERT(binom.length()==2);
Monomial bin_lead=binom.lead();
Monomial bin_last=*(++(binom.orderedBegin()));
MonomialSet dividing_terms=((MonomialSet)p).multiplesOf(bin_lead);
Monomial b_p_gcd=bin_last.GCD(bin_lead);
Monomial divide_by=bin_lead/b_p_gcd;
Monomial multiply_by=bin_last/b_p_gcd;
Polynomial rewritten=((Polynomial) dividing_terms)/divide_by;
return p-dividing_terms+rewritten*multiply_by;
}
inline Polynomial
reduce_by_binom_in_tail (const Polynomial& p, const Polynomial& binom){
PBORI_ASSERT(binom.length()==2);
Monomial lm=p.lead();
return lm+reduce_by_binom(p-lm,binom);
}
END_NAMESPACE_PBORIGB
#endif
LargerDegreeComparer.h
polynomial_properties.h
polybori::groebner::cancel_monomial_in_tail
Polynomial cancel_monomial_in_tail(const Polynomial &p, const Monomial &m)
Definition: groebner_alg.h:64
polybori::groebner::reduce_complete
Polynomial reduce_complete(const Polynomial &p, const PolyEntry &reductor, wlen_type &len)
Definition: groebner_alg.cc:234
polybori::BoolePolynomial::lead
monom_type lead() const
Get leading term.
Definition: BoolePolynomial.cc:225
polybori::BooleMonomial::GCD
self GCD(const self &) const
Compute the greatest common divisor.
Definition: BooleMonomial.cc:169
END_NAMESPACE_PBORIGB
#define END_NAMESPACE_PBORIGB
Definition: groebner_defs.h:16
LessCombinedManySizesInStrat.h
polybori::BooleSet::multiplesOf
self multiplesOf(const term_type &rhs) const
Compute intersection with multiples of rhs.
Definition: BooleSet.cc:171
LessUsedTailVariablesThenLessWeightedLengthInStrat.h
polybori::groebner::mod_var_set
MonomialSet mod_var_set(const MonomialSet &as, const MonomialSet &vs)
Definition: groebner_alg.cc:85
polybori::Polynomial
BoolePolynomial Polynomial
Definition: embed.h:51
BEGIN_NAMESPACE_PBORIGB
#define BEGIN_NAMESPACE_PBORIGB
Definition: groebner_defs.h:15
PairManager.h
polybori::BoolePolynomial
This class wraps the underlying decicion diagram type and defines the necessary operations.
Definition: BoolePolynomial.h:85
polybori::groebner::reduce_by_binom
Polynomial reduce_by_binom(const Polynomial &p, const Polynomial &binom)
Definition: groebner_alg.h:84
pairs.h
polybori::groebner::MonomialSet
polybori::BooleSet MonomialSet
Definition: groebner_defs.h:45
groebner_defs.h
LessWeightedLengthInStratModified.h
polybori::groebner::groebner
void groebner(GroebnerStrategy &strat)
polybori::groebner::map_every_x_to_x_plus_one
Polynomial map_every_x_to_x_plus_one(Polynomial p)
Definition: groebner_alg.cc:405
polybori::groebner::recursively_insert
MonomialSet recursively_insert(MonomialSet::navigator p, idx_type idx, MonomialSet mset)
Definition: groebner_alg.cc:368
PBORI_ASSERT
#define PBORI_ASSERT(arg)
Definition: pbori_defs.h:118
polybori::groebner::reduce_by_monom
Polynomial reduce_by_monom(const Polynomial &p, const Monomial &m)
assumes that divisibility condition is fullfilled
Definition: groebner_alg.cc:147
polybori::groebner::wlen_type
long wlen_type
Definition: groebner_defs.h:39
polybori::groebner::reduce_by_binom_in_tail
Polynomial reduce_by_binom_in_tail(const Polynomial &p, const Polynomial &binom)
Definition: groebner_alg.h:104
polybori::groebner::mult_fast_sim
Polynomial mult_fast_sim(const std::vector< Polynomial > &vec, const BoolePolyRing &ring)
Definition: groebner_alg.cc:417
polybori::BoolePolynomial::length
size_type length() const
Returns number of terms.
Definition: BoolePolynomial.cc:414
ReductionStrategy.h
PairStatusSet.h
LessEcartThenLessWeightedLengthInStrat.h
polybori.h
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
polybori::BooleSet
Definition: BooleSet.h:57
GroebnerStrategy.h
polybori::BooleMonomial
This class is just a wrapper for using variables from cudd's decicion diagram.
Definition: BooleMonomial.h:50
polybori::Monomial
BooleMonomial Monomial
Definition: embed.h:53
MonomialHasher.h
cache_manager.h
LessWeightedLengthInStrat.h
polybori::groebner::full_implication_gb
std::vector< Polynomial > full_implication_gb(const Polynomial &p, CacheManager &cache, GroebnerStrategy &strat)
Definition: groebner_alg.cc:458
polybori::BoolePolynomial::orderedBegin
ordered_iterator orderedBegin() const
Start of ordering respecting iterator.
Definition: BoolePolynomial.cc:491