00001
00002
00003
00004
00005
00006
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
00103
00104
00105
00106
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
00172
00173
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();
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
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
00252
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