knowrob::Unifier Class Reference

#include <Unifier.h>

Inheritance diagram for knowrob::Unifier:

Collaboration diagram for knowrob::Unifier:

Public Member Functions
	Unifier (const TermPtr &t0, const TermPtr &t1)
bool	exists () const
TermPtr	apply ()
	Unifier (const TermPtr &t0, const TermPtr &t1)
bool	exists () const
TermPtr	apply ()
Public Member Functions inherited from knowrob::Bindings
	Bindings ()=default
	Bindings (const std::map< std::shared_ptr< Variable >, TermPtr > &mapping)
	~Bindings () override=default
bool	operator== (const Bindings &other) const
void	operator+= (const Bindings &other)
bool	empty () const
auto	size () const
auto	begin () const
auto	end () const
auto	find (std::string_view varName) const
void	set (const std::shared_ptr< Variable > &var, const TermPtr &term)
const TermPtr &	get (std::string_view varName) const
std::shared_ptr< Atomic >	getAtomic (std::string_view varName) const
bool	contains (std::string_view varName) const
bool	unifyWith (const Bindings &other)
bool	isConsistentWith (const Bindings &other) const
size_t	hash () const
void	write (std::ostream &os) const override
	Bindings ()=default
	Bindings (const std::map< std::shared_ptr< Variable >, TermPtr > &mapping)
	~Bindings () override=default
bool	operator== (const Bindings &other) const
void	operator+= (const Bindings &other)
bool	empty () const
auto	size () const
auto	begin () const
auto	end () const
auto	find (std::string_view varName) const
void	set (const std::shared_ptr< Variable > &var, const TermPtr &term)
const TermPtr &	get (std::string_view varName) const
std::shared_ptr< Atomic >	getAtomic (std::string_view varName) const
bool	contains (std::string_view varName) const
bool	unifyWith (const Bindings &other)
bool	isConsistentWith (const Bindings &other) const
size_t	hash () const
void	write (std::ostream &os) const override
Public Member Functions inherited from knowrob::Printable
virtual	~Printable ()=default
virtual std::string	format () const
virtual	~Printable ()=default
virtual std::string	format () const

Protected Member Functions
bool	unify (const TermPtr &t0, const TermPtr &t1)
bool	unify (const std::shared_ptr< Variable > &var, const TermPtr &t)
bool	unify (const TermPtr &t0, const TermPtr &t1)
bool	unify (const std::shared_ptr< Variable > &var, const TermPtr &t)

Protected Attributes
TermPtr	t0_
TermPtr	t1_
bool	exists_
Protected Attributes inherited from knowrob::Bindings
Map	mapping_

Additional Inherited Members
Public Types inherited from knowrob::Bindings
using	Map = std::map< std::string_view, std::pair< std::shared_ptr< Variable >, TermPtr > >
using	VarMap = std::map< std::shared_ptr< Variable >, TermPtr >
using	Map = std::map< std::string_view, std::pair< std::shared_ptr< Variable >, TermPtr > >
using	VarMap = std::map< std::shared_ptr< Variable >, TermPtr >
Static Public Member Functions inherited from knowrob::Bindings
static std::shared_ptr< const Bindings >	emptyBindings ()
static std::shared_ptr< const Bindings >	emptyBindings ()

Detailed Description

A substitution that unifies some terms.

Definition at line 18 of file Unifier.h.

Constructor & Destructor Documentation

Unifier() [1/2]

Unifier::Unifier	(	const TermPtr &	t0,
		const TermPtr &	t1
	)

Compute a unifier of two terms.

Parameters

t0	a term.
t1	a term.

Definition at line 16 of file Unifier.cpp.

        : Bindings(),
          t0_(t0),
          t1_(t1),
          exists_(unify(t0, t1)) {
}

Unifier() [2/2]

knowrob::Unifier::Unifier	(	const TermPtr &	t0,
		const TermPtr &	t1
	)

Compute a unifier of two terms.

Parameters

t0	a term.
t1	a term.

Member Function Documentation

apply() [1/2]

TermPtr Unifier::apply

(

)

Applies the unifier to one of the unified terms.

Returns

an instance of the unified terms.

Definition at line 74 of file Unifier.cpp.

                       {
    if (!exists_) {
        // no unifier exists
        return Bottom::get()->functor();
    } else if (t0_->isGround() || t1_->termType() == TermType::VARIABLE) {
        // empty unifier, or only substitutions in t1
        return t0_;
    } else if (t1_->isGround() || t0_->termType() == TermType::VARIABLE) {
        // only substitutions in t0
        return t1_;
    } else if (t0_->termType() == TermType::FUNCTION) {
        // both t0_ and t1_ contain variables.
        auto &p = (
                t0_->variables().size() < t1_->variables().size() ?
                t0_ : t1_);
        return applyBindings(p, *this);
    } else {
        KB_WARN("something went wrong during unification.");
        return Bottom::get()->functor();
    }
}

apply() [2/2]

TermPtr knowrob::Unifier::apply

(

)

Applies the unifier to one of the unified terms.

Returns

an instance of the unified terms.

exists() [1/2]

bool knowrob::Unifier::exists ( ) const

inline

Returns

true is a unifier exists.

Definition at line 30 of file Unifier.h.

{ return exists_; }

exists() [2/2]

bool knowrob::Unifier::exists ( ) const

inline

Returns

true is a unifier exists.

Definition at line 30 of file Unifier.h.

{ return exists_; }

unify() [1/4]

bool Unifier::unify ( const std::shared_ptr< Variable > &  var, const TermPtr &  t  )

protected

Definition at line 60 of file Unifier.cpp.

                                                                        {
#ifdef USE_OCCURS_CHECK
    if (t->variables().find(var->name()) != t->variables().end()) {
        // fail if var *occurs* in t (occurs check)
        return false;
    } else {
#endif
        set(var, t);
        return true;
#ifdef USE_OCCURS_CHECK
    }
#endif
}

unify() [2/4]

bool knowrob::Unifier::unify ( const std::shared_ptr< Variable > &  var, const TermPtr &  t  )

protected

unify() [3/4]

bool Unifier::unify ( const TermPtr &  t0, const TermPtr &  t1  )

protected

Definition at line 23 of file Unifier.cpp.

{
    if (t1->termType() == TermType::VARIABLE) {
        return unify(std::static_pointer_cast<Variable>(t1), t0);
    } else {
        switch (t0->termType()) {
            case TermType::VARIABLE:
                return unify(std::static_pointer_cast<Variable>(t0), t1);
            case TermType::ATOMIC:
                // if one of the terms is an atomic, the other must be an equal atomic
                return *t0 == *t1;
            case TermType::FUNCTION: {
                // n-ary functions with n>0 only unify with other n-ary functions
                if (t1->termType() != TermType::FUNCTION) {
                    return false;
                }
                auto *p0 = (Function *) t0.get();
                auto *p1 = (Function *) t1.get();
                // tests for functor equality, and matching arity
                if (*p0->functor() != *p1->functor() ||
                    p0->arity() != p1->arity()) {
                    return false;
                }
                // unify all arguments
                for (std::size_t i = 0; i < p0->arity(); ++i) {
                    if (!unify(p0->arguments()[i], p1->arguments()[i])) {
                        return false;
                    }
                }
                break;
            }
        }
    }
 
    return true;
}

unify() [4/4]

bool knowrob::Unifier::unify ( const TermPtr &  t0, const TermPtr &  t1  )

protected

Member Data Documentation

exists_

bool knowrob::Unifier::exists_

protected

Definition at line 41 of file Unifier.h.

t0_

TermPtr knowrob::Unifier::t0_

protected

Definition at line 39 of file Unifier.h.

t1_

TermPtr knowrob::Unifier::t1_

protected

Definition at line 40 of file Unifier.h.

---

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

• build/_CPack_Packages/Linux/DEB/knowrob-2.1.0-Linux/usr/include/knowrob/terms/Unifier.h
• src/terms/Unifier.cpp