#include <unify.h>
Public Member Functions | |
~unifier () | |
unifier () | |
bool | add_binding (const string &s, const c_term *t) |
void | apply_to (struct c_term *t, bool skip_renaming=false) const |
void | apply_to (struct c_rule *r, bool skip_renaming=false) const |
void | apply_to (con_type &c) const |
bool | unify (const struct c_term *t1, const struct c_term *t2) |
bool | unify (const struct c_rule *r1, const struct c_rule *r2) |
Static Public Attributes | |
int | count = 0 |
Private Attributes | |
map< string, c_term * > | bindings |
Friends | |
ostream & | operator<< (ostream &os, const unifier *u) |
|
Destructor that deeply deletes all terms in its bindings. |
|
Default constructor. |
|
Adds a binding for a variable name to a term. The given term is copied.
|
|
Apply this binding to a constraint.
|
|
Apply this binding to a rule.
|
|
Apply this binding to a term.
|
|
Get the most general unifier of two rules. The necessary bindings will be added to the unifier. If two variables unify with eachother, the binding is directed from the second term to the first.
|
|
Get the most general unifier of two terms. The necessary bindings will be added to the unifier. If two variables unify with eachother, the binding is directed from the second term to the first.
|
|
Write a text representation of this unifier to an ostream.
|
|
|
|
The number of unifiers allocated and not destroyed. |