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	unify (Term *, Term *)
	Implementation of unification for a pair of Terms.
UnificationOutcome	unify_terms (Term *, Term *)
	Main method implementing the traditional unification algorithm.
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 &l1, const Literal &l2)
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: for the polynomial-time approach. All the real work happens here.

Private Attributes
Substitution	s
	Build the resulting substitution here.
vector< 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" and "unify_terms" methods, depending on whether you're using the traditional or polynomial time version.

For the polynomial time version, 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 vector, taking something from the end and placing any results on the end as well.

The traditional version is based on Figure 1, page 454, Handbook of Automated Reasoning Volume 1.

Note that some modifications have to be made compared with the original presentations, because the method used to make substitutions takes immediate effect. As a result, for example, 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 89 of file Unifier.hpp.

Constructor & Destructor Documentation

Unifier() [1/2]

Unifier::Unifier ( )

inline

There isn't really much to initialize.

Definition at line 108 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 195 of file Unifier.cpp.

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

complete_unification()

UnificationOutcome Unifier::complete_unification ( )

private

Implementation of unification: for the polynomial-time approach. All the real work happens here.

Definition at line 127 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.back());
        Term* t1(upair.first);
        Term* t2(upair.second);
        to_do.pop_back();
 
        bool t1_is_var;
        Variable* t1v;
        Function* t1f;
        size_t t1a;
        t1 = t1->skip_leading_variables_for_unification(t1_is_var, t1v, t1f, t1a);
 
        bool t2_is_var;
        Variable* t2v;
        Function* t2f;
        size_t t2a;
        t2 = t2->skip_leading_variables_for_unification(t2_is_var, t2v, t2f, t2a);
 
        // Swap
        if (!t1_is_var && t2_is_var) {
            to_do.push_back(UPair(t2, t1));
            continue;
        }
 
        // Delete
        if (t1->subbed_equal(t2)) {
            continue;
        }
 
        // Decompose/Conflict
        if (!t1_is_var && !t2_is_var) {
            // Conflict
            if ((t1f != t2f) ||
                (t1a != t2a)) {
                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;
            }
        }
 
        bool contains = t2->contains_variable(t1v);
        
        // Eliminate
        if (t1_is_var && !contains) {
            s.push_back(t1v, t2);
            t1v->substitute(t2);
            continue;
        }
 
        // Occurs
        if (t1_is_var && !t2_is_var && contains) {
            backtrack();
            return UnificationOutcome::OccursFail;
        }
    }
    return UnificationOutcome::Succeed;
}

get_substitution()

Substitution Unifier::get_substitution ( ) const

inline

Trivial get methods for the result.

Definition at line 122 of file Unifier.hpp.

{ return s; }

operator()() [1/4]

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

inline

Unification of Literals.

This is the version that is used most of the time, so there is an attempt here to optimize it.

Parameters

l1	Reference to first Literal
l2	Reference to second Literal

Definition at line 168 of file Unifier.hpp.

                                                                               {
        if (params::poly_unification) {
            to_do.clear();
            size_t s = l1.get_arity();
            for (size_t i = 0; i < s; i++) {
                to_do.push_back(UPair(l1[i], l2[i]));
            }
            return complete_unification();
        }
        else {
            auto i = l1.get_args().begin();
            for (Term* term1 : l2.get_args()) {
                UnificationOutcome outcome = unify_terms(term1, *i);
                if (outcome != UnificationOutcome::Succeed) {
                    backtrack();
                    return outcome;
                }
                i++;
            }   
            return UnificationOutcome::Succeed;
        }
    }

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 88 of file Unifier.cpp.

                                                                 {
    if (t1s.size() != t2s.size())
        return UnificationOutcome::ConflictFail;
    if (params::poly_unification) {
        to_do.clear();
        auto i = t2s.begin();
        for (Term* term1 : t1s) {
            to_do.push_back(UPair(term1, *i));
            i++;
        }    
        return complete_unification();
    }
    else {
        auto i = t2s.begin();
        for (Term* term1 : t1s) {
            UnificationOutcome outcome = unify_terms(term1, *i);
            if (outcome != UnificationOutcome::Succeed) {
                backtrack();
                return outcome;
            }
            i++;
        }
        return UnificationOutcome::Succeed;
    }
}

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 115 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.

Parameters

term1	Pointer to first term
term2	Pointer to second term

Definition at line 27 of file Unifier.cpp.

                                                               {
    if (params::poly_unification) {
        to_do.clear();
        to_do.push_back(UPair(term1, term2));
        return complete_unification();
    }
    else {
        return unify_terms(term1, term2);
    }
}

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 200 of file Unifier.hpp.

                                                {
        return s.to_string(subbed);
    }

unify()

UnificationOutcome Unifier::unify	(	Term *	t1,
		Term *	t2 )

Implementation of unification for a pair of Terms.

Parameters

term1	Pointer to first term
term2	Pointer to second term

Definition at line 38 of file Unifier.cpp.

                                                    {
    UnificationOutcome outcome = unify_terms(t1, t2);
    if (outcome != UnificationOutcome::Succeed) {
        backtrack();
    }
    return outcome;
}

unify_terms()

UnificationOutcome Unifier::unify_terms	(	Term *	t1,
		Term *	t2 )

Main method implementing the traditional unification algorithm.

Definition at line 48 of file Unifier.cpp.

                                                          {
    bool t1_is_var;
    Variable* t1v;
    Function* t1f;
    size_t t1a;
    t1 = t1->skip_leading_variables_for_unification(t1_is_var, t1v, t1f, t1a);
    
    bool t2_is_var;
    Variable* t2v;
    Function* t2f;
    size_t t2a;
    t2 = t2->skip_leading_variables_for_unification(t2_is_var, t2v, t2f, t2a);
 
    if (t1_is_var && t1v == t2v) {}
    else if (!t1_is_var && !t2_is_var) {
        if (t1f == t2f && t1a == t2a) {
            for (size_t i = 0; i < t1a; i++) {
                UnificationOutcome outcome = unify_terms((*t1)[i], (*t2)[i]);
                if (outcome != UnificationOutcome::Succeed) {
                    return outcome;
                }
            }
        }
        else {
            return UnificationOutcome::ConflictFail;
        }
    }
    else if (!t1_is_var) {
        return unify_terms(t2, t1);
    }
    else if (t2->contains_variable(t1v)) {
        return UnificationOutcome::OccursFail;
    }
    else {
        s.push_back(t1v, t2);
        t1v->substitute(t2);
    }
    return UnificationOutcome::Succeed;
}

Friends And Related Symbol Documentation

operator<<

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

friend

Definition at line 218 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 94 of file Unifier.hpp.

to_do

vector<UPair> Unifier::to_do

private

Queue used by complete_unification method.

Definition at line 98 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