16 #ifndef polybori_groebner_GroebnerStrategy_h_
17 #define polybori_groebner_GroebnerStrategy_h_
30 #include <boost/shared_ptr.hpp>
47 GroebnerStrategy(
const GroebnerStrategy& orig);
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;
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