00001 #ifndef UNIFY_H 00002 #define UNIFY_H 00003 00004 #include <map> 00005 #include <set> 00006 #include <string> 00007 00008 #include "parser-classes.hpp" 00009 #include "constraint.hpp" 00010 00011 class unifier 00012 { 00013 public: 00014 00020 friend std::ostream &operator<<(std::ostream &os, const unifier *u); 00021 00025 ~unifier(); 00026 00030 unifier(); 00031 00038 bool add_binding(const std::string &s, const c_term *t); 00039 00045 void apply_to(class c_term *t, bool skip_renaming = false) const; 00046 00052 void apply_to(class c_rule *r, bool skip_renaming = false) const; 00053 00058 void apply_to(con_type &c) const; 00059 00069 bool unify(const class c_term *t1, const class c_term *t2); 00070 00080 bool unify(const class c_rule *r1, const class c_rule *r2); 00081 00085 static int count; 00086 00087 private: 00088 00089 std::map<std::string, c_term*> bindings; 00090 }; 00091 00092 #endif //UNIFY_H