GroebnerStrategy.h
Go to the documentation of this file.
// -*- c++ -*-
//*****************************************************************************
//*****************************************************************************
#ifndef polybori_groebner_GroebnerStrategy_h_
#define polybori_groebner_GroebnerStrategy_h_
// include basic definitions
#include "pairs.h"
#include "cache_manager.h"
#include "PairManagerFacade.h"
#include "ReductionStrategy.h"
#include "groebner_defs.h"
#include "PolyEntryPtrLmLess.h"
#include "GroebnerOptions.h"
#include <vector>
#include <boost/shared_ptr.hpp>
#include <polybori/routines/pbori_algo.h> // member-for_each etc.
BEGIN_NAMESPACE_PBORIGB
class GroebnerStrategy:
public GroebnerOptions, public PairManagerFacade<GroebnerStrategy> {
typedef GroebnerStrategy self;
public:
GroebnerStrategy(const GroebnerStrategy& orig);
GroebnerStrategy(const BoolePolyRing& input_ring):
GroebnerOptions(input_ring.ordering().isBlockOrder(),
!input_ring.ordering().isDegreeOrder()),
PairManagerFacade<GroebnerStrategy>(input_ring),
generators(input_ring),
cache(new CacheManager()),
chainCriterions(0), variableChainCriterions(0),
easyProductCriterions(0), extendedProductCriterions(0) { }
const BoolePolyRing& ring() const { return generators.leadingTerms.ring(); }
bool containsOne() const { return generators.leadingTerms.ownsOne(); }
std::vector<Polynomial> minimalizeAndTailReduce();
std::vector<Polynomial> minimalize();
void addGenerator(const PolyEntry& entry);
void addGeneratorDelayed(const BoolePolynomial & p);
void addAsYouWish(const Polynomial& p);
void addGeneratorTrySplit(const Polynomial& p, bool is_minimal);
bool variableHasValue(idx_type i);
void llReduceAll();
void treat_m_p_1_case(const PolyEntry& e) {
generators.monomials_plus_one.update(e);
}
Polynomial nextSpoly(){ return pairs.nextSpoly(generators); }
void addNonTrivialImplicationsDelayed(const PolyEntry& p);
void propagate(const PolyEntry& e);
void log(const char* c) const { if (enabledLog) std::cout<<c<<std::endl; }
Polynomial redTail(const Polynomial& p);
std::vector<Polynomial> noroStep(const std::vector<Polynomial>&);
std::vector<Polynomial> faugereStepDense(const std::vector<Polynomial>&);
Polynomial nf(Polynomial p) const;
void symmGB_F2();
int suggestPluginVariable();
std::vector<Polynomial> allGenerators();
bool checkSingletonCriterion(int i, int j) const {
return generators[i].isSingleton() && generators[j].isSingleton();
}
bool checkPairCriteria(const Exponent& lm, int i, int j) {
return checkSingletonCriterion(i, j) || checkExtendedProductCriterion(i, j)
|| checkChainCriterion(lm, i, j);
}
bool checkChainCriterion(const Exponent& lm, int i, int j);
bool checkExtendedProductCriterion(int i, int j);
bool checkVariableSingletonCriterion(int idx) const {
return generators[idx].isSingleton();
}
bool checkVariableLeadOfFactorCriterion(int idx, int var) const {
bool result = generators[idx].literal_factors.occursAsLeadOfFactor(var);
if (result)
log("delayed variable linear factor criterion");
return result;
}
bool checkVariableChainCriterion(int idx) {
bool result = !generators[idx].minimal;
if (result)
++variableChainCriterions;
return result;
}
bool checkVariableCriteria(int idx, int var) {
return PBORI_UNLIKELY(checkVariableSingletonCriterion(idx) ||
checkVariableLeadOfFactorCriterion(idx, var)) ||
checkVariableChainCriterion(idx);
}
protected:
std::vector<Polynomial> treatVariablePairs(PolyEntryReference);
void normalPairsWithLast(const MonomialSet&);
void addVariablePairs(PolyEntryReference);
std::vector<Polynomial> add4ImplDelayed(PolyEntryReference);
std::vector<Polynomial> add4ImplDelayed(const Polynomial& p, const Exponent& lm_exp,
const Exponent& used_variables) const;
std::vector<Polynomial> addHigherImplDelayedUsing4(PolyEntryReference);
std::vector<Polynomial> addHigherImplDelayedUsing4(const LiteralFactorization&) const;
private:
int addGeneratorStep(const PolyEntry&);
void addImplications(const BoolePolynomial& p, std::vector<int>& indices);
bool add4ImplDelayed(const Polynomial& p, const Exponent& lm_exp,
const Exponent& used_variables, bool include_orig,
std::vector<Polynomial>& impl) const;
bool addHigherImplDelayedUsing4(const LiteralFactorization&,
bool include_orig, std::vector<Polynomial>&) const;
template <class Iterator>
void addImplications(Iterator, Iterator, std::vector<int>& indices);
void addImplications(const std::vector<Polynomial>& impl, int s);
typedef std::set<const PolyEntry*, PolyEntryPtrLmLess> entryset_type;
void propagateStep(entryset_type& others);
void exchange(const Polynomial&, const PolyEntry&, entryset_type&);
void updatePropagated(const PolyEntry& entry);
// product criterion doesn't hold - try length 1 crit
void checkSingletonCriterion(const PolyEntry& entry,
const MonomialSet& intersection) {
PBORI_ASSERT(generators.checked_index(entry) == -1);
pairs.status.prolong(PairStatusSet::HAS_T_REP);
for_each(intersection.expBegin(), intersection.expEnd(), *this,
(entry.isSingleton()? &self::markNextSingleton:
&self::markNextUncalculated));
}
void checkCriteria(const PolyEntry& entry, const MonomialSet& terms) {
checkSingletonCriterion(entry, terms);
easyProductCriterions += generators.minimalLeadingTerms.length() -
terms.length();
}
void markNextSingleton(const Exponent& key) {
if (generators[key].isSingleton())
++extendedProductCriterions;
else
markNextUncalculated(key);
}
void markNextUncalculated(const BooleExponent& key) {
pairs.status.setToUncalculated(generators.index(key), generators.size());
}
bool shorterElimination(const MonomialSet& divisors, wlen_type el,
MonomialSet::deg_type deg) const;
public:
ReductionStrategy generators;
boost::shared_ptr<CacheManager> cache;
unsigned int reductionSteps;
int normalForms;
int currentDegree;
int averageLength;
int chainCriterions;
int variableChainCriterions;
int easyProductCriterions;
int extendedProductCriterions;
};
END_NAMESPACE_PBORIGB
#endif /* polybori_GroebnerStrategy_h_ */
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::groebner::GroebnerStrategy::treat_m_p_1_case
void treat_m_p_1_case(const PolyEntry &e)
Definition: GroebnerStrategy.h:74
polybori::groebner::Exponent
polybori::BooleExponent Exponent
Definition: groebner_defs.h:33
END_NAMESPACE_PBORIGB
#define END_NAMESPACE_PBORIGB
Definition: groebner_defs.h:16
polybori::groebner::LiteralFactorization
Definition: LiteralFactorization.h:24
polybori::groebner::deg_type
int deg_type
Definition: groebner_defs.h:42
polybori::BooleSet::expEnd
exp_iterator expEnd() const
Finish of iteration over exponent vectors.
Definition: BooleSet.cc:109
PolyEntryPtrLmLess.h
polybori::groebner::GroebnerStrategy::checkPairCriteria
bool checkPairCriteria(const Exponent &lm, int i, int j)
Definition: GroebnerStrategy.h:99
polybori::BoolePolyRing
This class reinterprets decicion diagram managers as Boolean polynomial rings, adds an ordering and v...
Definition: BoolePolyRing.h:40
PairManagerFacade.h
polybori::groebner::GroebnerStrategy::normalForms
int normalForms
Definition: GroebnerStrategy.h:208
BEGIN_NAMESPACE_PBORIGB
#define BEGIN_NAMESPACE_PBORIGB
Definition: groebner_defs.h:15
polybori::groebner::GroebnerOptions
This class defines options settings for GroebnerStrategy.
Definition: GroebnerOptions.h:32
polybori::BooleSet::expBegin
exp_iterator expBegin() const
Start of iteration over exponent vectors.
Definition: BooleSet.cc:101
polybori::groebner::PolyEntry
This class defines PolyEntry.
Definition: PolyEntry.h:32
polybori::groebner::GroebnerStrategy::variableChainCriterions
int variableChainCriterions
Definition: GroebnerStrategy.h:213
polybori::groebner::GroebnerStrategy::generators
ReductionStrategy generators
Definition: GroebnerStrategy.h:204
polybori::BoolePolynomial
This class wraps the underlying decicion diagram type and defines the necessary operations.
Definition: BoolePolynomial.h:85
pairs.h
polybori::groebner::MonomialSet
polybori::BooleSet MonomialSet
Definition: groebner_defs.h:45
groebner_defs.h
polybori::groebner::GroebnerStrategy::currentDegree
int currentDegree
Definition: GroebnerStrategy.h:209
polybori::groebner::GroebnerStrategy::checkSingletonCriterion
bool checkSingletonCriterion(int i, int j) const
Definition: GroebnerStrategy.h:95
polybori::groebner::GroebnerStrategy::averageLength
int averageLength
Definition: GroebnerStrategy.h:210
polybori::groebner::GroebnerStrategy::nextSpoly
Polynomial nextSpoly()
Definition: GroebnerStrategy.h:79
polybori::groebner::GroebnerStrategy::checkVariableChainCriterion
bool checkVariableChainCriterion(int idx)
Definition: GroebnerStrategy.h:119
polybori::groebner::PolyEntry::isSingleton
bool isSingleton() const
Definition: PolyEntry.h:67
polybori::groebner::GroebnerStrategy::containsOne
bool containsOne() const
Definition: GroebnerStrategy.h:61
polybori::groebner::CacheManager
Definition: cache_manager.h:28
polybori::groebner::GroebnerStrategy
This class defines GroebnerStrategy.
Definition: GroebnerStrategy.h:41
polybori::groebner::GroebnerStrategy::checkVariableSingletonCriterion
bool checkVariableSingletonCriterion(int idx) const
Definition: GroebnerStrategy.h:108
polybori::groebner::GroebnerStrategy::easyProductCriterions
int easyProductCriterions
Definition: GroebnerStrategy.h:214
PBORI_ASSERT
#define PBORI_ASSERT(arg)
Definition: pbori_defs.h:118
polybori::groebner::GroebnerStrategy::log
void log(const char *c) const
Definition: GroebnerStrategy.h:83
polybori::groebner::wlen_type
long wlen_type
Definition: groebner_defs.h:39
polybori::groebner::GroebnerStrategy::reductionSteps
unsigned int reductionSteps
Definition: GroebnerStrategy.h:207
polybori::groebner::PairManagerFacade
This class defines a facade for a given Strategy, which.
Definition: PairManagerFacade.h:79
ReductionStrategy.h
polybori::groebner::GroebnerStrategy::ring
const BoolePolyRing & ring() const
Definition: GroebnerStrategy.h:60
polybori::groebner::GroebnerStrategy::extendedProductCriterions
int extendedProductCriterions
Definition: GroebnerStrategy.h:215
polybori::groebner::GroebnerStrategy::chainCriterions
int chainCriterions
Definition: GroebnerStrategy.h:212
polybori::groebner::idx_type
polybori::CTypes::idx_type idx_type
Definition: groebner_defs.h:44
polybori::groebner::GroebnerStrategy::cache
boost::shared_ptr< CacheManager > cache
Definition: GroebnerStrategy.h:205
polybori::groebner::GroebnerStrategy::GroebnerStrategy
GroebnerStrategy(const BoolePolyRing &input_ring)
Construct from a ring.
Definition: GroebnerStrategy.h:50
GroebnerOptions.h
polybori::BooleSet
Definition: BooleSet.h:57
polybori::groebner::GroebnerStrategy::checkVariableCriteria
bool checkVariableCriteria(int idx, int var)
Definition: GroebnerStrategy.h:126
polybori::groebner::ReductionStrategy
This class defines ReductionStrategy.
Definition: ReductionStrategy.h:34
polybori::groebner::PolyEntryReference
This class defines PolyEntryReference.
Definition: PolyEntryReference.h:34
pbori_algo.h
PBORI_UNLIKELY
#define PBORI_UNLIKELY(expression)
Definition: pbori_defs.h:59
cache_manager.h
polybori::for_each
void for_each(InIter start, InIter finish, Object &obj, MemberFuncPtr func)
Definition: pbori_algo.h:857
polybori::groebner::GroebnerStrategy::checkVariableLeadOfFactorCriterion
bool checkVariableLeadOfFactorCriterion(int idx, int var) const
Definition: GroebnerStrategy.h:112