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