00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012 #include <polybori.h>
00013 #include "groebner_defs.h"
00014 #include "pairs.h"
00015 #include <boost/dynamic_bitset.hpp>
00016 #include <vector>
00017 #include <string>
00018 #include <algorithm>
00019 #include <utility>
00020 #include <iostream>
00021 #include "cache_manager.h"
00022 #include "polynomial_properties.h"
00023
00024 #ifndef PBORI_GB_ALG_H
00025 #define PBORI_GB_ALG_H
00026
00027
00028 BEGIN_NAMESPACE_PBORIGB
00029
00030 #define LL_RED_FOR_GROEBNER 1
00031 MonomialSet minimal_elements(const MonomialSet& s);
00032 Polynomial map_every_x_to_x_plus_one(Polynomial p);
00033 class PairStatusSet{
00034 public:
00035 typedef boost::dynamic_bitset<> bitvector_type;
00036 bool hasTRep(int ia, int ja) const {
00037 int i,j;
00038 i=std::min(ia,ja);
00039 j=std::max(ia,ja);
00040 return table[j][i]==HAS_T_REP;
00041 }
00042 void setToHasTRep(int ia, int ja){
00043 int i,j;
00044 i=std::min(ia,ja);
00045 j=std::max(ia,ja);
00046 table[j][i]=HAS_T_REP;
00047 }
00048 void setToUncalculated(int ia, int ja){
00049 int i,j;
00050 i=std::min(ia,ja);
00051 j=std::max(ia,ja);
00052 table[j][i]=UNCALCULATED;
00053 }
00054 void prolong(bool value=UNCALCULATED){
00055 int s=table.size();
00056 table.push_back(bitvector_type(s, value));
00057 }
00058 PairStatusSet(int size=0){
00059 int s=0;
00060 for(s=0;s<size;s++){
00061 prolong();
00062 }
00063 }
00064 static const bool HAS_T_REP=true;
00065 static const bool UNCALCULATED=false;
00066
00067 protected:
00068 std::vector<bitvector_type> table;
00069 };
00070 class GroebnerStrategy;
00071 class PairManager{
00072 public:
00073 PairStatusSet status;
00074 GroebnerStrategy* strat;
00075 PairManager(GroebnerStrategy & strat){
00076 this->strat=&strat;
00077 }
00078
00079 void appendHiddenGenerators(std::vector<Polynomial>& vec);
00080 typedef std::priority_queue<Pair,std::vector<PairE>, PairECompare> queue_type;
00081 queue_type queue;
00082 void introducePair(const Pair& p);
00083 Polynomial nextSpoly(const PolyEntryVector& gen);
00084 bool pairSetEmpty() const;
00085 void cleanTopByChainCriterion();
00086 protected:
00087 void replacePair(int& i, int & j);
00088 };
00089 class MonomialHasher{
00090 public:
00091 size_t operator() (const Monomial & m) const{
00092 return m.hash();
00093 }
00094 };
00095
00096 typedef Monomial::idx_map_type lm2Index_map_type;
00097 typedef Exponent::idx_map_type exp2Index_map_type;
00098 class ReductionStrategy:public PolyEntryVector{
00099 public:
00100 MonomialSet leadingTerms;
00101 MonomialSet minimalLeadingTerms;
00102 MonomialSet leadingTerms11;
00103 MonomialSet leadingTerms00;
00104 MonomialSet llReductor;
00105 MonomialSet monomials;
00106 MonomialSet monomials_plus_one;
00107 lm2Index_map_type lm2Index;
00108 exp2Index_map_type exp2Index;
00109 bool optBrutalReductions;
00110
00111 bool optLL;
00112
00113 Polynomial nf(Polynomial p) const;
00114 bool optRedTailDegGrowth;
00115 bool optRedTail;
00116 idx_type reducibleUntil;
00117 void setupSetsForLastElement();
00118 ReductionStrategy(){
00119 optLL=false;
00120 reducibleUntil=-1;
00121 optBrutalReductions=true;
00122 optRedTail=true;
00123 optRedTailDegGrowth=true;
00124 }
00125 bool canRewrite(const Polynomial& p) const{
00126 return is_rewriteable(p,minimalLeadingTerms);
00127 }
00128 void addGenerator(const Polynomial& p){
00129 push_back(p);
00130 setupSetsForLastElement();
00131 }
00132 int select1(const Polynomial& p) const;
00133 int select1(const Monomial& m) const;
00134
00135 int select_short(const Polynomial& p) const;
00136 int select_short(const Monomial& m) const;
00137 Polynomial headNormalForm(Polynomial p) const;
00138
00139 Polynomial reducedNormalForm(Polynomial p) const;
00140 };
00141 class GroebnerStrategy{
00142 public:
00143 bool containsOne() const{
00144 return generators.leadingTerms.ownsOne();
00145 }
00146
00147 GroebnerStrategy(const GroebnerStrategy& orig);
00148 std::vector<Polynomial> minimalizeAndTailReduce();
00149 std::vector<Polynomial> minimalize();
00150 int addGenerator(const BoolePolynomial& p, bool is_impl=false, std::vector<int>* impl_v=NULL);
00151 void addGeneratorDelayed(const BoolePolynomial & p);
00152 void addAsYouWish(const Polynomial& p);
00153 void addGeneratorTrySplit(const Polynomial& p, bool is_minimal);
00154 bool variableHasValue(idx_type i);
00155 void llReduceAll();
00156 void treat_m_p_1_case(const PolyEntry& e);
00157 PairManager pairs;
00158 bool reduceByTailReduced;
00159 ReductionStrategy generators;
00160 bool optDrawMatrices;
00161 std::string matrixPrefix;
00162
00163 boost::shared_ptr<CacheManager> cache;
00164 BoolePolyRing r;
00165 bool enabledLog;
00166 unsigned int reductionSteps;
00167 int normalForms;
00168 int currentDegree;
00169 int chainCriterions;
00170 int variableChainCriterions;
00171 int easyProductCriterions;
00172 int extendedProductCriterions;
00173 int averageLength;
00174
00175 bool optHFE;
00176 bool optLazy;
00177 bool optModifiedLinearAlgebra;
00178 bool optDelayNonMinimals;
00179
00180 bool optExchange;
00181 bool optAllowRecursion;
00182
00183 bool optStepBounded;
00184 bool optLinearAlgebraInLastBlock;
00185 bool optRedTailInLastBlock;
00186
00187
00188 GroebnerStrategy():r(BooleEnv::ring()),pairs(*this),cache(new CacheManager()){
00189 optDrawMatrices=false;
00190 optModifiedLinearAlgebra=false;
00191 matrixPrefix="mat";
00192 optDelayNonMinimals=true;
00193
00194 chainCriterions=0;
00195 enabledLog=false;
00196
00197
00198
00199
00200
00201 variableChainCriterions=0;
00202 extendedProductCriterions=0;
00203 easyProductCriterions=0;
00204
00205 optExchange=true;
00206 optHFE=false;
00207 optStepBounded=false;
00208 optAllowRecursion=true;
00209 optLinearAlgebraInLastBlock=true;
00210 if (BooleEnv::ordering().isBlockOrder())
00211 optRedTailInLastBlock=true;
00212 else
00213 optRedTailInLastBlock=false;
00214
00215 if (BooleEnv::ordering().isDegreeOrder())
00216 optLazy=false;
00217 else
00218 optLazy=true;
00219 reduceByTailReduced=false;
00220 generators.llReductor=Polynomial(1).diagram();
00221 }
00222
00223 Polynomial nextSpoly(){
00224 return pairs.nextSpoly(generators);
00225 }
00226 void addNonTrivialImplicationsDelayed(const PolyEntry& p);
00227 void propagate(const PolyEntry& e);
00228 void propagate_step(const PolyEntry& e, std::set<int> others);
00229 void log(const char* c){
00230 if (this->enabledLog)
00231 std::cout<<c<<endl;
00232 }
00233
00234 Polynomial redTail(const Polynomial& p);
00235 std::vector<Polynomial> noroStep(const std::vector<Polynomial>&);
00236 std::vector<Polynomial> faugereStepDense(const std::vector<Polynomial>&);
00237
00238 Polynomial nf(Polynomial p) const;
00239 void symmGB_F2();
00240 int suggestPluginVariable();
00241 std::vector<Polynomial> allGenerators();
00242 protected:
00243 std::vector<Polynomial> treatVariablePairs(int s);
00244 void treatNormalPairs(int s,MonomialSet intersecting_terms,MonomialSet other_terms, MonomialSet ext_prod_terms);
00245 void addVariablePairs(int s);
00246 std::vector<Polynomial> add4ImplDelayed(const Polynomial& p, const Exponent& lm_exp, const Exponent& used_variables,int s, bool include_orig);
00247 std::vector<Polynomial> addHigherImplDelayedUsing4(int s, const LiteralFactorization& literal_factors, bool include_orig);
00248
00249
00250 };
00251 MonomialSet mod_var_set(const MonomialSet& as, const MonomialSet& vs);
00252 void groebner(GroebnerStrategy& strat);
00253 Polynomial reduce_by_binom(const Polynomial& p, const Polynomial& binom);
00254 Polynomial reduce_by_monom(const Polynomial& p, const Monomial& m);
00255 Polynomial reduce_complete(const Polynomial& p, const Polynomial& reductor);
00256 class LessWeightedLengthInStrat{
00257 public:
00258 const ReductionStrategy* strat;
00259 LessWeightedLengthInStrat(const ReductionStrategy& strat){
00260 this->strat=&strat;
00261 }
00262 bool operator() (const Monomial& a , const Monomial& b){
00263 return (*strat)[strat->lm2Index.find(a)->second].weightedLength<(*strat)[strat->lm2Index.find(b)->second].weightedLength;
00264
00265 }
00266 bool operator() (const Exponent& a , const Exponent& b){
00267 return (*strat)[strat->exp2Index.find(a)->second].weightedLength<(*strat)[strat->exp2Index.find(b)->second].weightedLength;
00268
00269 }
00270 };
00271
00272 inline wlen_type wlen_literal_exceptioned(const PolyEntry& e){
00273 wlen_type res=e.weightedLength;
00274 if ((e.deg==1) && (e.length<=4)){
00275
00276
00277 return res-1;
00278 }
00279 return res;
00280 }
00282 class LessWeightedLengthInStratModified{
00283 public:
00284 const ReductionStrategy* strat;
00285 LessWeightedLengthInStratModified(const ReductionStrategy& strat){
00286 this->strat=&strat;
00287 }
00288 bool operator() (const Monomial& a , const Monomial& b){
00289 wlen_type wa=wlen_literal_exceptioned((*strat)[strat->lm2Index.find(a)->second]);
00290 wlen_type wb=wlen_literal_exceptioned((*strat)[strat->lm2Index.find(b)->second]);
00291
00292 return wa<wb;
00293
00294 }
00295 bool operator() (const Exponent& a , const Exponent& b){
00296 wlen_type wa=wlen_literal_exceptioned((*strat)[strat->exp2Index.find(a)->second]);
00297 wlen_type wb=wlen_literal_exceptioned((*strat)[strat->exp2Index.find(b)->second]);
00298
00299 return wa<wb;
00300
00301 }
00302 };
00303 class LessEcartThenLessWeightedLengthInStrat{
00304 public:
00305 const GroebnerStrategy* strat;
00306 LessEcartThenLessWeightedLengthInStrat(const GroebnerStrategy& strat){
00307 this->strat=&strat;
00308 }
00309 bool operator() (const Monomial& a , const Monomial& b){
00310 int i=strat->generators.lm2Index.find(a)->second;
00311 int j=strat->generators.lm2Index.find(b)->second;
00312 if (strat->generators[i].ecart()!=strat->generators[j].ecart()){
00313 if (strat->generators[i].ecart()<strat->generators[j].ecart())
00314 return true;
00315 else
00316 return false;
00317 }
00318 return (strat->generators[i].weightedLength<strat->generators[j].weightedLength);
00319
00320 }
00321
00322 bool operator() (const Exponent& a , const Exponent& b){
00323 int i=strat->generators.exp2Index.find(a)->second;
00324 int j=strat->generators.exp2Index.find(b)->second;
00325 if (strat->generators[i].ecart()!=strat->generators[j].ecart()){
00326 if (strat->generators[i].ecart()<strat->generators[j].ecart())
00327 return true;
00328 else
00329 return false;
00330 }
00331 return (strat->generators[i].weightedLength<strat->generators[j].weightedLength);
00332
00333 }
00334 };
00335 class LessUsedTailVariablesThenLessWeightedLengthInStrat{
00336 public:
00337 const GroebnerStrategy* strat;
00338 LessUsedTailVariablesThenLessWeightedLengthInStrat(const GroebnerStrategy& strat){
00339 this->strat=&strat;
00340 }
00341 bool operator() (const Monomial& a , const Monomial& b) const{
00342 int i=strat->generators.lm2Index.find(a)->second;
00343 int j=strat->generators.lm2Index.find(b)->second;
00344 deg_type d1=strat->generators[i].tailVariables.deg();
00345 deg_type d2=strat->generators[j].tailVariables.deg();;
00346 if (d1!=d2){
00347 return (d1<d2);
00348 }
00349 return (strat->generators[i].weightedLength<strat->generators[j].weightedLength);
00350
00351 }
00352 };
00353
00354 class LessCombinedManySizesInStrat{
00355 public:
00356 GroebnerStrategy* strat;
00357 LessCombinedManySizesInStrat(GroebnerStrategy& strat){
00358 this->strat=&strat;
00359 }
00360 bool operator() (const Monomial& a , const Monomial& b){
00361 int i=strat->generators.lm2Index[a];
00362 int j=strat->generators.lm2Index[b];
00363 deg_type d1=strat->generators[i].tailVariables.deg();
00364 deg_type d2=strat->generators[j].tailVariables.deg();
00365 wlen_type w1=d1;
00366 wlen_type w2=d2;
00367 w1*=strat->generators[i].length;
00368 w1*=strat->generators[i].ecart();
00369 w2*=strat->generators[j].length;
00370 w2*=strat->generators[j].ecart();
00371 return w1<w2;
00372
00373
00374 }
00375 };
00376
00377
00378 Polynomial mult_fast_sim(const std::vector<Polynomial>& vec);
00379 std::vector<Polynomial> full_implication_gb(const Polynomial & p,CacheManager& cache,GroebnerStrategy& strat);
00380 Polynomial reduce_complete(const Polynomial &p, const PolyEntry& reductor, wlen_type &len);
00381 MonomialSet contained_variables_cudd_style(const MonomialSet& m);
00382 MonomialSet minimal_elements_cudd_style(MonomialSet m);
00383 MonomialSet recursively_insert(MonomialSet::navigator p, idx_type idx, MonomialSet mset);
00384 MonomialSet minimal_elements_cudd_style_unary(MonomialSet m);
00385 END_NAMESPACE_PBORIGB
00386
00387 #endif
00388