PolyBoRi
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 <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