PolyBoRi
GroebnerStrategy.h
Go to the documentation of this file.
1 // -*- c++ -*-
2 //*****************************************************************************
14 //*****************************************************************************
15 
16 #ifndef polybori_groebner_GroebnerStrategy_h_
17 #define polybori_groebner_GroebnerStrategy_h_
18 
19 // include basic definitions
20 #include "pairs.h"
21 #include "cache_manager.h"
22 
23 #include "PairManagerFacade.h"
24 #include "ReductionStrategy.h"
25 #include "groebner_defs.h"
26 #include "PolyEntryPtrLmLess.h"
27 #include "GroebnerOptions.h"
28 
29 #include <vector>
30 #include <boost/shared_ptr.hpp>
31 
32 #include <polybori/routines/pbori_algo.h> // member-for_each etc.
33 
35 
36 
42  public GroebnerOptions, public PairManagerFacade<GroebnerStrategy> {
43 
44  typedef GroebnerStrategy self;
45 public:
48 
50  GroebnerStrategy(const BoolePolyRing& input_ring):
51  GroebnerOptions(input_ring.ordering().isBlockOrder(),
52  !input_ring.ordering().isDegreeOrder()),
54  generators(input_ring),
55 
56  cache(new CacheManager()),
57  chainCriterions(0), variableChainCriterions(0),
58  easyProductCriterions(0), extendedProductCriterions(0) { }
59 
60  const BoolePolyRing& ring() const { return generators.leadingTerms.ring(); }
61  bool containsOne() const { return generators.leadingTerms.ownsOne(); }
62 
63  std::vector<Polynomial> minimalizeAndTailReduce();
64  std::vector<Polynomial> minimalize();
65 
66  void addGenerator(const PolyEntry& entry);
67  void addGeneratorDelayed(const BoolePolynomial & p);
68  void addAsYouWish(const Polynomial& p);
69  void addGeneratorTrySplit(const Polynomial& p, bool is_minimal);
70 
71  bool variableHasValue(idx_type i);
72  void llReduceAll();
73 
74  void treat_m_p_1_case(const PolyEntry& e) {
75  generators.monomials_plus_one.update(e);
76  }
77 
78 
79  Polynomial nextSpoly(){ return pairs.nextSpoly(generators); }
80  void addNonTrivialImplicationsDelayed(const PolyEntry& p);
81  void propagate(const PolyEntry& e);
82 
83  void log(const char* c) const { if (enabledLog) std::cout<<c<<std::endl; }
84 
85  Polynomial redTail(const Polynomial& p);
86  std::vector<Polynomial> noroStep(const std::vector<Polynomial>&);
87  std::vector<Polynomial> faugereStepDense(const std::vector<Polynomial>&);
88 
89  Polynomial nf(Polynomial p) const;
90  void symmGB_F2();
91  int suggestPluginVariable();
92  std::vector<Polynomial> allGenerators();
93 
94 
95  bool checkSingletonCriterion(int i, int j) const {
96  return generators[i].isSingleton() && generators[j].isSingleton();
97  }
98 
99  bool checkPairCriteria(const Exponent& lm, int i, int j) {
100  return checkSingletonCriterion(i, j) || checkExtendedProductCriterion(i, j)
101  || checkChainCriterion(lm, i, j);
102  }
103 
104  bool checkChainCriterion(const Exponent& lm, int i, int j);
105  bool checkExtendedProductCriterion(int i, int j);
106 
107 
108  bool checkVariableSingletonCriterion(int idx) const {
109  return generators[idx].isSingleton();
110  }
111 
112  bool checkVariableLeadOfFactorCriterion(int idx, int var) const {
113  bool result = generators[idx].literal_factors.occursAsLeadOfFactor(var);
114  if (result)
115  log("delayed variable linear factor criterion");
116  return result;
117  }
118 
120  bool result = !generators[idx].minimal;
121  if (result)
122  ++variableChainCriterions;
123  return result;
124  }
125 
126  bool checkVariableCriteria(int idx, int var) {
127  return PBORI_UNLIKELY(checkVariableSingletonCriterion(idx) ||
128  checkVariableLeadOfFactorCriterion(idx, var)) ||
129  checkVariableChainCriterion(idx);
130  }
131 protected:
132  std::vector<Polynomial> treatVariablePairs(PolyEntryReference);
133  void normalPairsWithLast(const MonomialSet&);
134  void addVariablePairs(PolyEntryReference);
135 
136  std::vector<Polynomial> add4ImplDelayed(PolyEntryReference);
137  std::vector<Polynomial> add4ImplDelayed(const Polynomial& p, const Exponent& lm_exp,
138  const Exponent& used_variables) const;
139 
140 
141  std::vector<Polynomial> addHigherImplDelayedUsing4(PolyEntryReference);
142  std::vector<Polynomial> addHigherImplDelayedUsing4(const LiteralFactorization&) const;
143 
144 
145 private:
146 
147  int addGeneratorStep(const PolyEntry&);
148 
149  void addImplications(const BoolePolynomial& p, std::vector<int>& indices);
150 
151 
152  bool add4ImplDelayed(const Polynomial& p, const Exponent& lm_exp,
153  const Exponent& used_variables, bool include_orig,
154  std::vector<Polynomial>& impl) const;
155 
156  bool addHigherImplDelayedUsing4(const LiteralFactorization&,
157  bool include_orig, std::vector<Polynomial>&) const;
158 
159  template <class Iterator>
160  void addImplications(Iterator, Iterator, std::vector<int>& indices);
161  void addImplications(const std::vector<Polynomial>& impl, int s);
162 
163  typedef std::set<const PolyEntry*, PolyEntryPtrLmLess> entryset_type;
164 
165  void propagateStep(entryset_type& others);
166  void exchange(const Polynomial&, const PolyEntry&, entryset_type&);
167  void updatePropagated(const PolyEntry& entry);
168 
169 
170  // product criterion doesn't hold - try length 1 crit
171  void checkSingletonCriterion(const PolyEntry& entry,
172  const MonomialSet& intersection) {
173 
174  PBORI_ASSERT(generators.checked_index(entry) == -1);
175  pairs.status.prolong(PairStatusSet::HAS_T_REP);
176 
177  for_each(intersection.expBegin(), intersection.expEnd(), *this,
178  (entry.isSingleton()? &self::markNextSingleton:
179  &self::markNextUncalculated));
180  }
181 
183  void checkCriteria(const PolyEntry& entry, const MonomialSet& terms) {
184  checkSingletonCriterion(entry, terms);
185  easyProductCriterions += generators.minimalLeadingTerms.length() -
186  terms.length();
187  }
188 
189  void markNextSingleton(const Exponent& key) {
190  if (generators[key].isSingleton())
191  ++extendedProductCriterions;
192  else
193  markNextUncalculated(key);
194  }
195 
196  void markNextUncalculated(const BooleExponent& key) {
197  pairs.status.setToUncalculated(generators.index(key), generators.size());
198  }
199 
200  bool shorterElimination(const MonomialSet& divisors, wlen_type el,
201  MonomialSet::deg_type deg) const;
202 public:
205  boost::shared_ptr<CacheManager> cache;
206 
207  unsigned int reductionSteps;
211 
216 
217 };
218 
220 
221 #endif /* polybori_GroebnerStrategy_h_ */