00001 #ifndef UNIFICATION_H 00002 #define UNIFICATION_H 00003 00004 #include "parser.h" 00005 #include "config.h" 00006 #include <ostream> 00007 00008 class Unification; 00009 00010 class Solution 00011 { 00012 public: 00013 virtual void display(ostream &o) = 0; 00014 virtual bool check() = 0; 00015 }; 00016 00017 class VariableSolution 00018 { 00019 public: 00020 VariableSolution(); 00021 bool seeoutside; 00022 Node *definition; 00023 list<Condition*> definitionc; 00024 }; 00025 00026 class SimpleSolution : public Solution 00027 { 00028 public: 00029 Unification *unification; 00030 bool fail; 00031 unsigned int ndvar; 00032 unsigned int ndnumvar; 00033 VariableSolution *variableSolution; 00034 VariableSolution *numericalvariableSolution; 00035 SimpleSolution(unsigned int ndvar,unsigned int ndnumvar,Unification *unification); 00036 ~SimpleSolution(); 00037 void display(ostream &o); 00038 bool check(); 00039 }; 00040 00041 class Unification 00042 { 00043 public: 00044 Configuration *configuration; 00045 Parser *parser; 00046 bool result; 00047 00048 list<Solution*> solutions; 00049 00050 Unification(Configuration *configuration,Parser *parser); 00051 void run(); 00052 Node* ApplyR0(Node *start=NULL); 00053 bool tryApplyR1(); 00054 bool tryApplyR2(); 00055 bool tryApplyR3(); 00056 bool tryApplyR4(); 00057 bool tryApplyR5(); 00058 Node* SetDisjunctiveSystem(Node *start = NULL); 00059 bool checkDefinition(); 00060 void debugDisplay(ostream &s); 00061 bool exploDefinition(Node *n, SimpleSolution *solution); 00062 bool verifValidPresburger(Node *n); 00063 ~Unification(); 00064 00065 static int gcd(unsigned int a,unsigned int b); 00066 static bool prefix(const list<unsigned int> &l1,const list<unsigned int> &l2); 00067 static list<unsigned int> append(const list<unsigned int> &l1,const list<unsigned int> &l2); 00068 00069 }; 00070 00071 #endif 00072