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 optLazy; 00151 bool optLL; 00152 bool optDelayNonMinimals; 00153 bool optBrutalReductions; 00154 bool optExchange; 00155 bool optAllowRecursion; 00156 bool optRedTailDegGrowth; 00157 bool optStepBounded; 00158 bool optLinearAlgebraInLastBlock; 00159 bool optRedTailInLastBlock; 00160 lm2Index_map_type lm2Index; 00161 exp2Index_map_type exp2Index; 00162 00163 GroebnerStrategy():r(BooleEnv::ring()),pairs(*this),cache(new CacheManager()){ 00164 reducibleUntil=-1; 00165 optDelayNonMinimals=true; 00166 optRedTailDegGrowth=true; 00167 chainCriterions=0; 00168 enabledLog=false; 00169 optLL=false; 00170 //if (BooleEnv::ordering().isDegreeOrder()) 00171 // optBrutalReductions=false; 00172 //else 00173 optBrutalReductions=true; 00174 variableChainCriterions=0; 00175 extendedProductCriterions=0; 00176 easyProductCriterions=0; 00177 optRedTail=true; 00178 optExchange=true; 00179 optStepBounded=false; 00180 optAllowRecursion=true; 00181 optLinearAlgebraInLastBlock=true; 00182 if (BooleEnv::ordering().isBlockOrder()) 00183 optRedTailInLastBlock=true; 00184 else 00185 optRedTailInLastBlock=false; 00186 00187 if (BooleEnv::ordering().isDegreeOrder()) 00188 optLazy=false; 00189 else 00190 optLazy=true; 00191 reduceByTailReduced=false; 00192 llReductor=Polynomial(1).diagram(); // todo: is this unsafe? 00193 } 00194 00195 Polynomial nextSpoly(){ 00196 return pairs.nextSpoly(generators); 00197 } 00198 void addNonTrivialImplicationsDelayed(const PolyEntry& p); 00199 void propagate(const PolyEntry& e); 00200 void propagate_step(const PolyEntry& e, std::set<int> others); 00201 void log(const char* c){ 00202 if (this->enabledLog) 00203 std::cout<<c<<endl; 00204 } 00205 bool canRewrite(const Polynomial& p) const{ 00206 return is_rewriteable(p,minimalLeadingTerms); 00207 } 00208 Polynomial redTail(const Polynomial& p); 00209 std::vector<Polynomial> noroStep(const std::vector<Polynomial>&); 00210 std::vector<Polynomial> faugereStepDense(const std::vector<Polynomial>&); 00211 //std::vector<Polynomial> faugereStepDenseModified(const std::vector<Polynomial>&); 00212 Polynomial nf(Polynomial p) const; 00213 void symmGB_F2(); 00214 int suggestPluginVariable(); 00215 std::vector<Polynomial> allGenerators(); 00216 protected: 00217 std::vector<Polynomial> treatVariablePairs(int s); 00218 void treatNormalPairs(int s,MonomialSet intersecting_terms,MonomialSet other_terms, MonomialSet ext_prod_terms); 00219 void addVariablePairs(int s); 00220 std::vector<Polynomial> add4ImplDelayed(const Polynomial& p, const Exponent& lm_exp, const Exponent& used_variables,int s, bool include_orig); 00221 std::vector<Polynomial> addHigherImplDelayedUsing4(int s, const LiteralFactorization& literal_factors, bool include_orig); 00222 00223 00224 }; 00225 MonomialSet mod_var_set(const MonomialSet& as, const MonomialSet& vs); 00226 void groebner(GroebnerStrategy& strat); 00227 Polynomial reduce_by_binom(const Polynomial& p, const Polynomial& binom); 00228 Polynomial reduce_by_monom(const Polynomial& p, const Monomial& m); 00229 Polynomial reduce_complete(const Polynomial& p, const Polynomial& reductor); 00230 class LessWeightedLengthInStrat{ 00231 public: 00232 const GroebnerStrategy* strat; 00233 LessWeightedLengthInStrat(const GroebnerStrategy& strat){ 00234 this->strat=&strat; 00235 } 00236 bool operator() (const Monomial& a , const Monomial& b){ 00237 return strat->generators[strat->lm2Index.find(a)->second].weightedLength<strat->generators[strat->lm2Index.find(b)->second].weightedLength; 00238 00239 } 00240 bool operator() (const Exponent& a , const Exponent& b){ 00241 return strat->generators[strat->exp2Index.find(a)->second].weightedLength<strat->generators[strat->exp2Index.find(b)->second].weightedLength; 00242 00243 } 00244 }; 00245 00246 inline wlen_type wlen_literal_exceptioned(const PolyEntry& e){ 00247 wlen_type res=e.weightedLength; 00248 if ((e.deg==1) && (e.length<=4)){ 00249 //if (e.length==1) return -1; 00250 //if (e.p.hasConstantPart()) return 0; 00251 return res-1; 00252 } 00253 return res; 00254 } 00256 class LessWeightedLengthInStratModified{ 00257 public: 00258 const GroebnerStrategy* strat; 00259 LessWeightedLengthInStratModified(const GroebnerStrategy& strat){ 00260 this->strat=&strat; 00261 } 00262 bool operator() (const Monomial& a , const Monomial& b){ 00263 wlen_type wa=wlen_literal_exceptioned(strat->generators[strat->lm2Index.find(a)->second]); 00264 wlen_type wb=wlen_literal_exceptioned(strat->generators[strat->lm2Index.find(b)->second]); 00265 00266 return wa<wb; 00267 00268 } 00269 bool operator() (const Exponent& a , const Exponent& b){ 00270 wlen_type wa=wlen_literal_exceptioned(strat->generators[strat->exp2Index.find(a)->second]); 00271 wlen_type wb=wlen_literal_exceptioned(strat->generators[strat->exp2Index.find(b)->second]); 00272 00273 return wa<wb; 00274 00275 } 00276 }; 00277 class LessEcartThenLessWeightedLengthInStrat{ 00278 public: 00279 const GroebnerStrategy* strat; 00280 LessEcartThenLessWeightedLengthInStrat(const GroebnerStrategy& strat){ 00281 this->strat=&strat; 00282 } 00283 bool operator() (const Monomial& a , const Monomial& b){ 00284 int i=strat->lm2Index.find(a)->second; 00285 int j=strat->lm2Index.find(b)->second; 00286 if (strat->generators[i].ecart()!=strat->generators[j].ecart()){ 00287 if (strat->generators[i].ecart()<strat->generators[j].ecart()) 00288 return true; 00289 else 00290 return false; 00291 } 00292 return (strat->generators[i].weightedLength<strat->generators[j].weightedLength); 00293 00294 } 00295 00296 bool operator() (const Exponent& a , const Exponent& b){ 00297 int i=strat->exp2Index.find(a)->second; 00298 int j=strat->exp2Index.find(b)->second; 00299 if (strat->generators[i].ecart()!=strat->generators[j].ecart()){ 00300 if (strat->generators[i].ecart()<strat->generators[j].ecart()) 00301 return true; 00302 else 00303 return false; 00304 } 00305 return (strat->generators[i].weightedLength<strat->generators[j].weightedLength); 00306 00307 } 00308 }; 00309 class LessUsedTailVariablesThenLessWeightedLengthInStrat{ 00310 public: 00311 const GroebnerStrategy* strat; 00312 LessUsedTailVariablesThenLessWeightedLengthInStrat(const GroebnerStrategy& strat){ 00313 this->strat=&strat; 00314 } 00315 bool operator() (const Monomial& a , const Monomial& b) const{ 00316 int i=strat->lm2Index.find(a)->second; 00317 int j=strat->lm2Index.find(b)->second; 00318 deg_type d1=strat->generators[i].tailVariables.deg(); 00319 deg_type d2=strat->generators[j].tailVariables.deg();; 00320 if (d1!=d2){ 00321 return (d1<d2); 00322 } 00323 return (strat->generators[i].weightedLength<strat->generators[j].weightedLength); 00324 00325 } 00326 }; 00327 00328 class LessCombinedManySizesInStrat{ 00329 public: 00330 GroebnerStrategy* strat; 00331 LessCombinedManySizesInStrat(GroebnerStrategy& strat){ 00332 this->strat=&strat; 00333 } 00334 bool operator() (const Monomial& a , const Monomial& b){ 00335 int i=strat->lm2Index[a]; 00336 int j=strat->lm2Index[b]; 00337 deg_type d1=strat->generators[i].tailVariables.deg(); 00338 deg_type d2=strat->generators[j].tailVariables.deg(); 00339 wlen_type w1=d1; 00340 wlen_type w2=d2; 00341 w1*=strat->generators[i].length; 00342 w1*=strat->generators[i].ecart(); 00343 w2*=strat->generators[j].length; 00344 w2*=strat->generators[j].ecart(); 00345 return w1<w2; 00346 00347 00348 } 00349 }; 00350 00351 00352 Polynomial mult_fast_sim(const std::vector<Polynomial>& vec); 00353 std::vector<Polynomial> full_implication_gb(const Polynomial & p,CacheManager& cache,GroebnerStrategy& strat); 00354 Polynomial reduce_complete(const Polynomial &p, const PolyEntry& reductor, wlen_type &len); 00355 MonomialSet contained_variables_cudd_style(const MonomialSet& m); 00356 MonomialSet minimal_elements_cudd_style(MonomialSet m); 00357 MonomialSet recursively_insert(MonomialSet::navigator p, idx_type idx, MonomialSet mset); 00358 MonomialSet minimal_elements_cudd_style_unary(MonomialSet m); 00359 END_NAMESPACE_PBORIGB 00360 00361 #endif 00362