00001 #include "aterm.hh"
00002 #include "ppsig.hh"
00003
00004
00005 #undef TRACE
00006
00007 using namespace std;
00008
00009 typedef map<Tree,mterm> SM;
00010
00011 aterm::aterm ()
00012 {}
00013
00014
00018 aterm::aterm (Tree t)
00019 {
00020 #ifdef TRACE
00021 cerr << "aterm::aterm (" << ppsig(t)<< ")" << endl;
00022 #endif
00023 *this += t;
00024 #ifdef TRACE
00025 cerr << "aterm::aterm (" << ppsig(t)<< ") : -> " << *this << endl;
00026 #endif
00027 }
00028
00029
00033 static Tree simplifyingAdd(Tree t1, Tree t2)
00034 {
00035 assert(t1!=0);
00036 assert(t2!=0);
00037
00038 if (isNum(t1) && isNum(t2)) {
00039 return addNums(t1,t2);
00040
00041 } else if (isZero(t1)) {
00042 return t2;
00043
00044 } else if (isZero(t2)) {
00045 return t1;
00046
00047 } else if (t1 <= t2) {
00048 return sigAdd(t1, t2);
00049
00050 } else {
00051 return sigAdd(t2, t1);
00052 }
00053 }
00054
00059 Tree aterm::normalizedTree() const
00060 {
00061
00062
00063
00064 Tree P[4], N[4];
00065
00066
00067 for (int order = 0; order < 4; order++) P[order] = N[order] = tree(0);
00068
00069
00070 for (SM::const_iterator p = fSig2MTerms.begin(); p != fSig2MTerms.end(); p++) {
00071 const mterm& m = p->second;
00072 if (m.isNegative()) {
00073 Tree t = m.normalizedTree(false, true);
00074 int order = getSigOrder(t);
00075 N[order] = simplifyingAdd(N[order],t);
00076 } else {
00077 Tree t = m.normalizedTree();
00078 int order = getSigOrder(t);
00079 P[order] = simplifyingAdd(P[order],t);
00080 }
00081 }
00082
00083
00084 Tree SUM = tree(0);
00085 for (int order = 0; order < 4; order++) {
00086 if (!isZero(P[order])) {
00087 SUM = simplifyingAdd(SUM,P[order]);
00088 }
00089 if (!isZero(N[order])) {
00090 if (isZero(SUM) && (order < 3)) {
00091
00092 N[order+1] = simplifyingAdd(N[order], N[order+1]);
00093 } else {
00094 SUM = sigSub(SUM, N[order]);
00095 }
00096 }
00097 }
00098
00099 assert(SUM);
00100 return SUM;
00101 }
00102
00103
00107 ostream& aterm::print(ostream& dst) const
00108 {
00109 if (fSig2MTerms.empty()) {
00110 dst << "AZERO";
00111 } else {
00112 const char* sep = "";
00113 for (SM::const_iterator p = fSig2MTerms.begin(); p != fSig2MTerms.end(); p++) {
00114 dst << sep << p->second;
00115 sep = " + ";
00116 }
00117 }
00118
00119 return dst;
00120 }
00121
00122
00127 const aterm& aterm::operator += (Tree t)
00128 {
00129 int op;
00130 Tree x,y;
00131
00132 assert(t!=0);
00133
00134 if (isSigBinOp(t, &op, x, y) && (op == kAdd)) {
00135 *this += x;
00136 *this += y;
00137
00138 } else if (isSigBinOp(t, &op, x, y) && (op == kSub)) {
00139 *this += x;
00140 *this -= y;
00141
00142 } else {
00143 mterm m(t);
00144 *this += m;
00145 }
00146 return *this;
00147 }
00148
00149
00154 const aterm& aterm::operator -= (Tree t)
00155 {
00156 int op;
00157 Tree x,y;
00158
00159 assert(t!=0);
00160
00161 if (isSigBinOp(t, &op, x, y) && (op == kAdd)) {
00162 *this -= x;
00163 *this -= y;
00164
00165 } else if (isSigBinOp(t, &op, x, y) && (op == kSub)) {
00166 *this -= x;
00167 *this += y;
00168
00169 } else {
00170 mterm m(t);
00171 *this -= m;
00172 }
00173 return *this;
00174 }
00175
00176
00180 const aterm& aterm::operator += (const mterm& m)
00181 {
00182 #ifdef TRACE
00183 cerr << *this << " aterm::+= " << m << endl;
00184 #endif
00185 Tree sig = m.signatureTree();
00186 #ifdef TRACE
00187 cerr << "signature " << *sig << endl;
00188 #endif
00189 SM::const_iterator p = fSig2MTerms.find(sig);
00190 if (p == fSig2MTerms.end()) {
00191
00192 fSig2MTerms.insert(make_pair(sig,m));
00193 } else {
00194 fSig2MTerms[sig] += m;
00195 }
00196 return *this;
00197 }
00198
00199
00203 const aterm& aterm::operator -= (const mterm& m)
00204 {
00205
00206 Tree sig = m.signatureTree();
00207
00208 SM::const_iterator p = fSig2MTerms.find(sig);
00209 if (p == fSig2MTerms.end()) {
00210
00211 fSig2MTerms.insert(make_pair(sig,m*mterm(-1)));
00212 } else {
00213 fSig2MTerms[sig] -= m;
00214 }
00215 return *this;
00216 }
00217
00218 mterm aterm::greatestDivisor() const
00219 {
00220 int maxComplexity = 0;
00221 mterm maxGCD(1);
00222
00223 for (SM::const_iterator p1 = fSig2MTerms.begin(); p1 != fSig2MTerms.end(); p1++) {
00224 for (SM::const_iterator p2 = p1; p2 != fSig2MTerms.end(); p2++) {
00225 if (p2 != p1) {
00226 mterm g = gcd(p1->second,p2->second);
00227 if (g.complexity()>maxComplexity) {
00228 maxComplexity = g.complexity();
00229 maxGCD = g;
00230 }
00231 }
00232 }
00233 }
00234
00235 return maxGCD;
00236 }
00237
00241 aterm aterm::factorize(const mterm& d)
00242 {
00243
00244 aterm A;
00245 aterm Q;
00246
00247
00248 for (SM::const_iterator p1 = fSig2MTerms.begin(); p1 != fSig2MTerms.end(); p1++) {
00249 mterm t = p1->second;
00250 if (t.hasDivisor(d)) {
00251 mterm q = t/d;
00252
00253 Q += q;
00254
00255 } else {
00256 A += t;
00257
00258 }
00259 }
00260
00261
00262
00263
00264
00265
00266
00267
00268 A += sigMul(d.normalizedTree(), Q.normalizedTree());
00269
00270
00271 return A;
00272 }
00273
00274
00275