TermIndex Class Reference

Look after terms, using hash consing to avoid storing copies of terms. More...

#include <TermIndex.hpp>

Collaboration diagram for TermIndex:

Public Member Functions
	TermIndex (const TermIndex &)=delete
	Don't allow copying as this is a terrible idea.
	TermIndex (const TermIndex &&)=delete
TermIndex &	operator= (const TermIndex &)=delete
TermIndex &	operator= (const TermIndex &&)=delete
size_t	get_size () const
	Basic get method.
Term *	add_variable_term (Variable *)
	Self-explanatory: add a Term containing a variable to the index.
Term *	add_function_term (Function *, const vector< Term * > &)
	Self-explanatory: add a Term containing a function to the index.
Term *	replace_variable_in_term (Variable *, Variable *, Term *)
	Replace a variable in a term with an alternative, maintaining the structure of the TermIndex.
Term *	replace_variable_in_term_with_term (Term *, Variable *, Term *)
	Minor variation on replace_variable_in_term.

Private Member Functions
Term *	find (const Term &)
	Find a term in the index.

Private Attributes
unordered_map< Term, Term *, term_hash >	index
	Hash table for storing pointers to where Terms are actually stored.
vector< Term * >	term_pointers
	Used to make destruction easy.

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

Detailed Description

Look after terms, using hash consing to avoid storing copies of terms.

Everything is implemented such that this ignores whether or not Variables are substituted. (Because to do otherwise isn't necessary.)

Using the unordered_map means allowing various kinds of copying of Terms, which I'd rather not do.

You should only use this to make Terms. As long as you do that then this class takes all the responsibility for memory allocation and deallocation for Terms.

Definition at line 54 of file TermIndex.hpp.

Constructor & Destructor Documentation

TermIndex() [1/2]

TermIndex::TermIndex ( )

inline

Definition at line 75 of file TermIndex.hpp.

: index(), term_pointers() {}

~TermIndex()

TermIndex::~TermIndex

(

)

Definition at line 36 of file TermIndex.cpp.

                      {
    for (size_t i = 0; i < term_pointers.size(); i++)
        delete term_pointers[i];
}

TermIndex() [2/2]

TermIndex::TermIndex ( const TermIndex & )

delete

Don't allow copying as this is a terrible idea.

As usual, let the compiler be your friend.

Member Function Documentation

add_function_term()

Term * TermIndex::add_function_term	(	Function *	fp,
		const vector< Term * > &	args )

Self-explanatory: add a Term containing a function to the index.

It's only actually added if it's not already present. If present, a pointer to the existing copy is returned.

Parameters

fp	Pointer to a Function for which an appropriate Term is to be added
args	Vector of pointers to Terms constituting the arguments for the new function Term to be added.

Definition at line 56 of file TermIndex.cpp.

                                                              {
    for (size_t i = 0; i < args.size(); i++) {
      if (args[i]->is_subbed()) {
        cerr << "Don't add substituted functions to the Term Index!" << endl;
      }
    }
    Term t(fp, args);
    Term* p = find(t);
    if (p != nullptr) {
        return p;
    }
    p = new Term(fp, args);
    index.insert(pair<Term, Term*>(t, p));
    term_pointers.push_back(p);
    return p;
}

add_variable_term()

Term * TermIndex::add_variable_term

(

Variable *

vp

)

Self-explanatory: add a Term containing a variable to the index.

It's only actually added if it's not already present. If present, a pointer to the existing copy is returned.

Parameters

vp	Pointer to Variable for which an equivalent Term is to be added

Definition at line 41 of file TermIndex.cpp.

                                               {
    if (vp->is_subbed()) {
      cerr << "Don't add substituted variables to the Term Index!" << endl;
    }
    Term t(vp);
    Term* p = find(t);
    if (p != nullptr) {
      return p;
    }
    p = new Term(vp);
    index.insert(pair<Term, Term*>(t, p));
    term_pointers.push_back(p);
    return p;
}

find()

Term * TermIndex::find ( const Term & t )

private

Find a term in the index.

Parameters

t	The term you want to look up.

Definition at line 28 of file TermIndex.cpp.

                                   {
  auto i = index.find(t);
  if (i != index.end()) {
    return i->second;
  }
  return nullptr;
}

get_size()

size_t TermIndex::get_size ( ) const

inline

Basic get method.

Definition at line 89 of file TermIndex.hpp.

{ return term_pointers.size(); }

replace_variable_in_term()

Term * TermIndex::replace_variable_in_term	(	Variable *	new_v,
		Variable *	old_v,
		Term *	t )

Replace a variable in a term with an alternative, maintaining the structure of the TermIndex.

The first two arguments are variables and the third a general term. Replace one variable with another while keeping the structure of the index correct. Replacement replaces any substitutions for the variable being replaced with those applied to the new one. You should probably not do that as ideally the index should only contain unsubstituted variables.

Parameters

new_v	Pointer to a Variable to use as replacement.
old_v	Pointer to a Variable to be replaced.
t	Pointer to Term to make the replacement for. This should already be in the index.

Definition at line 74 of file TermIndex.cpp.

                                                   {
  if (t->is_variable()) {
    if (old_v == t->get_v()) {
      return add_variable_term(new_v);
    }
    else
      return t;
  }
  else {
    Function* f = t->get_f();
    vector<Term*> new_args;
    for (size_t i = 0; i < t->arity(); i++)
      new_args.push_back(replace_variable_in_term(new_v, old_v, (*t)[i]));
    return add_function_term(f, new_args);
  }
}

replace_variable_in_term_with_term()

Term * TermIndex::replace_variable_in_term_with_term	(	Term *	new_t,
		Variable *	old_v,
		Term *	t )

Minor variation on replace_variable_in_term.

ONLY use this if the new Term is in the index!

Parameters

new_t	Pointer to a Term to use as replacement.
old_v	Pointer to a Variable to be replaced.
t	Pointer to Term to make the replacement for. This should already be in the index.

Definition at line 95 of file TermIndex.cpp.

                                                   {
  if (t->is_variable()) {
    if (old_v == t->get_v()) {
      return new_t;
    }
    else
      return t;
  }
  else {
    Function* f = t->get_f();
    vector<Term*> new_args;
    for (size_t i = 0; i < t->arity(); i++)
      new_args.push_back(replace_variable_in_term_with_term(new_t, old_v, (*t)[i]));
    return add_function_term(f, new_args);
  }
}

Friends And Related Symbol Documentation

operator<<

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

friend

Definition at line 114 of file TermIndex.cpp.

                                                      {
    out << "Contents of term index:" << endl;
    out << "-----------------------" << endl;
    for (Term* p : t.term_pointers)
        out << p << " : " << *p << endl;
    return out;
}

Member Data Documentation

index

unordered_map<Term, Term*, term_hash> TermIndex::index

private

Hash table for storing pointers to where Terms are actually stored.

The key is the Term itself. term_hash is defined in TermHash.hpp.

Definition at line 63 of file TermIndex.hpp.

term_pointers

vector<Term*> TermIndex::term_pointers

private

Used to make destruction easy.

Definition at line 67 of file TermIndex.hpp.

---

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

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