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