PolyBoRi
|
00001 /* 00002 * groebner_alg.h 00003 * PolyBoRi 00004 * 00005 * Created by Michael Brickenstein on 20.04.06. 00006 * Copyright 2006 The PolyBoRi Team. See LICENSE file. 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 00119 ReductionStrategy(){ set_defaults(); } 00120 00121 ReductionStrategy(const BoolePolyRing& theRing): 00122 leadingTerms(theRing.zero()), minimalLeadingTerms(theRing.zero()), 00123 leadingTerms11(theRing.zero()), leadingTerms00(theRing.zero()), llReductor(theRing.zero()), 00124 monomials(theRing.zero()), monomials_plus_one(theRing.zero()), lm2Index(), 00125 exp2Index() { 00126 set_defaults(); 00127 } 00128 00129 bool canRewrite(const Polynomial& p) const{ 00130 return is_rewriteable(p,minimalLeadingTerms); 00131 } 00132 void addGenerator(const Polynomial& p){ 00133 push_back(p); 00134 setupSetsForLastElement(); 00135 } 00136 int select1(const Polynomial& p) const; 00137 int select1(const Monomial& m) const; 00138 00139 int select_short(const Polynomial& p) const; 00140 int select_short(const Monomial& m) const; 00141 Polynomial headNormalForm(Polynomial p) const; 00142 00143 Polynomial reducedNormalForm(Polynomial p) const; 00144 00145 protected: 00146 void set_defaults(){ 00147 optLL=false; 00148 reducibleUntil=-1; 00149 optBrutalReductions=true; 00150 optRedTail=true; 00151 optRedTailDegGrowth=true; 00152 } 00153 }; 00154 class GroebnerStrategy{ 00155 public: 00156 bool containsOne() const{ 00157 return generators.leadingTerms.ownsOne(); 00158 } 00159 00160 GroebnerStrategy(const GroebnerStrategy& orig); 00161 std::vector<Polynomial> minimalizeAndTailReduce(); 00162 std::vector<Polynomial> minimalize(); 00163 int addGenerator(const BoolePolynomial& p, bool is_impl=false, std::vector<int>* impl_v=NULL); 00164 void addGeneratorDelayed(const BoolePolynomial & p); 00165 void addAsYouWish(const Polynomial& p); 00166 void addGeneratorTrySplit(const Polynomial& p, bool is_minimal); 00167 bool variableHasValue(idx_type i); 00168 void llReduceAll(); 00169 void treat_m_p_1_case(const PolyEntry& e); 00170 PairManager pairs; 00171 bool reduceByTailReduced; 00172 ReductionStrategy generators; 00173 bool optDrawMatrices; 00174 std::string matrixPrefix; 00175 //const char* matrixPrefix; 00176 boost::shared_ptr<CacheManager> cache; 00177 BoolePolyRing r; 00178 bool enabledLog; 00179 unsigned int reductionSteps; 00180 int normalForms; 00181 int currentDegree; 00182 int chainCriterions; 00183 int variableChainCriterions; 00184 int easyProductCriterions; 00185 int extendedProductCriterions; 00186 int averageLength; 00187 00188 bool optHFE; 00189 bool optLazy; 00190 bool optModifiedLinearAlgebra; 00191 bool optDelayNonMinimals; 00192 00193 bool optExchange; 00194 bool optAllowRecursion; 00195 00196 bool optStepBounded; 00197 bool optLinearAlgebraInLastBlock; 00198 bool optRedTailInLastBlock; 00199 00200 00201 GroebnerStrategy():r(BooleEnv::ring()),pairs(*this),cache(new CacheManager()){ 00202 optDrawMatrices=false; 00203 optModifiedLinearAlgebra=false; 00204 matrixPrefix="mat"; 00205 optDelayNonMinimals=true; 00206 00207 chainCriterions=0; 00208 enabledLog=false; 00209 00210 //if (BooleEnv::ordering().isDegreeOrder()) 00211 // optBrutalReductions=false; 00212 //else 00213 00214 variableChainCriterions=0; 00215 extendedProductCriterions=0; 00216 easyProductCriterions=0; 00217 00218 optExchange=true; 00219 optHFE=false; 00220 optStepBounded=false; 00221 optAllowRecursion=true; 00222 optLinearAlgebraInLastBlock=true; 00223 if (BooleEnv::ordering().isBlockOrder()) 00224 optRedTailInLastBlock=true; 00225 else 00226 optRedTailInLastBlock=false; 00227 00228 if (BooleEnv::ordering().isDegreeOrder()) 00229 optLazy=false; 00230 else 00231 optLazy=true; 00232 reduceByTailReduced=false; 00233 generators.llReductor=Polynomial(1).diagram(); // todo: is this unsafe? 00234 } 00235 00236 Polynomial nextSpoly(){ 00237 return pairs.nextSpoly(generators); 00238 } 00239 void addNonTrivialImplicationsDelayed(const PolyEntry& p); 00240 void propagate(const PolyEntry& e); 00241 void propagate_step(const PolyEntry& e, std::set<int> others); 00242 void log(const char* c){ 00243 if (this->enabledLog) 00244 std::cout<<c<<std::endl; 00245 } 00246 00247 Polynomial redTail(const Polynomial& p); 00248 std::vector<Polynomial> noroStep(const std::vector<Polynomial>&); 00249 std::vector<Polynomial> faugereStepDense(const std::vector<Polynomial>&); 00250 //std::vector<Polynomial> faugereStepDenseModified(const std::vector<Polynomial>&); 00251 Polynomial nf(Polynomial p) const; 00252 void symmGB_F2(); 00253 int suggestPluginVariable(); 00254 std::vector<Polynomial> allGenerators(); 00255 protected: 00256 std::vector<Polynomial> treatVariablePairs(int s); 00257 void treatNormalPairs(int s,MonomialSet intersecting_terms,MonomialSet other_terms, MonomialSet ext_prod_terms); 00258 void addVariablePairs(int s); 00259 std::vector<Polynomial> add4ImplDelayed(const Polynomial& p, const Exponent& lm_exp, const Exponent& used_variables,int s, bool include_orig); 00260 std::vector<Polynomial> addHigherImplDelayedUsing4(int s, const LiteralFactorization& literal_factors, bool include_orig); 00261 00262 00263 }; 00264 MonomialSet mod_var_set(const MonomialSet& as, const MonomialSet& vs); 00265 void groebner(GroebnerStrategy& strat); 00266 Polynomial reduce_by_binom(const Polynomial& p, const Polynomial& binom); 00267 Polynomial reduce_by_monom(const Polynomial& p, const Monomial& m); 00268 Polynomial reduce_complete(const Polynomial& p, const Polynomial& reductor); 00269 class LessWeightedLengthInStrat{ 00270 public: 00271 const ReductionStrategy* strat; 00272 LessWeightedLengthInStrat(const ReductionStrategy& strat){ 00273 this->strat=&strat; 00274 } 00275 bool operator() (const Monomial& a , const Monomial& b){ 00276 return (*strat)[strat->lm2Index.find(a)->second].weightedLength<(*strat)[strat->lm2Index.find(b)->second].weightedLength; 00277 00278 } 00279 bool operator() (const Exponent& a , const Exponent& b){ 00280 return (*strat)[strat->exp2Index.find(a)->second].weightedLength<(*strat)[strat->exp2Index.find(b)->second].weightedLength; 00281 00282 } 00283 }; 00284 00285 00286 class LargerDegreeComparer{ 00287 public: 00288 bool operator() (const Monomial& a , const Monomial& b){ 00289 return a.deg() > b.deg(); 00290 00291 } 00292 bool operator() (const Exponent& a , const Exponent& b){ 00293 return a.deg()>b.deg(); 00294 00295 } 00296 }; 00297 00298 inline wlen_type wlen_literal_exceptioned(const PolyEntry& e){ 00299 wlen_type res=e.weightedLength; 00300 if ((e.deg==1) && (e.length<=4)){ 00301 //if (e.length==1) return -1; 00302 //if (e.p.hasConstantPart()) return 0; 00303 return res-1; 00304 } 00305 return res; 00306 } 00308 class LessWeightedLengthInStratModified{ 00309 public: 00310 const ReductionStrategy* strat; 00311 LessWeightedLengthInStratModified(const ReductionStrategy& strat){ 00312 this->strat=&strat; 00313 } 00314 bool operator() (const Monomial& a , const Monomial& b){ 00315 wlen_type wa=wlen_literal_exceptioned((*strat)[strat->lm2Index.find(a)->second]); 00316 wlen_type wb=wlen_literal_exceptioned((*strat)[strat->lm2Index.find(b)->second]); 00317 00318 return wa<wb; 00319 00320 } 00321 bool operator() (const Exponent& a , const Exponent& b){ 00322 wlen_type wa=wlen_literal_exceptioned((*strat)[strat->exp2Index.find(a)->second]); 00323 wlen_type wb=wlen_literal_exceptioned((*strat)[strat->exp2Index.find(b)->second]); 00324 00325 return wa<wb; 00326 00327 } 00328 }; 00329 class LessEcartThenLessWeightedLengthInStrat{ 00330 public: 00331 const GroebnerStrategy* strat; 00332 LessEcartThenLessWeightedLengthInStrat(const GroebnerStrategy& strat){ 00333 this->strat=&strat; 00334 } 00335 bool operator() (const Monomial& a , const Monomial& b){ 00336 int i=strat->generators.lm2Index.find(a)->second; 00337 int j=strat->generators.lm2Index.find(b)->second; 00338 if (strat->generators[i].ecart()!=strat->generators[j].ecart()){ 00339 if (strat->generators[i].ecart()<strat->generators[j].ecart()) 00340 return true; 00341 else 00342 return false; 00343 } 00344 return (strat->generators[i].weightedLength<strat->generators[j].weightedLength); 00345 00346 } 00347 00348 bool operator() (const Exponent& a , const Exponent& b){ 00349 int i=strat->generators.exp2Index.find(a)->second; 00350 int j=strat->generators.exp2Index.find(b)->second; 00351 if (strat->generators[i].ecart()!=strat->generators[j].ecart()){ 00352 if (strat->generators[i].ecart()<strat->generators[j].ecart()) 00353 return true; 00354 else 00355 return false; 00356 } 00357 return (strat->generators[i].weightedLength<strat->generators[j].weightedLength); 00358 00359 } 00360 }; 00361 class LessUsedTailVariablesThenLessWeightedLengthInStrat{ 00362 public: 00363 const GroebnerStrategy* strat; 00364 LessUsedTailVariablesThenLessWeightedLengthInStrat(const GroebnerStrategy& strat){ 00365 this->strat=&strat; 00366 } 00367 bool operator() (const Monomial& a , const Monomial& b) const{ 00368 int i=strat->generators.lm2Index.find(a)->second; 00369 int j=strat->generators.lm2Index.find(b)->second; 00370 deg_type d1=strat->generators[i].tailVariables.deg(); 00371 deg_type d2=strat->generators[j].tailVariables.deg();; 00372 if (d1!=d2){ 00373 return (d1<d2); 00374 } 00375 return (strat->generators[i].weightedLength<strat->generators[j].weightedLength); 00376 00377 } 00378 }; 00379 00380 class LessCombinedManySizesInStrat{ 00381 public: 00382 GroebnerStrategy* strat; 00383 LessCombinedManySizesInStrat(GroebnerStrategy& strat){ 00384 this->strat=&strat; 00385 } 00386 bool operator() (const Monomial& a , const Monomial& b){ 00387 int i=strat->generators.lm2Index[a]; 00388 int j=strat->generators.lm2Index[b]; 00389 deg_type d1=strat->generators[i].tailVariables.deg(); 00390 deg_type d2=strat->generators[j].tailVariables.deg(); 00391 wlen_type w1=d1; 00392 wlen_type w2=d2; 00393 w1*=strat->generators[i].length; 00394 w1*=strat->generators[i].ecart(); 00395 w2*=strat->generators[j].length; 00396 w2*=strat->generators[j].ecart(); 00397 return w1<w2; 00398 00399 00400 } 00401 }; 00402 00403 00404 Polynomial mult_fast_sim(const std::vector<Polynomial>& vec); 00405 std::vector<Polynomial> full_implication_gb(const Polynomial & p,CacheManager& cache,GroebnerStrategy& strat); 00406 Polynomial reduce_complete(const Polynomial &p, const PolyEntry& reductor, wlen_type &len); 00407 MonomialSet contained_variables_cudd_style(const MonomialSet& m); 00408 MonomialSet minimal_elements_cudd_style(MonomialSet m); 00409 MonomialSet recursively_insert(MonomialSet::navigator p, idx_type idx, MonomialSet mset); 00410 MonomialSet minimal_elements_cudd_style_unary(MonomialSet m); 00411 END_NAMESPACE_PBORIGB 00412 00413 #endif 00414