• Main Page
  • Related Pages
  • Namespaces
  • Classes
  • Files
  • File List
  • File Members

groebner_alg.h

Go to the documentation of this file.
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 

Generated on Tue Sep 14 2010 for PolyBoRi by  doxygen 1.7.1