Substitution Class Reference

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	make_LaTeX (bool=false) const
	Make a useable LaTeX 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 &, const Substitution &)

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.

: sub() {}

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 56 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 62 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 117 of file Substitution.hpp.

{ return sub.begin(); }

cbegin()

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

inline

Iteration is just iteration over the vector of pairs.

Definition at line 125 of file Substitution.hpp.

{ return sub.cbegin(); }

cend()

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

inline

Iteration is just iteration over the vector of pairs.

Definition at line 129 of file Substitution.hpp.

{ return sub.cend(); }

clear()

void Substitution::clear ( )

inline

Clear a substitution.

Definition at line 85 of file Substitution.hpp.

{ sub.clear(); }

end()

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

inline

Iteration is just iteration over the vector of pairs.

Definition at line 121 of file Substitution.hpp.

{ return sub.end(); }

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 39 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 52 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.

{ 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;
}

Friends And Related Symbol Documentation

operator<<

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

friend

Definition at line 68 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++/v0.5.0/source/substitution/Substitution.hpp
• /Users/sbh11/Desktop/connection-prover/c++/connect++/v0.5.0/source/substitution/Substitution.cpp