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