00001
00002
00003
00004
00005
00006
00007
00008
00009 #include <functional>
00010 #include "groebner_defs.h"
00011 #include "literal_factorization.h"
00012 #include <boost/shared_ptr.hpp>
00013 #include <queue>
00014 #include <algorithm>
00015 #include <utility>
00016 #include <set>
00017
00018 #ifndef PB_PAIR_H
00019 #define PB_PAIR_H
00020
00021 BEGIN_NAMESPACE_PBORIGB
00022
00023 class PolyEntry{
00024 public:
00025 PolyEntry(const Polynomial &p);
00026 LiteralFactorization literal_factors;
00027 Polynomial p;
00028 Monomial lm;
00029 wlen_type weightedLength;
00030 len_type length;
00031 deg_type deg;
00032 deg_type lmDeg;
00033 Exponent lmExp;
00034 Monomial gcdOfTerms;
00035 Exponent usedVariables;
00036 Exponent tailVariables;
00037 Polynomial tail;
00039 std::set<idx_type> vPairCalculated;
00040 deg_type ecart() const{
00041 return deg-lmDeg;
00042 }
00043 bool minimal;
00044 void recomputeInformation();
00045 };
00046
00047 typedef std::vector<PolyEntry> PolyEntryVector;
00048
00049 class PairData{
00050 public:
00051
00052 virtual ~PairData()=0;
00053
00054 virtual Polynomial extract(const PolyEntryVector& v)=0;
00055 };
00056 class IJPairData: public PairData{
00057 public:
00058 int i;
00059 int j;
00060 Polynomial extract(const PolyEntryVector& v){
00061 return spoly(v[i].p,v[j].p);
00062 }
00063 IJPairData(int i, int j){
00064 this->i=i;
00065 this->j=j;
00066 }
00067 };
00068 class PolyPairData: public PairData{
00069 public:
00070 Polynomial p;
00071 Polynomial extract(const PolyEntryVector& v){
00072 return p;
00073 }
00074 PolyPairData(const BoolePolynomial& p){
00075 this->p=p;
00076 }
00077 };
00078
00079 class VariablePairData: public PairData{
00080 public:
00081 int i;
00082 idx_type v;
00083 Polynomial extract(const PolyEntryVector& gen){
00084 return Monomial(Variable(v, gen[i].p.ring()))*gen[i].p;
00085 }
00086 VariablePairData(int i, idx_type v){
00087 this->v=v;
00088 this->i=i;
00089 }
00090 };
00091 typedef boost::shared_ptr<PairData> pair_data_ptr;
00092 enum {
00093 VARIABLE_PAIR,
00094 IJ_PAIR,
00095 DELAYED_PAIR
00096 };
00097
00098 class PairLS{
00099 private:
00100 int type;
00101 public:
00102 int getType() const{
00103 return type;
00104 }
00105 wlen_type wlen;
00106 deg_type sugar;
00107
00108
00109 pair_data_ptr data;
00110 Monomial lm;
00111 Polynomial extract(const PolyEntryVector& v){
00112 return data->extract(v);
00113 }
00114 PairLS(int i, int j, const PolyEntryVector &v):
00115 data(new IJPairData(i,j)),
00116 lm(v[i].lm*v[j].lm),
00117 wlen(v[i].weightedLength+v[j].weightedLength-2)
00118 {
00119 type=IJ_PAIR;
00120 sugar=lm.deg()+std::max(v[i].ecart(),v[j].ecart());
00121 }
00122 PairLS(int i, idx_type v, const PolyEntryVector &gen,int type):
00123 data(new VariablePairData(i,v)),
00124 sugar(gen[i].deg+1),
00125
00126 wlen(gen[i].weightedLength+gen[i].length),
00127 lm(gen[i].lm)
00128
00129 {
00130 assert(type==VARIABLE_PAIR);
00131 this->type=type;
00132 }
00133
00134 PairLS(const Polynomial& delayed):
00135 data(new PolyPairData(delayed)),
00136 lm(delayed.lead()),
00137 sugar(delayed.deg()), wlen(delayed.eliminationLength()){
00138 this->type=DELAYED_PAIR;
00139 }
00140
00141 };
00142
00143 class PairE{
00144 private:
00145 int type;
00146 public:
00147 int getType() const{
00148 return type;
00149 }
00150 wlen_type wlen;
00151 deg_type sugar;
00152
00153
00154 pair_data_ptr data;
00155 Exponent lm;
00156 Polynomial extract(const PolyEntryVector& v){
00157 return data->extract(v);
00158 }
00159 PairE(int i, int j, const PolyEntryVector &v):
00160 data(new IJPairData(i,j)),
00161 lm(v[i].lmExp+v[j].lmExp),
00162 wlen(v[i].weightedLength+v[j].weightedLength-2)
00163 {
00164 type=IJ_PAIR;
00165 sugar=lm.deg()+std::max(v[i].ecart(),v[j].ecart());
00166 }
00167 PairE(int i, idx_type v, const PolyEntryVector &gen,int type):
00168 data(new VariablePairData(i,v)),
00169 sugar(gen[i].deg+1),
00170
00171 wlen(gen[i].weightedLength+gen[i].length),
00172 lm(gen[i].lmExp)
00173
00174 {
00175 assert(type==VARIABLE_PAIR);
00176 this->type=type;
00177 if (gen[i].lmExp==gen[i].usedVariables)
00178 sugar=gen[i].deg;
00179 if (gen[i].tailVariables.deg()<gen[i].deg)
00180 sugar=gen[i].deg;
00181 }
00182
00183 PairE(const Polynomial& delayed):
00184 data(new PolyPairData(delayed)),
00185
00186 lm(delayed.leadExp()),
00187 sugar(delayed.deg()), wlen(delayed.eliminationLength()){
00188 this->type=DELAYED_PAIR;
00189 }
00190
00191 };
00192
00193
00194
00195 class PairLSCompare{
00196 public:
00198 bool operator() (const PairLS& l, const PairLS& r){
00199 if (l.sugar!=r.sugar) return l.sugar>r.sugar;
00200 if (l.wlen!=r.wlen) return l.wlen>r.wlen;
00201 if (l.lm!=r.lm) return l.lm>r.lm;
00202
00204 return false;
00205 }
00206 };
00207
00208 class PairECompare{
00209 public:
00211 bool operator() (const PairE& l, const PairE& r){
00212 if (l.sugar!=r.sugar) return l.sugar>r.sugar;
00213 if (l.wlen!=r.wlen) return l.wlen>r.wlen;
00214 if (l.lm!=r.lm) return l.lm>r.lm;
00215
00217 return false;
00218 }
00219 };
00220 typedef PairE Pair;
00221
00222 END_NAMESPACE_PBORIGB
00223
00224 #endif