PolyBoRi
|
00001 // -*- c++ -*- 00002 //***************************************************************************** 00014 //***************************************************************************** 00015 00016 #ifndef polybori_groebner_GroebnerStrategy_h_ 00017 #define polybori_groebner_GroebnerStrategy_h_ 00018 00019 // include basic definitions 00020 #include "pairs.h" 00021 #include "cache_manager.h" 00022 00023 #include "PairManagerFacade.h" 00024 #include "ReductionStrategy.h" 00025 #include "groebner_defs.h" 00026 #include "PolyEntryPtrLmLess.h" 00027 #include "GroebnerOptions.h" 00028 00029 #include <vector> 00030 #include <boost/shared_ptr.hpp> 00031 00032 #include <polybori/routines/pbori_algo.h> // member-for_each etc. 00033 00034 BEGIN_NAMESPACE_PBORIGB 00035 00036 00041 class GroebnerStrategy: 00042 public GroebnerOptions, public PairManagerFacade<GroebnerStrategy> { 00043 00044 typedef GroebnerStrategy self; 00045 public: 00047 GroebnerStrategy(const GroebnerStrategy& orig); 00048 00050 GroebnerStrategy(const BoolePolyRing& input_ring): 00051 GroebnerOptions(input_ring.ordering().isBlockOrder(), 00052 !input_ring.ordering().isDegreeOrder()), 00053 PairManagerFacade<GroebnerStrategy>(input_ring), 00054 generators(input_ring), 00055 00056 cache(new CacheManager()), 00057 chainCriterions(0), variableChainCriterions(0), 00058 easyProductCriterions(0), extendedProductCriterions(0) { } 00059 00060 const BoolePolyRing& ring() const { return generators.leadingTerms.ring(); } 00061 bool containsOne() const { return generators.leadingTerms.ownsOne(); } 00062 00063 std::vector<Polynomial> minimalizeAndTailReduce(); 00064 std::vector<Polynomial> minimalize(); 00065 00066 void addGenerator(const PolyEntry& entry); 00067 void addGeneratorDelayed(const BoolePolynomial & p); 00068 void addAsYouWish(const Polynomial& p); 00069 void addGeneratorTrySplit(const Polynomial& p, bool is_minimal); 00070 00071 bool variableHasValue(idx_type i); 00072 void llReduceAll(); 00073 00074 void treat_m_p_1_case(const PolyEntry& e) { 00075 generators.monomials_plus_one.update(e); 00076 } 00077 00078 00079 Polynomial nextSpoly(){ return pairs.nextSpoly(generators); } 00080 void addNonTrivialImplicationsDelayed(const PolyEntry& p); 00081 void propagate(const PolyEntry& e); 00082 00083 void log(const char* c) const { if (enabledLog) std::cout<<c<<std::endl; } 00084 00085 Polynomial redTail(const Polynomial& p); 00086 std::vector<Polynomial> noroStep(const std::vector<Polynomial>&); 00087 std::vector<Polynomial> faugereStepDense(const std::vector<Polynomial>&); 00088 00089 Polynomial nf(Polynomial p) const; 00090 void symmGB_F2(); 00091 int suggestPluginVariable(); 00092 std::vector<Polynomial> allGenerators(); 00093 00094 00095 bool checkSingletonCriterion(int i, int j) const { 00096 return generators[i].isSingleton() && generators[j].isSingleton(); 00097 } 00098 00099 bool checkPairCriteria(const Exponent& lm, int i, int j) { 00100 return checkSingletonCriterion(i, j) || checkExtendedProductCriterion(i, j) 00101 || checkChainCriterion(lm, i, j); 00102 } 00103 00104 bool checkChainCriterion(const Exponent& lm, int i, int j); 00105 bool checkExtendedProductCriterion(int i, int j); 00106 00107 00108 bool checkVariableSingletonCriterion(int idx) const { 00109 return generators[idx].isSingleton(); 00110 } 00111 00112 bool checkVariableLeadOfFactorCriterion(int idx, int var) const { 00113 bool result = generators[idx].literal_factors.occursAsLeadOfFactor(var); 00114 if (result) 00115 log("delayed variable linear factor criterion"); 00116 return result; 00117 } 00118 00119 bool checkVariableChainCriterion(int idx) { 00120 bool result = !generators[idx].minimal; 00121 if (result) 00122 ++variableChainCriterions; 00123 return result; 00124 } 00125 00126 bool checkVariableCriteria(int idx, int var) { 00127 return PBORI_UNLIKELY(checkVariableSingletonCriterion(idx) || 00128 checkVariableLeadOfFactorCriterion(idx, var)) || 00129 checkVariableChainCriterion(idx); 00130 } 00131 protected: 00132 std::vector<Polynomial> treatVariablePairs(PolyEntryReference); 00133 void normalPairsWithLast(const MonomialSet&); 00134 void addVariablePairs(PolyEntryReference); 00135 00136 std::vector<Polynomial> add4ImplDelayed(PolyEntryReference); 00137 std::vector<Polynomial> add4ImplDelayed(const Polynomial& p, const Exponent& lm_exp, 00138 const Exponent& used_variables) const; 00139 00140 00141 std::vector<Polynomial> addHigherImplDelayedUsing4(PolyEntryReference); 00142 std::vector<Polynomial> addHigherImplDelayedUsing4(const LiteralFactorization&) const; 00143 00144 00145 private: 00146 00147 int addGeneratorStep(const PolyEntry&); 00148 00149 void addImplications(const BoolePolynomial& p, std::vector<int>& indices); 00150 00151 00152 bool add4ImplDelayed(const Polynomial& p, const Exponent& lm_exp, 00153 const Exponent& used_variables, bool include_orig, 00154 std::vector<Polynomial>& impl) const; 00155 00156 bool addHigherImplDelayedUsing4(const LiteralFactorization&, 00157 bool include_orig, std::vector<Polynomial>&) const; 00158 00159 template <class Iterator> 00160 void addImplications(Iterator, Iterator, std::vector<int>& indices); 00161 void addImplications(const std::vector<Polynomial>& impl, int s); 00162 00163 typedef std::set<const PolyEntry*, PolyEntryPtrLmLess> entryset_type; 00164 00165 void propagateStep(entryset_type& others); 00166 void exchange(const Polynomial&, const PolyEntry&, entryset_type&); 00167 void updatePropagated(const PolyEntry& entry); 00168 00169 00170 // product criterion doesn't hold - try length 1 crit 00171 void checkSingletonCriterion(const PolyEntry& entry, 00172 const MonomialSet& intersection) { 00173 00174 PBORI_ASSERT(generators.checked_index(entry) == -1); 00175 pairs.status.prolong(PairStatusSet::HAS_T_REP); 00176 00177 for_each(intersection.expBegin(), intersection.expEnd(), *this, 00178 (entry.isSingleton()? &self::markNextSingleton: 00179 &self::markNextUncalculated)); 00180 } 00181 00183 void checkCriteria(const PolyEntry& entry, const MonomialSet& terms) { 00184 checkSingletonCriterion(entry, terms); 00185 easyProductCriterions += generators.minimalLeadingTerms.length() - 00186 terms.length(); 00187 } 00188 00189 void markNextSingleton(const Exponent& key) { 00190 if (generators[key].isSingleton()) 00191 ++extendedProductCriterions; 00192 else 00193 markNextUncalculated(key); 00194 } 00195 00196 void markNextUncalculated(const BooleExponent& key) { 00197 pairs.status.setToUncalculated(generators.index(key), generators.size()); 00198 } 00199 00200 bool shorterElimination(const MonomialSet& divisors, wlen_type el, 00201 MonomialSet::deg_type deg) const; 00202 public: 00204 ReductionStrategy generators; 00205 boost::shared_ptr<CacheManager> cache; 00206 00207 unsigned int reductionSteps; 00208 int normalForms; 00209 int currentDegree; 00210 int averageLength; 00211 00212 int chainCriterions; 00213 int variableChainCriterions; 00214 int easyProductCriterions; 00215 int extendedProductCriterions; 00216 00217 }; 00218 00219 END_NAMESPACE_PBORIGB 00220 00221 #endif /* polybori_GroebnerStrategy_h_ */