15 #include <boost/dynamic_bitset.hpp>
23 #include <ext/hash_map>
30 #ifndef PBORI_GB_ALG_H
31 #define PBORI_GB_ALG_H
36 #define LL_RED_FOR_GROEBNER 1
46 return table[j][i]==HAS_T_REP;
52 table[j][i]=HAS_T_REP;
58 table[j][i]=UNCALCULATED;
70 static const bool HAS_T_REP=
true;
71 static const bool UNCALCULATED=
false;
74 std::vector<bitvector_type>
table;
85 void appendHiddenGenerators(std::vector<Polynomial>& vec);
88 void introducePair(
const Pair& p);
90 bool pairSetEmpty()
const;
91 void cleanTopByChainCriterion();
93 void replacePair(
int& i,
int & j);
115 return leadingTerms.ownsOne();
119 std::vector<Polynomial> minimalizeAndTailReduce();
120 std::vector<Polynomial> minimalize();
121 int addGenerator(
const BoolePolynomial& p,
bool is_impl=
false, std::vector<int>* impl_v=NULL);
124 void addGeneratorTrySplit(
const Polynomial& p,
bool is_minimal);
127 void treat_m_p_1_case(
const PolyEntry& e);
138 boost::shared_ptr<CacheManager>
cache;
165 optDelayNonMinimals=
true;
166 optRedTailDegGrowth=
true;
173 optBrutalReductions=
true;
174 variableChainCriterions=0;
175 extendedProductCriterions=0;
176 easyProductCriterions=0;
179 optStepBounded=
false;
180 optAllowRecursion=
true;
181 optLinearAlgebraInLastBlock=
true;
182 if (BooleEnv::ordering().isBlockOrder())
183 optRedTailInLastBlock=
true;
185 optRedTailInLastBlock=
false;
187 if (BooleEnv::ordering().isDegreeOrder())
191 reduceByTailReduced=
false;
196 return pairs.nextSpoly(generators);
198 void addNonTrivialImplicationsDelayed(
const PolyEntry& p);
200 void propagate_step(
const PolyEntry& e, std::set<int> others);
202 if (this->enabledLog)
209 std::vector<Polynomial> noroStep(
const std::vector<Polynomial>&);
210 std::vector<Polynomial> faugereStepDense(
const std::vector<Polynomial>&);
214 int suggestPluginVariable();
215 std::vector<Polynomial> allGenerators();
217 std::vector<Polynomial> treatVariablePairs(
int s);
219 void addVariablePairs(
int s);
220 std::vector<Polynomial> add4ImplDelayed(
const Polynomial& p,
const Exponent& lm_exp,
const Exponent& used_variables,
int s,
bool include_orig);
221 std::vector<Polynomial> addHigherImplDelayedUsing4(
int s,
const LiteralFactorization& literal_factors,
bool include_orig);
226 void groebner(GroebnerStrategy& strat);
237 return strat->
generators[strat->lm2Index.find(a)->second].weightedLength<strat->generators[strat->lm2Index.find(b)->second].weightedLength;
241 return strat->generators[strat->exp2Index.find(a)->second].weightedLength<strat->generators[strat->exp2Index.find(b)->second].weightedLength;
284 int i=strat->
lm2Index.find(a)->second;
285 int j=strat->lm2Index.find(b)->second;
286 if (strat->generators[i].ecart()!=strat->generators[j].ecart()){
287 if (strat->generators[i].ecart()<strat->generators[j].ecart())
292 return (strat->generators[i].weightedLength<strat->generators[j].weightedLength);
297 int i=strat->exp2Index.find(a)->second;
298 int j=strat->exp2Index.find(b)->second;
299 if (strat->generators[i].ecart()!=strat->generators[j].ecart()){
300 if (strat->generators[i].ecart()<strat->generators[j].ecart())
305 return (strat->generators[i].weightedLength<strat->generators[j].weightedLength);
316 int i=strat->
lm2Index.find(a)->second;
317 int j=strat->lm2Index.find(b)->second;
318 deg_type d1=strat->generators[i].tailVariables.deg();
319 deg_type d2=strat->generators[j].tailVariables.deg();;
323 return (strat->generators[i].weightedLength<strat->generators[j].weightedLength);
336 int j=strat->lm2Index[b];
337 deg_type d1=strat->generators[i].tailVariables.deg();
338 deg_type d2=strat->generators[j].tailVariables.deg();
341 w1*=strat->generators[i].length;
342 w1*=strat->generators[i].ecart();
343 w2*=strat->generators[j].length;
344 w2*=strat->generators[j].ecart();