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:
47  GroebnerStrategy(const GroebnerStrategy& orig);
48 
50  GroebnerStrategy(const BoolePolyRing& input_ring):
51  GroebnerOptions(input_ring.ordering().isBlockOrder(),
52  !input_ring.ordering().isDegreeOrder()),
53  PairManagerFacade<GroebnerStrategy>(input_ring),
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_ */
This class is just a wrapper for using variables for storing indices as interim data structure for Bo...
Definition: BooleExponent.h:34
void treat_m_p_1_case(const PolyEntry &e)
Definition: GroebnerStrategy.h:74
polybori::BooleExponent Exponent
Definition: groebner_defs.h:33
#define END_NAMESPACE_PBORIGB
Definition: groebner_defs.h:16
Definition: LiteralFactorization.h:24
int deg_type
Definition: groebner_defs.h:42
exp_iterator expEnd() const
Finish of iteration over exponent vectors.
Definition: BooleSet.cc:109
bool checkPairCriteria(const Exponent &lm, int i, int j)
Definition: GroebnerStrategy.h:99
This class reinterprets decicion diagram managers as Boolean polynomial rings, adds an ordering and v...
Definition: BoolePolyRing.h:40
int normalForms
Definition: GroebnerStrategy.h:208
#define BEGIN_NAMESPACE_PBORIGB
Definition: groebner_defs.h:15
This class defines options settings for GroebnerStrategy.
Definition: GroebnerOptions.h:32
exp_iterator expBegin() const
Start of iteration over exponent vectors.
Definition: BooleSet.cc:101
This class defines PolyEntry.
Definition: PolyEntry.h:32
int variableChainCriterions
Definition: GroebnerStrategy.h:213
ReductionStrategy generators
Definition: GroebnerStrategy.h:204
This class wraps the underlying decicion diagram type and defines the necessary operations.
Definition: BoolePolynomial.h:85
polybori::BooleSet MonomialSet
Definition: groebner_defs.h:45
int currentDegree
Definition: GroebnerStrategy.h:209
bool checkSingletonCriterion(int i, int j) const
Definition: GroebnerStrategy.h:95
int averageLength
Definition: GroebnerStrategy.h:210
Polynomial nextSpoly()
Definition: GroebnerStrategy.h:79
bool checkVariableChainCriterion(int idx)
Definition: GroebnerStrategy.h:119
bool isSingleton() const
Definition: PolyEntry.h:67
bool containsOne() const
Definition: GroebnerStrategy.h:61
Definition: cache_manager.h:28
This class defines GroebnerStrategy.
Definition: GroebnerStrategy.h:41
bool checkVariableSingletonCriterion(int idx) const
Definition: GroebnerStrategy.h:108
int easyProductCriterions
Definition: GroebnerStrategy.h:214
#define PBORI_ASSERT(arg)
Definition: pbori_defs.h:118
void log(const char *c) const
Definition: GroebnerStrategy.h:83
long wlen_type
Definition: groebner_defs.h:39
unsigned int reductionSteps
Definition: GroebnerStrategy.h:207
This class defines a facade for a given Strategy, which.
Definition: PairManagerFacade.h:79
const BoolePolyRing & ring() const
Definition: GroebnerStrategy.h:60
int extendedProductCriterions
Definition: GroebnerStrategy.h:215
int chainCriterions
Definition: GroebnerStrategy.h:212
polybori::CTypes::idx_type idx_type
Definition: groebner_defs.h:44
boost::shared_ptr< CacheManager > cache
Definition: GroebnerStrategy.h:205
GroebnerStrategy(const BoolePolyRing &input_ring)
Construct from a ring.
Definition: GroebnerStrategy.h:50
Definition: BooleSet.h:57
bool checkVariableCriteria(int idx, int var)
Definition: GroebnerStrategy.h:126
This class defines ReductionStrategy.
Definition: ReductionStrategy.h:34
This class defines PolyEntryReference.
Definition: PolyEntryReference.h:34
#define PBORI_UNLIKELY(expression)
Definition: pbori_defs.h:59
void for_each(InIter start, InIter finish, Object &obj, MemberFuncPtr func)
Definition: pbori_algo.h:857
bool checkVariableLeadOfFactorCriterion(int idx, int var) const
Definition: GroebnerStrategy.h:112