aterm.hh

#ifndef __ATERM__
#define __ATERM__

#include <stdio.h>
#include <assert.h>
#include "tlib.hh"
#include "signals.hh"
#include "sigprint.hh"
#include "simplify.hh"
#include "normalize.hh"
#include "sigorderrules.hh"
#include <map>
#include <list>

#include "mterm.hh"

using namespace std;

class aterm
{

    map<Tree,mterm> fSig2MTerms;                

 public:
    aterm ();                                   
    aterm (Tree t);                             
    aterm (const aterm& a);                     

    const aterm& operator += (Tree t);          
    const aterm& operator -= (Tree t);          
    
    const aterm& operator += (const mterm& m);  
    const aterm& operator -= (const mterm& m);  
    Tree normalizedTree() const;                
    
    ostream& print(ostream& dst) const;         
    mterm greatestDivisor() const;              
    aterm factorize(const mterm& d);            
};

inline ostream& operator << (ostream& s, const aterm& a) { return a.print(s); }


#endif

---