Unifier Class Reference

Wrap up various applications of unificiation into a single class: all the unification you need to do happens here. More...

#include <Unifier.hpp>

Public Member Functions
	Unifier ()
	There isn't really much to initialize.
	Unifier (const Unifier &)=delete
	You really only need one Unifier!
	Unifier (const Unifier &&)=delete
Unifier &	operator= (const Unifier &)=delete
Unifier &	operator= (const Unifier &&)=delete
Substitution	get_substitution () const
	Trivial get methods for the result.
UnificationOutcome	operator() (Term *, Term *)
	Implementation of unification for a pair of Terms.
UnificationOutcome	operator() (const vector< Term * > &, const vector< Term * > &)
	The same as the main operator(), but you've already extracted the arguments for the things of interest into lists.
UnificationOutcome	operator() (Literal *, Literal *)
	Unification of Literals.
UnificationOutcome	operator() (const Literal &, const Literal &)
void	backtrack ()
	Apply the backtracking process to the substitution that has been constructed.
string	to_string (bool subbed=false) const
	Make a nice string representation.

Friends
ostream &	operator<< (ostream &, const Unifier &)

Detailed Description

Wrap up various applications of unificiation into a single class: all the unification you need to do happens here.

You may find yourself unifying Terms, Literals and so on. This puts it all in one place. The class is a function class with various overloaded operator() methods.

All the real work happens in the "complete_unification" method.

See the Wikipedia page. This is apparently due to Montelli and Montanari (1982). Looking at "An Efficient Unification Algorithm – yes, indeed it is. The algorithm as stated in the paper is nondeterministic, and apparently you get a bunch of different outcomes depending on the details of the implementation.

So: this one uses a queue, taking something from the end and placing any results at the beginning.

Note that some modifications have to be made compared with the paper's presentation, because the method used to make substitutions takes immediate effect. As a result, substitutions get removed by the Delete rule, so you might as well remove them immediately. Also, when substituting x=? you don't need to check whether x appears in the other equations.

Constructor & Destructor Documentation

Unifier()

Unifier::Unifier ( const Unifier &  )

delete

You really only need one Unifier!

As always, copying is a bad idea so let the compiler help you out.

Member Function Documentation

operator()() [1/4]

UnificationOutcome Unifier::operator()	(	const Literal &	l1,
		const Literal &	l2
	)

Unification of Literals.

Parameters

l1	Reference to first Literal
l2	Reference to second Literal

operator()() [2/4]

UnificationOutcome Unifier::operator()	(	const vector< Term * > &	t1s,
		const vector< Term * > &	t2s
	)

The same as the main operator(), but you've already extracted the arguments for the things of interest into lists.

Parameters

t1s	Reference to vector of pointers to Terms
t2s	Reference to vector of pointers to Terms

operator()() [3/4]

UnificationOutcome Unifier::operator()	(	Literal *	l1,
		Literal *	l2
	)

Unification of Literals.

Parameters

l1	Pointer to first Literal
l2	Pointer to second Literal

operator()() [4/4]

UnificationOutcome Unifier::operator()	(	Term *	term1,
		Term *	term2
	)

Implementation of unification for a pair of Terms.

See the Wikipedia page. This is apparently due to Montelli and Montanari (1982). Looking at "An Efficient Unification Algorithm – yes, indeed it is.

See also the documentation for complete_unification.

Parameters

term1	Pointer to first term
term2	Pointer to second term

to_string()

string Unifier::to_string ( bool  subbed = false ) const

inline

Make a nice string representation.

Parameters

subbed

Use substitutions if true.

---

The documentation for this class was generated from the following files:

• Unifier.hpp
• Unifier.cpp