16 #ifndef polybori_groebner_GroebnerStrategy_h_
17 #define polybori_groebner_GroebnerStrategy_h_
30 #include <boost/shared_ptr.hpp>
52 !input_ring.ordering().isDegreeOrder()),
54 generators(input_ring),
57 chainCriterions(0), variableChainCriterions(0),
58 easyProductCriterions(0), extendedProductCriterions(0) { }
61 bool containsOne()
const {
return generators.leadingTerms.ownsOne(); }
63 std::vector<Polynomial> minimalizeAndTailReduce();
64 std::vector<Polynomial> minimalize();
66 void addGenerator(
const PolyEntry& entry);
69 void addGeneratorTrySplit(
const Polynomial& p,
bool is_minimal);
75 generators.monomials_plus_one.update(e);
80 void addNonTrivialImplicationsDelayed(
const PolyEntry& p);
83 void log(
const char* c)
const {
if (enabledLog) std::cout<<c<<std::endl; }
86 std::vector<Polynomial> noroStep(
const std::vector<Polynomial>&);
87 std::vector<Polynomial> faugereStepDense(
const std::vector<Polynomial>&);
91 int suggestPluginVariable();
92 std::vector<Polynomial> allGenerators();
96 return generators[i].isSingleton() && generators[j].isSingleton();
100 return checkSingletonCriterion(i, j) || checkExtendedProductCriterion(i, j)
101 || checkChainCriterion(lm, i, j);
104 bool checkChainCriterion(
const Exponent& lm,
int i,
int j);
105 bool checkExtendedProductCriterion(
int i,
int j);
109 return generators[idx].isSingleton();
113 bool result = generators[idx].literal_factors.occursAsLeadOfFactor(var);
115 log(
"delayed variable linear factor criterion");
120 bool result = !generators[idx].minimal;
122 ++variableChainCriterions;
128 checkVariableLeadOfFactorCriterion(idx, var)) ||
129 checkVariableChainCriterion(idx);
138 const Exponent& used_variables)
const;
149 void addImplications(
const BoolePolynomial& p, std::vector<int>& indices);
153 const Exponent& used_variables,
bool include_orig,
154 std::vector<Polynomial>& impl)
const;
157 bool include_orig, std::vector<Polynomial>&)
const;
159 template <
class Iterator>
160 void addImplications(Iterator, Iterator, std::vector<int>& indices);
161 void addImplications(
const std::vector<Polynomial>& impl,
int s);
163 typedef std::set<const PolyEntry*, PolyEntryPtrLmLess> entryset_type;
165 void propagateStep(entryset_type& others);
167 void updatePropagated(
const PolyEntry& entry);
171 void checkSingletonCriterion(
const PolyEntry& entry,
175 pairs.status.prolong(PairStatusSet::HAS_T_REP);
179 &self::markNextUncalculated));
183 void checkCriteria(
const PolyEntry& entry,
const MonomialSet& terms) {
184 checkSingletonCriterion(entry, terms);
185 easyProductCriterions += generators.minimalLeadingTerms.length() -
189 void markNextSingleton(
const Exponent& key) {
190 if (generators[key].isSingleton())
191 ++extendedProductCriterions;
193 markNextUncalculated(key);
196 void markNextUncalculated(
const BooleExponent& key) {
197 pairs.status.setToUncalculated(generators.index(key), generators.size());
205 boost::shared_ptr<CacheManager>
cache;