PolyBoRi
groebner_alg.h
Go to the documentation of this file.
1 /*
2  * groebner_alg.h
3  * PolyBoRi
4  *
5  * Created by Michael Brickenstein on 20.04.06.
6  * Copyright 2006 The PolyBoRi Team. See LICENSE file.
7  *
8  */
9 
10 
11 
12 #include <polybori.h>
13 #include "groebner_defs.h"
14 #include "pairs.h"
15 #include <boost/dynamic_bitset.hpp>
16 #include <vector>
17 #include <algorithm>
18 #include <utility>
19 #include <iostream>
20 #include "cache_manager.h"
21 #include "polynomial_properties.h"
22 #ifdef HAVE_HASH_MAP
23 #include <ext/hash_map>
24 #else
25 #include <map>
26 #endif
27 
28 
29 
30 #ifndef PBORI_GB_ALG_H
31 #define PBORI_GB_ALG_H
32 
33 
35 
36 #define LL_RED_FOR_GROEBNER 1
40 public:
41  typedef boost::dynamic_bitset<> bitvector_type;
42  bool hasTRep(int ia, int ja) const {
43  int i,j;
44  i=std::min(ia,ja);
45  j=std::max(ia,ja);
46  return table[j][i]==HAS_T_REP;
47  }
48  void setToHasTRep(int ia, int ja){
49  int i,j;
50  i=std::min(ia,ja);
51  j=std::max(ia,ja);
52  table[j][i]=HAS_T_REP;
53  }
54  void setToUncalculated(int ia, int ja){
55  int i,j;
56  i=std::min(ia,ja);
57  j=std::max(ia,ja);
58  table[j][i]=UNCALCULATED;
59  }
60  void prolong(bool value=UNCALCULATED){
61  int s=table.size();
62  table.push_back(bitvector_type(s, value));
63  }
64  PairStatusSet(int size=0){
65  int s=0;
66  for(s=0;s<size;s++){
67  prolong();
68  }
69  }
70  static const bool HAS_T_REP=true;
71  static const bool UNCALCULATED=false;
72 
73 protected:
74 std::vector<bitvector_type> table;
75 };
76 class GroebnerStrategy;
78 public:
82  this->strat=&strat;
83  }
84 
85  void appendHiddenGenerators(std::vector<Polynomial>& vec);
86  typedef std::priority_queue<Pair,std::vector<PairE>, PairECompare> queue_type;
88  void introducePair(const Pair& p);
89  Polynomial nextSpoly(const PolyEntryVector& gen);
90  bool pairSetEmpty() const;
91  void cleanTopByChainCriterion();
92 protected:
93  void replacePair(int& i, int & j);
94  };
96 public:
97  size_t operator() (const Monomial & m) const{
98  return m.hash();
99  }
100 };
101 /*
102 #ifdef HAVE_HASH_MAP
103 typedef __gnu_cxx::hash_map<Monomial,int, MonomialHasher> lm2Index_map_type;
104 #else
105 typedef std::map<Monomial,int> lm2Index_map_type;
106 #endif
107 */
108 
109 
113 public:
114  bool containsOne() const{
115  return leadingTerms.ownsOne();
116  }
118  GroebnerStrategy(const GroebnerStrategy& orig);
119  std::vector<Polynomial> minimalizeAndTailReduce();
120  std::vector<Polynomial> minimalize();
121  int addGenerator(const BoolePolynomial& p, bool is_impl=false, std::vector<int>* impl_v=NULL);
122  void addGeneratorDelayed(const BoolePolynomial & p);
123  void addAsYouWish(const Polynomial& p);
124  void addGeneratorTrySplit(const Polynomial& p, bool is_minimal);
125  bool variableHasValue(idx_type i);
126  void llReduceAll();
127  void treat_m_p_1_case(const PolyEntry& e);
138  boost::shared_ptr<CacheManager> cache;
141  unsigned int reductionSteps;
150  bool optLazy;
151  bool optLL;
162 
163  GroebnerStrategy():r(BooleEnv::ring()),pairs(*this),cache(new CacheManager()){
164  reducibleUntil=-1;
165  optDelayNonMinimals=true;
166  optRedTailDegGrowth=true;
167  chainCriterions=0;
168  enabledLog=false;
169  optLL=false;
170  //if (BooleEnv::ordering().isDegreeOrder())
171  // optBrutalReductions=false;
172  //else
173  optBrutalReductions=true;
174  variableChainCriterions=0;
175  extendedProductCriterions=0;
176  easyProductCriterions=0;
177  optRedTail=true;
178  optExchange=true;
179  optStepBounded=false;
180  optAllowRecursion=true;
181  optLinearAlgebraInLastBlock=true;
182  if (BooleEnv::ordering().isBlockOrder())
183  optRedTailInLastBlock=true;
184  else
185  optRedTailInLastBlock=false;
186 
187  if (BooleEnv::ordering().isDegreeOrder())
188  optLazy=false;
189  else
190  optLazy=true;
191  reduceByTailReduced=false;
192  llReductor=Polynomial(1).diagram(); // todo: is this unsafe?
193  }
194 
196  return pairs.nextSpoly(generators);
197  }
198  void addNonTrivialImplicationsDelayed(const PolyEntry& p);
199  void propagate(const PolyEntry& e);
200  void propagate_step(const PolyEntry& e, std::set<int> others);
201  void log(const char* c){
202  if (this->enabledLog)
203  std::cout<<c<<endl;
204  }
205  bool canRewrite(const Polynomial& p) const{
206  return is_rewriteable(p,minimalLeadingTerms);
207  }
208  Polynomial redTail(const Polynomial& p);
209  std::vector<Polynomial> noroStep(const std::vector<Polynomial>&);
210  std::vector<Polynomial> faugereStepDense(const std::vector<Polynomial>&);
211  //std::vector<Polynomial> faugereStepDenseModified(const std::vector<Polynomial>&);
212  Polynomial nf(Polynomial p) const;
213  void symmGB_F2();
214  int suggestPluginVariable();
215  std::vector<Polynomial> allGenerators();
216  protected:
217  std::vector<Polynomial> treatVariablePairs(int s);
218  void treatNormalPairs(int s,MonomialSet intersecting_terms,MonomialSet other_terms, MonomialSet ext_prod_terms);
219  void addVariablePairs(int s);
220  std::vector<Polynomial> add4ImplDelayed(const Polynomial& p, const Exponent& lm_exp, const Exponent& used_variables,int s, bool include_orig);
221  std::vector<Polynomial> addHigherImplDelayedUsing4(int s, const LiteralFactorization& literal_factors, bool include_orig);
222 
223 
224 };
225 MonomialSet mod_var_set(const MonomialSet& as, const MonomialSet& vs);
226 void groebner(GroebnerStrategy& strat);
227 Polynomial reduce_by_binom(const Polynomial& p, const Polynomial& binom);
228 Polynomial reduce_by_monom(const Polynomial& p, const Monomial& m);
229 Polynomial reduce_complete(const Polynomial& p, const Polynomial& reductor);
231 public:
234  this->strat=&strat;
235  }
236  bool operator() (const Monomial& a , const Monomial& b){
237  return strat->generators[strat->lm2Index.find(a)->second].weightedLength<strat->generators[strat->lm2Index.find(b)->second].weightedLength;
238 
239  }
240  bool operator() (const Exponent& a , const Exponent& b){
241  return strat->generators[strat->exp2Index.find(a)->second].weightedLength<strat->generators[strat->exp2Index.find(b)->second].weightedLength;
242 
243  }
244 };
245 
248  if ((e.deg==1) && (e.length<=4)){
249  //if (e.length==1) return -1;
250  //if (e.p.hasConstantPart()) return 0;
251  return res-1;
252  }
253  return res;
254 }
257 public:
260  this->strat=&strat;
261  }
262  bool operator() (const Monomial& a , const Monomial& b){
263  wlen_type wa=wlen_literal_exceptioned(strat->generators[strat->lm2Index.find(a)->second]);
264  wlen_type wb=wlen_literal_exceptioned(strat->generators[strat->lm2Index.find(b)->second]);
265 
266  return wa<wb;
267 
268  }
269  bool operator() (const Exponent& a , const Exponent& b){
270  wlen_type wa=wlen_literal_exceptioned(strat->generators[strat->exp2Index.find(a)->second]);
271  wlen_type wb=wlen_literal_exceptioned(strat->generators[strat->exp2Index.find(b)->second]);
272 
273  return wa<wb;
274 
275  }
276 };
278 public:
281  this->strat=&strat;
282  }
283  bool operator() (const Monomial& a , const Monomial& b){
284  int i=strat->lm2Index.find(a)->second;
285  int j=strat->lm2Index.find(b)->second;
286  if (strat->generators[i].ecart()!=strat->generators[j].ecart()){
287  if (strat->generators[i].ecart()<strat->generators[j].ecart())
288  return true;
289  else
290  return false;
291  }
292  return (strat->generators[i].weightedLength<strat->generators[j].weightedLength);
293 
294  }
295 
296  bool operator() (const Exponent& a , const Exponent& b){
297  int i=strat->exp2Index.find(a)->second;
298  int j=strat->exp2Index.find(b)->second;
299  if (strat->generators[i].ecart()!=strat->generators[j].ecart()){
300  if (strat->generators[i].ecart()<strat->generators[j].ecart())
301  return true;
302  else
303  return false;
304  }
305  return (strat->generators[i].weightedLength<strat->generators[j].weightedLength);
306 
307  }
308 };
310 public:
313  this->strat=&strat;
314  }
315  bool operator() (const Monomial& a , const Monomial& b) const{
316  int i=strat->lm2Index.find(a)->second;
317  int j=strat->lm2Index.find(b)->second;
318  deg_type d1=strat->generators[i].tailVariables.deg();
319  deg_type d2=strat->generators[j].tailVariables.deg();;
320  if (d1!=d2){
321  return (d1<d2);
322  }
323  return (strat->generators[i].weightedLength<strat->generators[j].weightedLength);
324 
325  }
326 };
327 
329 public:
332  this->strat=&strat;
333  }
334  bool operator() (const Monomial& a , const Monomial& b){
335  int i=strat->lm2Index[a];
336  int j=strat->lm2Index[b];
337  deg_type d1=strat->generators[i].tailVariables.deg();
338  deg_type d2=strat->generators[j].tailVariables.deg();
339  wlen_type w1=d1;
340  wlen_type w2=d2;
341  w1*=strat->generators[i].length;
342  w1*=strat->generators[i].ecart();
343  w2*=strat->generators[j].length;
344  w2*=strat->generators[j].ecart();
345  return w1<w2;
346 
347 
348  }
349 };
350 
351 
352 Polynomial mult_fast_sim(const std::vector<Polynomial>& vec);
353 std::vector<Polynomial> full_implication_gb(const Polynomial & p,CacheManager& cache,GroebnerStrategy& strat);
354 Polynomial reduce_complete(const Polynomial &p, const PolyEntry& reductor, wlen_type &len);
357 MonomialSet recursively_insert(MonomialSet::navigator p, idx_type idx, MonomialSet mset);
360 
361 #endif
362