General representation of a substitution. More...

#include <Substitution.hpp>

Collaboration diagram for Substitution:

Public Member Functions
	Substitution ()
	Trivial constructor.

size_t	size () const
	Trivial get method.

void	push_back (Variable , Term )
	Add a pair to a substitution.

void	clear ()
	Clear a substitution.

void	apply () const
	Apply a substitution everywhere.

void	backtrack () const
	Remove a substitution everywhere.

string	to_string (bool=false) const
	Make a string representation.

string	to_tptp_string (bool=false) const
	Make a string representation in the TPTP format.

string	make_LaTeX (bool=false) const
	Make a useable LaTeX representation.

string	make_Graphviz (bool=false) const
	Make a useable Graphviz representation.

vector< SubPair >::iterator	begin ()
	Iteration is just iteration over the vector of pairs.

vector< SubPair >::iterator	end ()
	Iteration is just iteration over the vector of pairs.

vector< SubPair >::const_iterator	cbegin ()
	Iteration is just iteration over the vector of pairs.

vector< SubPair >::const_iterator	cend ()
	Iteration is just iteration over the vector of pairs.

Private Attributes
vector< SubPair >	sub
	A single substitution is just a pointer to the Variable being sustituted, and a pointer to the Term to use. The Substitution is just a vector of those.

Friends
ostream &	operator<< (ostream &out, const Substitution &s)

Detailed Description

General representation of a substitution.

This is just a vector of individual substitutions, each a pair of pointers, one to the Variable and one to the Term.

Only very minimal methods are needed, essentially for applying and removing the substitutions.

Definition at line 57 of file Substitution.hpp.

Constructor & Destructor Documentation

◆ Substitution()

Substitution::Substitution ( )

inline

Trivial constructor.

Definition at line 70 of file Substitution.hpp.

70: sub() {}

Substitution::sub

vector< SubPair > sub

A single substitution is just a pointer to the Variable being sustituted, and a pointer to the Term t...

Definition Substitution.hpp:65

Member Function Documentation

◆ apply()

void Substitution::apply ( ) const

Apply a substitution everywhere.

Because of the way terms are represented this is easy, and involves updating a single pointer for each variable.

Definition at line 85 of file Substitution.cpp.

                               {
    for (SubPair s : sub) {
        s.first->substitute(s.second);
    }
}

◆ backtrack()

void Substitution::backtrack ( ) const

Remove a substitution everywhere.

Because of the way terms are represented this is easy, and involves updating a single pointer for each variable.

Definition at line 91 of file Substitution.cpp.

                                   {
    for (SubPair s : sub) {
        s.first->remove_substitution();
    }
}

◆ begin()

vector< SubPair >::iterator Substitution::begin ( )

inline

Iteration is just iteration over the vector of pairs.

Definition at line 130 of file Substitution.hpp.

130{ return sub.begin(); }

◆ cbegin()

vector< SubPair >::const_iterator Substitution::cbegin ( )

inline

Iteration is just iteration over the vector of pairs.

Definition at line 138 of file Substitution.hpp.

138{ return sub.cbegin(); }

◆ cend()

vector< SubPair >::const_iterator Substitution::cend ( )

inline

Iteration is just iteration over the vector of pairs.

Definition at line 142 of file Substitution.hpp.

142{ return sub.cend(); }

◆ clear()

void Substitution::clear ( )

inline

Clear a substitution.

Definition at line 85 of file Substitution.hpp.

85{ sub.clear(); }

◆ end()

vector< SubPair >::iterator Substitution::end ( )

inline

Iteration is just iteration over the vector of pairs.

Definition at line 134 of file Substitution.hpp.

134{ return sub.end(); }

◆ make_Graphviz()

string Substitution::make_Graphviz ( bool subbed = false ) const

Make a useable Graphviz representation.

Parameters

subbed Implement substitutions if true.

Definition at line 66 of file Substitution.cpp.

                                                    {
  commas::comma com(sub.size());
  string result ("( ");
  for (SubPair s : sub) {
    result += s.first->make_Graphviz();
    result += " ";
    result += unicode_symbols::LogSym::subbed;
    result += " ";
    result += s.second->make_Graphviz(subbed);
    result += com();
  }
  result += " )";
  return result;
}

◆ make_LaTeX()

string Substitution::make_LaTeX ( bool subbed = false ) const

Make a useable LaTeX representation.

Assumes you're in Math Mode.

Parameters

subbed Implement substitutions if true.

Definition at line 53 of file Substitution.cpp.

                                                 {
  commas::comma com(sub.size());
  string result ("( ");
  for (SubPair s : sub) {
    result += s.first->make_LaTeX();
    result += " \\leftarrow ";
    result += s.second->make_LaTeX(subbed);
    result += com();
  }
  result += " )";
  return result;
}

◆ push_back()

void Substitution::push_back	(	Variable *	v,
		Term *	t )

Add a pair to a substitution.

Parameters

v	Pointer to the Variable.
t	Pointer to the Term.

Definition at line 81 of file Substitution.cpp.

                                                 {
    sub.push_back(SubPair(v, t));
}

◆ size()

size_t Substitution::size ( ) const

inline

Trivial get method.

Definition at line 74 of file Substitution.hpp.

74{ return sub.size(); }

◆ to_string()

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

Make a string representation.

Parameters

subbed Implement substitutions if true.

Definition at line 28 of file Substitution.cpp.

                                                {
    string result("\n");
    for (SubPair s : sub) {
        result += s.first->to_string();
        result += " <- ";
        result += s.second->to_string(subbed);
        result += '\n';
    }
    return result;
}

◆ to_tptp_string()

string Substitution::to_tptp_string ( bool subbed = false ) const

Make a string representation in the TPTP format.

Apply substitutions (not to variable being substituted!) if argument is true.

Definition at line 39 of file Substitution.cpp.

                                                     {
    commas::comma com(sub.size());
    string result;
    for (SubPair s : sub) {
        result += "bind(";
        result += s.first->to_prolog_string(false);
        result += ", ";
        result += s.second->to_prolog_string(subbed);
        result += ")";
        result += com();
    }
    return result;
}

Friends And Related Symbol Documentation

◆ operator<<

ostream & operator<<	(	ostream &	out,
		const Substitution &	s )

friend

Definition at line 97 of file Substitution.cpp.

                                                         {
  colour_string::ColourString cs(params::use_colours);
  for (SubPair sp : s.sub) {
      out << cs("(").orange() << sp.first->to_string();
      out << cs(" -> ").orange();
      out << sp.second->to_string() << cs(") ").orange();
  }
  return out;
}

Member Data Documentation

◆ sub

vector<SubPair> Substitution::sub

private

A single substitution is just a pointer to the Variable being sustituted, and a pointer to the Term to use. The Substitution is just a vector of those.

Definition at line 65 of file Substitution.hpp.

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

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

Public Member Functions

Private Attributes

Friends

Detailed Description

Constructor & Destructor Documentation

◆ Substitution()

Member Function Documentation

◆ apply()

◆ backtrack()

◆ begin()

◆ cbegin()

◆ cend()

◆ clear()

◆ end()

◆ make_Graphviz()

◆ make_LaTeX()

◆ push_back()

◆ size()

◆ to_string()

◆ to_tptp_string()

Friends And Related Symbol Documentation

◆ operator<<

Member Data Documentation

◆ sub