Term Class Reference

General representation of terms. More...

#include <Term.hpp>

Collaboration diagram for Term:

Public Member Functions
Variable *	get_v () const
	Self-explanatory access function.
Function *	get_f () const
	Self-explanatory access function.
bool	is_variable () const
	Self-explanatory.
bool	is_function () const
	Self-explanatory.
Arity	arity () const
	Self-explanatory access function.
Term *	operator[] (size_t) const
	Access to args, but don't mess with them!
bool	is_ground () const
	Is the term ground?
string	to_string (bool=false, bool=false) const
	Make a string representation of the Term, taking into account any substitutions that have been made.
string	to_prolog_string () const
	Convert to a string that can be read by Prolog.
string	make_LaTeX (bool=false) const
	Make a useable LaTeX representation.
bool	operator== (const Term &) const
	For the TermIndex you want strict equaliity of the data members.
bool	is_subbed () const
	Test whether any variable has been substituted.
bool	subbed_equal (Term *) const
	Equality test, taking substitution into account.
bool	is_unsubbed_variable () const
	Is this a variable that hasn't been substituted?
bool	subbed_is_function () const
	Is this term a function, taking substitution into accoumt?
bool	subbed_is_variable () const
	Is this term a variable, taking substitution into accoumt?
bool	contains_variable (Variable *) const
	Taking substitution into account, does the term include the variable passed?
Variable *	subbed_variable () const
	Taking substitution into account, what variable do we actually have?
Function *	get_subbed_f () const
	Taking substitution into account, what function do we actually have?
Arity	get_subbed_arity () const
	Taking substitution into account, what arity do we actually have?
Term *	skip_leading_variables () const
	It may be that there is a chain of substitutions attached to a variable.
Term *	skip_leading_variables_for_unification (bool &, Variable *&, Function *&, size_t &) const
	It may be that there is a chain of substitutions attached to a variable.
void	find_subbed_vars (set< Variable * > &) const
	Taking substitution into account, find all the variables in a term.
Term *	make_copy_with_new_vars (VariableIndex &, TermIndex &) const
	Does as the name suggests.
Term *	make_copy_with_new_vars_helper (VariableIndex &, TermIndex &, unordered_map< Variable *, Term * > &) const
	Main implementation of make_copy_with_new_vars.
set< Term * >	all_variables () const
	Assuming nothing has been substituted, find all the variables in this term.

Private Member Functions
	Term ()
	Constructors - these are private as Terms should only ever be constructed by the TermIndex, which is a friend.
	Term (Variable *new_v)
	Term (Function *, const vector< Term * > &)
	This is the only non-trivial constructor because of the need to deal with the function arguments.

Private Attributes
Variable *	v
Function *	f
vector< Term * >	args

Friends
class	TermIndex
ostream &	operator<< (ostream &, const Term &)

Detailed Description

General representation of terms.

Terms can be variables or function-based. This requires care, because after you substitute the former for the latter, it effectively becomes the latter. Similarly, function-based terms are altered by substitution. If a method has "subbed" in the name it means substitutions will be taken into account.

And, yes, the OO mob want to do this with inheritance, but I don't because ultimately I want hash consing, and inheritance would stuff that up BIG TIME!

Definition at line 62 of file Term.hpp.

Constructor & Destructor Documentation

Term() [1/3]

Term::Term ( )

inlineprivate

Constructors - these are private as Terms should only ever be constructed by the TermIndex, which is a friend.

Definition at line 72 of file Term.hpp.

: v(nullptr), f(nullptr), args() {}

Term() [2/3]

Term::Term ( Variable * new_v )

inlineprivate

Definition at line 73 of file Term.hpp.

: v(new_v), f(nullptr), args() {}

Term() [3/3]

Term::Term ( Function * new_f, const vector< Term * > & new_args )

private

This is the only non-trivial constructor because of the need to deal with the function arguments.

You really should make sure you only pass arguments that were obtained from the TermIndex.

Definition at line 35 of file Term.cpp.

: v(nullptr), f(new_f), args(new_args)
{
    if (new_f->get_arity() != new_args.size()) {
        cerr << "Number of arguments doesn't match function arity" << endl;
        cerr << "Perhaps your function names are mixed up?" << endl;
    }
}

Member Function Documentation

all_variables()

set< Term * > Term::all_variables

(

)

const

Assuming nothing has been substituted, find all the variables in this term.

Definition at line 287 of file Term.cpp.

                                     {
    set<Term*> result;
    if (v != nullptr) {
        if (v->is_subbed()) 
            cerr << "STOP IT!!! You shouldn't be using this with substituted variables!" << endl;
        Term* p = const_cast<Term*>(this);
        result.insert(p);
    }
    else {
        for (Term* p : args) {
            set<Term*> some_vars = p->all_variables();
            result.insert(some_vars.begin(), some_vars.end());
        }
    }
    return result;
}

arity()

Arity Term::arity ( ) const

inline

Self-explanatory access function.

Definition at line 102 of file Term.hpp.

{ return args.size(); }

contains_variable()

bool Term::contains_variable

(

Variable *

v2

)

const

Taking substitution into account, does the term include the variable passed?

Note that this acts on the eventual term, so if you look for something that has itself been subbed then the answer is "no".

Definition at line 143 of file Term.cpp.

                                               {
    if (v != nullptr)
       return v->contains_variable(v2);
    if (f != nullptr)
        for (size_t i = 0; i < args.size(); i++)
            if (args[i]->contains_variable(v2))
                return true;
    return false;
}

find_subbed_vars()

void Term::find_subbed_vars

(

set< Variable * > &

vs

)

const

Taking substitution into account, find all the variables in a term.

Does not clear the parameter – you may be adding to it across a bunch of terms.

Definition at line 167 of file Term.cpp.

                                                    {
    if (v != nullptr) {
        if (v->is_subbed())
            v->get_subbed_term()->find_subbed_vars(vs);
        else
            vs.insert(v);
    }
    else {
        for (size_t i = 0; i < args.size(); i++)
            args[i]->find_subbed_vars(vs);
    }
}

get_f()

Function * Term::get_f ( ) const

inline

Self-explanatory access function.

Definition at line 90 of file Term.hpp.

{ return f; }

get_subbed_arity()

Arity Term::get_subbed_arity

(

)

const

Taking substitution into account, what arity do we actually have?

Definition at line 160 of file Term.cpp.

                                   {
    if (f != nullptr)
        return f->get_arity();
    else
        return v->get_subbed_arity();
}

get_subbed_f()

Function * Term::get_subbed_f

(

)

const

Taking substitution into account, what function do we actually have?

Definition at line 153 of file Term.cpp.

                                   {
    if (f != nullptr)
        return f;
    else
        return v->get_subbed_f();
}

get_v()

Variable * Term::get_v ( ) const

inline

Self-explanatory access function.

Definition at line 86 of file Term.hpp.

{ return v; }

is_function()

bool Term::is_function ( ) const

inline

Self-explanatory.

Definition at line 98 of file Term.hpp.

{ return f != nullptr; }

is_ground()

bool Term::is_ground

(

)

const

Is the term ground?

Do not attempt to follow substitutions.

Definition at line 72 of file Term.cpp.

                           {
    if (v != nullptr) {
        return false;
    }
    for (Term* t : args) {
        if (!t->is_ground()) {
            return false;
        }
    }
    return true;
}

is_subbed()

bool Term::is_subbed

(

)

const

Test whether any variable has been substituted.

Definition at line 58 of file Term.cpp.

                           {
    if (v != nullptr) {
        return v->is_subbed();
    }
    else {
        for (size_t i = 0; i < args.size(); i++) {
            if (args[i]->is_subbed()) {
                return true;
            }
        }
    }
    return false;
}

is_unsubbed_variable()

bool Term::is_unsubbed_variable

(

)

const

Is this a variable that hasn't been substituted?

Definition at line 239 of file Term.cpp.

                                      {
    if (v == nullptr)
        return false;
    return !(v->is_subbed());
}

is_variable()

bool Term::is_variable ( ) const

inline

Self-explanatory.

Definition at line 94 of file Term.hpp.

{ return v != nullptr; }

make_copy_with_new_vars()

Term * Term::make_copy_with_new_vars	(	VariableIndex &	vi,
		TermIndex &	ti ) const

Does as the name suggests.

Not straightforward! See documentation for make_copy_with_new_vars_helper

Implementation is in TermIndex.cpp

Parameters

vi	Reference to the VariableIndex
ti	Reference to the TermIndex

Definition at line 160 of file TermIndex.cpp.

                                                        {
 
    unordered_map<Variable*,Term*> v_map;
    return make_copy_with_new_vars_helper(vi, ti, v_map);
}

make_copy_with_new_vars_helper()

Term * Term::make_copy_with_new_vars_helper	(	VariableIndex &	vi,
		TermIndex &	ti,
		unordered_map< Variable *, Term * > &	v_map ) const

Main implementation of make_copy_with_new_vars.

Requires care. You need to build this so that the hash consing is maintained.

In general you might also need to account for substituted variables. This method removes them entirely, so you end up with a term whose only variables are new, and which are also leaves.

This needs to be maintained because the TermIndex should only ever have unsubstituted terms added. (In fact at present TermIndex doesn't make any distinction.)

It may be necessary at some point to add something that also replaces subbed variables with new ones, and additionally updates the current substitution so that they are subbed to the newly constructed terms. However, for Connection Calculus, this method is only needed with stuff in the matrix, and as variables are never directly substituted for things in the matrix the issue never arises.

Implementation is in TermIndex.cpp

Parameters

vi	Reference to the VariableIndex
ti	Reference to the TermIndex
v_map	Reference to an unordered_map from pointers to Variables, to pointers to Terms. Initially empty. On completion contains a map from variables, to the terms corresponding to the new variables made to replace them.

Definition at line 129 of file TermIndex.cpp.

                                                                                        {
    Term* result = nullptr;
    if (v != nullptr) {
        if (v->is_subbed()) {
            result = v->get_subbed_term()->make_copy_with_new_vars_helper(vi, ti, v_map);
            cerr << "If you're doing Connection Calculus then something's wrong!" << endl;
        }
        else {
            auto i = v_map.find(v);
            if (i == v_map.end()) {
                Variable* new_v = vi.add_anon_var();
                result = ti.add_variable_term(new_v);
                v_map.insert(VarMapType(v, result));
            }
            else {
                result = i->second;
            }
        }
    }
    else {
        vector<Term*> new_args;
        for (size_t i = 0; i < args.size(); i++) {
            new_args.push_back(args[i]->make_copy_with_new_vars_helper(vi, ti, v_map));
        }
        result = ti.add_function_term(f, new_args);
    }
    return result;
}

make_LaTeX()

string Term::make_LaTeX

(

bool

subbed = false

)

const

Make a useable LaTeX representation.

Assumes you are in Math mode.

Parameters

subbed

Implement substitutions if true

Definition at line 222 of file Term.cpp.

                                         {
  if (v != nullptr) {
      return v->make_LaTeX(subbed);
  }
  string s = f->make_LaTeX();
  if (args.size() > 0) {
    s += "(";
    commas::comma com(args.size());
    for (size_t j = 0; j < args.size(); j++) {
        s += args[j]->make_LaTeX(subbed);
        s += com();    
    }
    s += ")";
  }
  return s;
}

operator==()

bool Term::operator==

(

const Term &

t

)

const

For the TermIndex you want strict equaliity of the data members.

This will not take substitutions into account.

Definition at line 44 of file Term.cpp.

                                         {
    return (v == t.v &&
            f == t.f &&
            args == t.args);
}

operator[]()

Term * Term::operator[]

(

size_t

i

)

const

Access to args, but don't mess with them!

Do you really need to use this? Be careful as the parameter isn't checked.

Parameters

i	Index of the argument you want.

Definition at line 50 of file Term.cpp.

                                     {
    if (args.size() == 0) {
        cerr << "You shouldn't be accessing a term's arguments here." << endl;
        return nullptr;
    }
    return args[i];
}

skip_leading_variables()

Term * Term::skip_leading_variables

(

)

const

It may be that there is a chain of substitutions attached to a variable.

When doing unification we actually want a pointer either to the final variable in a chain or to the first term that's a function. This returns it.

Definition at line 245 of file Term.cpp.

                                         {
    if (f == nullptr) {
        if (v->is_subbed()) {
            return v->skip_leading_variables();
        }
    }
    Term* p = const_cast<Term*>(this);
    return p;
}

skip_leading_variables_for_unification()

Term * Term::skip_leading_variables_for_unification	(	bool &	_subbed_is_var,
		Variable *&	_subbed_v,
		Function *&	_subbed_f,
		size_t &	_subbed_arity ) const

It may be that there is a chain of substitutions attached to a variable.

When doing unification we actually want a pointer either to the final variable in a chain or to the first term that's a function. This returns it.

In addition to what's done by skip_leading_variables, this finds some other info needed for unification, and in doing so avoids some further function calls.

Definition at line 255 of file Term.cpp.

                                 {
    
    if (f == nullptr && v == nullptr) { 
    }
    Term* p = const_cast<Term*>(this);
    while (p->f == nullptr) {
        if (p->v->is_subbed()) {
            p = p->v->get_subbed_term();
        }
        else {
            break;
        }
    }
    if (p->f == nullptr) {
        _subbed_v = p->v;
        _subbed_f = nullptr;
        _subbed_arity = 0;
        _subbed_is_var = true;
    }
    else {
        _subbed_v = nullptr;
        _subbed_f = p->f;
        _subbed_arity = p->f->get_arity();
        _subbed_is_var = false;
    }
    return p;
}

subbed_equal()

bool Term::subbed_equal

(

Term *

t

)

const

Equality test, taking substitution into account.

For unification you have to take substitution into account, so this needs different treatment to operator==.

Definition at line 84 of file Term.cpp.

                                     {
    if (this == t) {
        return true;
    }
    Variable* tv = t->v;
    // LHS is a variable.
    if (v != nullptr) {
        if (v->is_subbed()) {
            return (v->get_subbed_term())->subbed_equal(t);
        }
        else if (t->subbed_is_variable()) {
            return (t->subbed_variable() == v);
        }
        else return false;
    }
    // RHS is a variable.
    else if (tv != nullptr) {
        if (tv->is_subbed()) {
            return subbed_equal(tv->get_subbed_term());
        }
        else return false;
    }
    // Both sides are functions.
    else {
        if (f != t->f)
            return false;
        if (f->get_arity() != t->f->get_arity())
            return false;
        for (size_t i = 0; i < f->get_arity(); i++) {
            if (!(args[i]->subbed_equal(t->args[i])))
                return false;
        }
        return true;
    }
}

subbed_is_function()

bool Term::subbed_is_function

(

)

const

Is this term a function, taking substitution into accoumt?

Definition at line 120 of file Term.cpp.

                                    {
    if (v == nullptr)
        return true;
    else
        return v->subbed_is_function();
}

subbed_is_variable()

bool Term::subbed_is_variable

(

)

const

Is this term a variable, taking substitution into accoumt?

Definition at line 127 of file Term.cpp.

                                    {
    if (v == nullptr)
        return false;
    else
        return v->subbed_is_variable();
}

subbed_variable()

Variable * Term::subbed_variable

(

)

const

Taking substitution into account, what variable do we actually have?

Definition at line 134 of file Term.cpp.

                                      {
    if (f != nullptr) {
        cerr << "You shouldn't be using this with a function term." << endl;
        return nullptr;
    }
    else
        return v->subbed_variable();
}

to_prolog_string()

string Term::to_prolog_string

(

)

const

Convert to a string that can be read by Prolog.

Does not apply substitutions.

Definition at line 202 of file Term.cpp.

                                    {
  string result;
  if (v != nullptr) {
    result += v->get_name();
  }
  else if (f != nullptr) {
      commas::comma com(args.size());
      result += f->get_name();
      if (args.size() > 0) {
        result += "(";
        for (size_t j = 0; j < args.size(); j++) {
            result += args[j]->to_prolog_string();
            result += com();
        }
      result += ")";
    }
  }
  return result;
}

to_string()

string Term::to_string	(	bool	subbed = false,
		bool	show_addresses = false ) const

Make a string representation of the Term, taking into account any substitutions that have been made.

Parameters

subbed	Implement substitutions if true
show_addresses	Show memory address of this Term if true

Definition at line 180 of file Term.cpp.

                                                             {
    string result;
    if (v != nullptr) {
      result += v->to_string(subbed);
    }
    else if (f != nullptr) {
        result += f->to_string();
        if (f->get_arity() > 0) {
            result += vector_to_string(args, subbed, show_addresses);
        }
    }
    else
        result += "You're trying to print a badly-formed term.";
    if (show_addresses) {
        result += ":";
        ostringstream oss;
        oss << this;
        result += oss.str();
    }
    return result;
}

Friends And Related Symbol Documentation

operator<<

ostream & operator<< ( ostream & out, const Term & t )

friend

Definition at line 304 of file Term.cpp.

                                                 {
  out << t.to_string(params::output_terms_with_substitution, true);
  return out;
}

TermIndex

friend class TermIndex

friend

Definition at line 283 of file Term.hpp.

Member Data Documentation

args

vector<Term*> Term::args

private

Definition at line 66 of file Term.hpp.

f

Function* Term::f

private

Definition at line 65 of file Term.hpp.

v

Variable* Term::v

private

Definition at line 64 of file Term.hpp.

---

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

• /Users/sbh11/Desktop/connection-prover/c++/connect++/source/terms/Term.hpp
• /Users/sbh11/Desktop/connection-prover/c++/connect++/source/terms/Term.cpp
• /Users/sbh11/Desktop/connection-prover/c++/connect++/source/terms/TermIndex.cpp