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>

Collaboration diagram for Unifier:

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.

Private Member Functions
UnificationOutcome	complete_unification ()
	Implementation of unification: all the real work happens here.

Private Attributes
Substitution	s
	Build the resulting substitution here.
deque< UPair >	to_do
	Queue used by complete_unification method.

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.

Definition at line 83 of file Unifier.hpp.

Constructor & Destructor Documentation

Unifier() [1/2]

Unifier::Unifier ( )

inline

There isn't really much to initialize.

Definition at line 102 of file Unifier.hpp.

: s(), to_do() {}

Unifier() [2/2]

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

backtrack()

void Unifier::backtrack

(

)

Apply the backtracking process to the substitution that has been constructed.

Definition at line 134 of file Unifier.cpp.

                        {
    s.backtrack();
    s.clear();
}

complete_unification()

UnificationOutcome Unifier::complete_unification ( )

private

Implementation of unification: all the real work happens here.

Definition at line 72 of file Unifier.cpp.

                                                 {
    s.clear();
    while (to_do.size() > 0) {
        // Get the next thing from the queue and split it up.
        UPair upair(to_do.front());
        Term* t1(upair.first);
        Term* t2(upair.second);
        // Make sure you do this! Many long debugging sessions
        // await if you ignore my advice.
        t1 = t1->skip_leading_variables();
        t2 = t2->skip_leading_variables();
        to_do.pop_front();
        // Work out exactly what everything is.
        bool t1_is_fun = t1->subbed_is_function();
        bool t2_is_fun = t2->subbed_is_function();
        bool t1_is_var = t1->subbed_is_variable();
        bool t2_is_var = t2->subbed_is_variable();
        Variable* t1v = nullptr;
        if (t1_is_var)
            t1v = t1->get_v()->subbed_variable();
 
        // Delete
        if (t1->subbed_equal(t2)) {
            continue;
        }
        // Swap
        if (t1_is_fun && t2_is_var) {
            to_do.push_back(UPair(t2, t1));
            continue;
        }
        // Occurs
        if (t1_is_var && t2_is_fun && t2->contains_variable(t1v)) {
            backtrack();
            return UnificationOutcome::OccursFail;
        }
        // Eliminate
        if (t1_is_var && !t2->contains_variable(t1v)) {
            s.push_back(t1v, t2);
            t1v->substitute(t2);
            continue;
        }
        // Decompose/Conflict
        if (t1_is_fun && t2_is_fun) {
            // Conflict
            if ((t1->get_subbed_f() != t2->get_subbed_f()) ||
                (t1->get_subbed_arity() != t2->get_subbed_arity())) {
                backtrack();
                return UnificationOutcome::ConflictFail;
            }
            // Decompose
            else {
                size_t n_args = t1->arity();
                for (size_t i = 0; i < n_args; i++) {
                    to_do.push_back(UPair((*t1)[i], (*t2)[i]));
                }
                continue;
            }
        }
    }
    return UnificationOutcome::Succeed;
}

get_substitution()

Substitution Unifier::get_substitution ( ) const

inline

Trivial get methods for the result.

Definition at line 116 of file Unifier.hpp.

{ return s; }

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

Definition at line 59 of file Unifier.cpp.

                                                          {
    if (!l1.is_compatible_with(&l2)) {
        cerr << "ERROR" << ": ";
        cerr << "You're trying to unify non-compatible literals." << endl;
        cerr << "ERROR" << ": " << l1 << endl;
        cerr << "ERROR" << ": " << l2 << endl;
    }
    const vector<Term*>& args1 = l1.get_args();
    const vector<Term*>& args2 = l2.get_args();
    return operator()(args1, args2);
}

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

Definition at line 34 of file Unifier.cpp.

                                                                 {
    if (t1s.size() != t2s.size())
        return UnificationOutcome::ConflictFail;
    to_do.clear();
    auto i = t2s.begin();
    for (Term* term1 : t1s) {
        to_do.push_front(UPair(term1, *i));
        i++;
    }
    return complete_unification();
}

operator()() [3/4]

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

Unification of Literals.

Parameters

l1	Pointer to first Literal
l2	Pointer to second Literal

Definition at line 47 of file Unifier.cpp.

                                                               {
    if (!l1->is_compatible_with(l2)) {
        cerr << "ERROR" << ": ";
        cerr << "You're trying to unify non-compatible literals." << endl;
        cerr << "ERROR" << ": " << *l1 << endl;
        cerr << "ERROR" << ": " << *l2 << endl;
    }
    const vector<Term*>& args1 = l1->get_args();
    const vector<Term*>& args2 = l2->get_args();
    return operator()(args1, args2);
}

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

Definition at line 28 of file Unifier.cpp.

                                                               {
    to_do.clear();
    to_do.push_front(UPair(term1, term2));
    return complete_unification();
}

to_string()

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

inline

Make a nice string representation.

Parameters

subbed

Use substitutions if true.

Definition at line 164 of file Unifier.hpp.

                                                {
        return s.to_string(subbed);
    }

Friends And Related Symbol Documentation

operator<<

ostream & operator<< ( ostream & out, const Unifier & u )

friend

Definition at line 157 of file Unifier.cpp.

                                                    {
    out << u.to_string();
    return out;
}

Member Data Documentation

s

Substitution Unifier::s

private

Build the resulting substitution here.

Definition at line 88 of file Unifier.hpp.

to_do

deque<UPair> Unifier::to_do

private

Queue used by complete_unification method.

Definition at line 92 of file Unifier.hpp.

---

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

• /Users/sbh11/Desktop/connection-prover/c++/connect++/source/substitution/Unifier.hpp
• /Users/sbh11/Desktop/connection-prover/c++/connect++/source/substitution/Unifier.cpp