#include <Bindings.h>

Inheritance diagram for knowrob::Bindings:

Collaboration diagram for knowrob::Bindings:

Public Types
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 >

Public Member Functions
	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

Static Public Member Functions
static std::shared_ptr< const Bindings >	emptyBindings ()

static std::shared_ptr< const Bindings >	emptyBindings ()

Protected Attributes
Map	mapping_

Detailed Description

A substitution is a mapping from variable names to terms. For example, {x1 -> t1, ..., xn -> tn} represents a substitution of each variable xi with the corresponding term ti. Applying a substitution to a term t means to replace occurrences of each xi with ti. The resulting term is referred to as an instance of t.

Definition at line 28 of file Bindings.h.

Member Typedef Documentation

◆ Map [1/2]

using knowrob::Bindings::Map = std::map<std::string_view, std::pair<std::shared_ptr<Variable>, TermPtr> >

A mapping from variable names to terms.

Definition at line 33 of file Bindings.h.

◆ Map [2/2]

using knowrob::Bindings::Map = std::map<std::string_view, std::pair<std::shared_ptr<Variable>, TermPtr> >

A mapping from variable names to terms.

Definition at line 33 of file Bindings.h.

◆ VarMap [1/2]

using knowrob::Bindings::VarMap = std::map<std::shared_ptr<Variable>, TermPtr>

Definition at line 34 of file Bindings.h.

◆ VarMap [2/2]

using knowrob::Bindings::VarMap = std::map<std::shared_ptr<Variable>, TermPtr>

Definition at line 34 of file Bindings.h.

Constructor & Destructor Documentation

◆ Bindings() [1/4]

knowrob::Bindings::Bindings ( )

default

◆ Bindings() [2/4]

Bindings::Bindings ( const std::map< std::shared_ptr< Variable >, TermPtr > & mapping )

explicit

Parameters

mapping a mapping from variables to terms.

Definition at line 22 of file Bindings.cpp.

                                                                           {
     for (const auto &pair: mapping) {
         set(pair.first, pair.second);
     }
 }

◆ ~Bindings() [1/2]

knowrob::Bindings::~Bindings ( )

overridedefault

◆ Bindings() [3/4]

knowrob::Bindings::Bindings ( )

default

◆ Bindings() [4/4]

knowrob::Bindings::Bindings ( const std::map< std::shared_ptr< Variable >, TermPtr > & mapping )

explicit

Parameters

mapping a mapping from variables to terms.

◆ ~Bindings() [2/2]

knowrob::Bindings::~Bindings ( )

overridedefault

Member Function Documentation

◆ begin() [1/2]

auto knowrob::Bindings::begin ( ) const

inline

Returns: begin iterator of substitution.

Definition at line 70 of file Bindings.h.

70 { return mapping_.begin(); }

knowrob::Bindings::mapping_

Map mapping_

Definition: Bindings.h:147

◆ begin() [2/2]

auto knowrob::Bindings::begin ( ) const

inline

Returns: begin iterator of substitution.

Definition at line 70 of file Bindings.h.

70 { return mapping_.begin(); }

◆ contains() [1/2]

bool Bindings::contains ( std::string_view varName ) const

Returns true if the given var is mapped to a term by this substitution.

Parameters

varName a variable.

Returns: true if this substitution isMoreGeneralThan the variable.

Definition at line 56 of file Bindings.cpp.

                                                     {
     return mapping_.find(varName) != mapping_.end();
 }

◆ contains() [2/2]

bool knowrob::Bindings::contains ( std::string_view varName ) const

Returns true if the given var is mapped to a term by this substitution.

Parameters

varName a variable.

Returns: true if this substitution isMoreGeneralThan the variable.

◆ empty() [1/2]

bool knowrob::Bindings::empty ( ) const

inline

Returns: true if this substitution does not map a single variable to a term.

Definition at line 60 of file Bindings.h.

60 { return mapping_.empty(); }

◆ empty() [2/2]

bool knowrob::Bindings::empty ( ) const

inline

Returns: true if this substitution does not map a single variable to a term.

Definition at line 60 of file Bindings.h.

60 { return mapping_.empty(); }

◆ emptyBindings() [1/2]

std::shared_ptr< const Bindings > Bindings::emptyBindings ( )

static

Returns: a const empty substitution.

Definition at line 99 of file Bindings.cpp.

                                                       {
     static const auto empty = std::make_shared<Bindings>();
     return empty;
 }

◆ emptyBindings() [2/2]

static std::shared_ptr<const Bindings> knowrob::Bindings::emptyBindings ( )

static

Returns: a const empty substitution.

◆ end() [1/2]

auto knowrob::Bindings::end ( ) const

inline

Returns: end iterator of substitution.

Definition at line 75 of file Bindings.h.

75 { return mapping_.end(); }

◆ end() [2/2]

auto knowrob::Bindings::end ( ) const

inline

Returns: end iterator of substitution.

Definition at line 75 of file Bindings.h.

75 { return mapping_.end(); }

◆ find() [1/2]

auto knowrob::Bindings::find ( std::string_view varName ) const

inline

Returns: a const iterator to the variable-term mapping.

Definition at line 80 of file Bindings.h.

80 { return mapping_.find(varName); }

◆ find() [2/2]

auto knowrob::Bindings::find ( std::string_view varName ) const

inline

Returns: a const iterator to the variable-term mapping.

Definition at line 80 of file Bindings.h.

80 { return mapping_.find(varName); }

◆ get() [1/2]

const TermPtr & Bindings::get ( std::string_view varName ) const

Map the name of a variable to a term. A null pointer reference is returned if the given variable is not included in the mapping.

Parameters

varName a variable.

Returns: a term reference.

Definition at line 60 of file Bindings.cpp.

                                                          {
     static const TermPtr null_term;
  
     auto it = mapping_.find(varName);
     if (it != mapping_.end()) {
         return it->second.second;
     } else {
         return null_term;
     }
 }

◆ get() [2/2]

const TermPtr& knowrob::Bindings::get ( std::string_view varName ) const

Map the name of a variable to a term. A null pointer reference is returned if the given variable is not included in the mapping.

Parameters

varName a variable.

Returns: a term reference.

◆ getAtomic() [1/2]

std::shared_ptr< Atomic > Bindings::getAtomic ( std::string_view varName ) const

Map the name of a variable to a term. A null pointer reference is returned if the given variable is not included in the mapping.

Parameters

varName a variable.

Returns: a term reference.

Definition at line 71 of file Bindings.cpp.

                                                                       {
     static const std::shared_ptr<Atomic> null_term;
  
     auto term = get(varName);
     if (term && term->termType() == TermType::ATOMIC) {
         return std::static_pointer_cast<Atomic>(term);
     } else {
         return null_term;
     }
 }

◆ getAtomic() [2/2]

std::shared_ptr<Atomic> knowrob::Bindings::getAtomic ( std::string_view varName ) const

Map the name of a variable to a term. A null pointer reference is returned if the given variable is not included in the mapping.

Parameters

varName a variable.

Returns: a term reference.

◆ hash() [1/2]

size_t Bindings::hash ( ) const

Returns: the hash of this.

Definition at line 82 of file Bindings.cpp.

                             {
     auto seed = static_cast<size_t>(0);
  
     for (const auto &item: mapping_) {
         // Compute the hash of the key using the in-built hash function for string.
         hashCombine(seed, std::hash<std::string_view>{}(item.first));
  
         auto value_hash = static_cast<size_t>(0);
         if (item.second.second) {
             value_hash = item.second.second->hash();
         }
         hashCombine(seed, value_hash);
     }
  
     return seed;
 }

◆ hash() [2/2]

size_t knowrob::Bindings::hash ( ) const

Returns: the hash of this.

◆ isConsistentWith() [1/2]

bool Bindings::isConsistentWith ( const Bindings & other ) const

Check if this substitution is consistent with another substitution, i.e. if both can be unified.

Parameters

other another substitution.

Returns: true if this substitution is consistent with the other substitution.

Definition at line 104 of file Bindings.cpp.

                                                            {
     const Map *map_small;
     const Map *map_large;
     if (mapping_.size() < other.mapping_.size()) {
         map_small = &mapping_;
         map_large = &other.mapping_;
     } else {
         map_small = &other.mapping_;
         map_large = &mapping_;
     }
  
     for (const auto &pair: *map_small) {
         auto it = map_large->find(pair.first);
         if (it != map_large->end()) {
             auto t0 = pair.second.second;
             auto t1 = it->second.second;
             Unifier sigma(t0, t1);
             if (!sigma.exists()) {
                 return false;
             }
         }
     }
  
     return true;
 }

◆ isConsistentWith() [2/2]

bool knowrob::Bindings::isConsistentWith ( const Bindings & other ) const

Check if this substitution is consistent with another substitution, i.e. if both can be unified.

Parameters

other another substitution.

Returns: true if this substitution is consistent with the other substitution.

◆ operator+=() [1/2]

void Bindings::operator+= ( const Bindings & other )

Combine with another substitution.

Parameters

other another substitution.

Definition at line 46 of file Bindings.cpp.

                                                {
     for (auto &x: other.mapping_) {
         set(x.second.first, x.second.second);
     }
 }

◆ operator+=() [2/2]

void knowrob::Bindings::operator+= ( const Bindings & other )

Combine with another substitution.

Parameters

other another substitution.

◆ operator==() [1/2]

bool Bindings::operator== ( const Bindings & other ) const

Parameters

other another substitution.

Returns: true if this substitution is equal to the other substitution.

Definition at line 28 of file Bindings.cpp.

                                                      {
     if (mapping_.size() != other.mapping_.size()) {
         return false;
     }
  
     for (auto &x: mapping_) {
         auto &val1 = x.second.second;
         auto &val2 = other.get(x.first);
         if (val1 && val2) {
             if (!(*val1 == *val2)) return false;
         } else if (val1 || val2) {
             return false;
         }
     }
  
     return true;
 }

◆ operator==() [2/2]

bool knowrob::Bindings::operator== ( const Bindings & other ) const

Parameters

other another substitution.

Returns: true if this substitution is equal to the other substitution.

◆ set() [1/2]

void Bindings::set	(	const std::shared_ptr< Variable > &	var,
		const TermPtr &	term
	)

Map a variable to a term.

Parameters

var	a variable.
term	a term.

Definition at line 52 of file Bindings.cpp.

                                                                           {
     mapping_.insert({var->name(), {var, term}});
 }

◆ set() [2/2]

void knowrob::Bindings::set	(	const std::shared_ptr< Variable > &	var,
		const TermPtr &	term
	)

Map a variable to a term.

Parameters

var	a variable.
term	a term.

◆ size() [1/2]

auto knowrob::Bindings::size ( ) const

inline

Returns: number of variables mapped to terms.

Definition at line 65 of file Bindings.h.

65 { return mapping_.size(); }

◆ size() [2/2]

auto knowrob::Bindings::size ( ) const

inline

Returns: number of variables mapped to terms.

Definition at line 65 of file Bindings.h.

65 { return mapping_.size(); }

◆ unifyWith() [1/2]

bool Bindings::unifyWith ( const Bindings & other )

Combine with another substitution. If both substitute the same variable to some term, then the combination maps to the unification of these terms, if one exists.

Parameters

other another substitution

Returns: true if the operation succeeded.

Definition at line 130 of file Bindings.cpp.

                                               {
     for (const auto &pair: other.mapping_) {
         auto it = mapping_.find(pair.first);
         if (it == mapping_.end()) {
             // new variable instantiation
             mapping_.insert(pair);
         } else {
             // variable has already an instantiation, need to unify
             TermPtr t0 = it->second.second;
             TermPtr t1 = pair.second.second;
  
             // t0 and t1 are not syntactically equal -> compute a unifier
             Unifier sigma(t0, t1);
             if (sigma.exists()) {
                 // a unifier exists
                 it->second.second = sigma.apply();
             } else {
                 // no unifier exists
                 return false;
             }
         }
     }
  
     return true;
 }

◆ unifyWith() [2/2]

bool knowrob::Bindings::unifyWith ( const Bindings & other )

Combine with another substitution. If both substitute the same variable to some term, then the combination maps to the unification of these terms, if one exists.

Parameters

other another substitution

Returns: true if the operation succeeded.

◆ write() [1/2]

void Bindings::write ( std::ostream & os ) const

overridevirtual

Print this object to a stream.

Parameters

os	the stream to print to.

Implements knowrob::Printable.

Definition at line 156 of file Bindings.cpp.

                                          {
     uint32_t i = 0;
     os << '{';
     for (const auto &pair: mapping_) {
         if (i++ > 0) os << ',';
         os << pair.first << ':' << ' ' << (*pair.second.second);
     }
     os << '}';
 }

◆ write() [2/2]

void knowrob::Bindings::write ( std::ostream & os ) const

overridevirtual

Print this object to a stream.

Parameters

os	the stream to print to.

Implements knowrob::Printable.

Member Data Documentation

◆ mapping_

Map knowrob::Bindings::mapping_

protected

Definition at line 147 of file Bindings.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/Bindings.h
src/terms/Bindings.cpp

Public Types

Public Member Functions

Static Public Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ Map [1/2]

◆ Map [2/2]

◆ VarMap [1/2]

◆ VarMap [2/2]

Constructor & Destructor Documentation

◆ Bindings() [1/4]

◆ Bindings() [2/4]

◆ ~Bindings() [1/2]

◆ Bindings() [3/4]

◆ Bindings() [4/4]

◆ ~Bindings() [2/2]

Member Function Documentation

◆ begin() [1/2]

◆ begin() [2/2]

◆ contains() [1/2]

◆ contains() [2/2]

◆ empty() [1/2]

◆ empty() [2/2]

◆ emptyBindings() [1/2]

◆ emptyBindings() [2/2]

◆ end() [1/2]

◆ end() [2/2]

◆ find() [1/2]

◆ find() [2/2]

◆ get() [1/2]

◆ get() [2/2]

◆ getAtomic() [1/2]

◆ getAtomic() [2/2]

◆ hash() [1/2]

◆ hash() [2/2]

◆ isConsistentWith() [1/2]

◆ isConsistentWith() [2/2]

◆ operator+=() [1/2]

◆ operator+=() [2/2]

◆ operator==() [1/2]

◆ operator==() [2/2]

◆ set() [1/2]

◆ set() [2/2]

◆ size() [1/2]

◆ size() [2/2]

◆ unifyWith() [1/2]

◆ unifyWith() [2/2]

◆ write() [1/2]

◆ write() [2/2]

Member Data Documentation

◆ mapping_