Main Page | Namespace List | Class Hierarchy | Alphabetical List | Class List | File List | Class Members | File Members

unifier Class Reference

#include <unify.hpp>

List of all members.

Public Member Functions

 ~unifier ()
 unifier ()
bool add_binding (const std::string &s, const c_term *t)
void apply_to (class c_term *t, bool skip_renaming=false) const
void apply_to (class c_rule *r, bool skip_renaming=false) const
void apply_to (con_type &c) const
bool unify (const class c_term *t1, const class c_term *t2)
bool unify (const class c_rule *r1, const class c_rule *r2)

Static Public Attributes

int count = 0

Private Attributes

std::map< std::string, c_term * > bindings

Friends

std::ostream & operator<< (std::ostream &os, const unifier *u)


Constructor & Destructor Documentation

unifier::~unifier  ) 
 

Destructor that deeply deletes all terms in its bindings.

unifier::unifier  ) 
 

Default constructor.


Member Function Documentation

bool unifier::add_binding const std::string &  s,
const c_term t
 

Adds a binding for a variable name to a term. The given term is copied.

Parameters:
s the variable name.
t the term.
Returns:
Could the binding be added? (did it not collide with earlier non-unifiable bindings?)

void unifier::apply_to con_type c  )  const
 

Apply this binding to a constraint.

Parameters:
c the constraint to apply the unifier to.

void unifier::apply_to class c_rule r,
bool  skip_renaming = false
const
 

Apply this binding to a rule.

Parameters:
r the rule to apply the unifier to.
skip_renaming are we doing only structural changes?

void unifier::apply_to class c_term t,
bool  skip_renaming = false
const
 

Apply this binding to a term.

Parameters:
t the term to apply the unifier to.
skip_renaming are we doing only structural changes?

bool unifier::unify const class c_rule r1,
const class c_rule r2
 

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.

Parameters:
r1 the first rule.
r2 the second rule.
Returns:
Do they unify? If this is false, the unifier must not be used.

bool unifier::unify const class c_term t1,
const class c_term t2
 

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.

Parameters:
t1 the first term.
t2 the second term.
Returns:
Do they unify? If this is false, the unifier must not be used.


Friends And Related Function Documentation

std::ostream& operator<< std::ostream &  os,
const unifier u
[friend]
 

Write a text representation of this unifier to an ostream.

Parameters:
os the ostream to write to.
u the unifier to write.


Member Data Documentation

std::map<std::string, c_term*> unifier::bindings [private]
 

int unifier::count = 0 [static]
 

The number of unifiers allocated and not destroyed.


The documentation for this class was generated from the following files:
Generated on Mon Mar 21 00:08:47 2005 for Fixpoint Engine by  doxygen 1.3.9.1