00001 #ifndef __ATERM__ 00002 #define __ATERM__ 00003 00004 #include <stdio.h> 00005 #include <assert.h> 00006 #include "tlib.hh" 00007 #include "signals.hh" 00008 #include "sigprint.hh" 00009 #include "simplify.hh" 00010 #include "normalize.hh" 00011 #include "sigorderrules.hh" 00012 #include <map> 00013 #include <list> 00014 00015 #include "mterm.hh" 00016 00017 using namespace std; 00018 00023 class aterm 00024 { 00025 00026 map<Tree,mterm> fSig2MTerms; 00027 00028 public: 00029 aterm (); 00030 aterm (Tree t); 00031 aterm (const aterm& a); 00032 00033 const aterm& operator += (Tree t); 00034 const aterm& operator -= (Tree t); 00035 00036 const aterm& operator += (const mterm& m); 00037 const aterm& operator -= (const mterm& m); 00038 Tree normalizedTree() const; 00039 00040 ostream& print(ostream& dst) const; 00041 mterm greatestDivisor() const; 00042 aterm factorize(const mterm& d); 00043 }; 00044 00045 inline ostream& operator << (ostream& s, const aterm& a) { return a.print(s); } 00046 00047 00048 #endif