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