TermIndex Class Reference

Look after terms, (ideally) 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
vector< Term * >	term_pointers
	Hash table for storing pointers to where Terms are actually stored.

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

Detailed Description

Look after terms, (ideally) 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.)

At present this is the best of two worlds. Unfortunately, use of unordered_map with Term and proper hash consing can result in strange errors, on some compilers but not others, and I'm not too sure where they come from, although there seems to be a problem with memory allocation/deallocation. Using the unordered_map means allowing various kinds of copying of Terms, which I'd rather not do, and that may be the place to look.

Despite this, early indications are that it's definitely worth using the full-blown hash table. If you allow HASHCONSTERMS to be defined in BasicTypes.hpp you will compile with full hash consing. Otherwise you'll get the alternative.

The alternative version has the same behaviour but is likely to be a little less efficient. The fact that it works just fine on every compiler I've tried suggests that something very obscure might be happening in the bowels of the hashed version to make memory errors show up. TODO...

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 75 of file TermIndex.hpp.

Constructor & Destructor Documentation

TermIndex() [1/2]

TermIndex::TermIndex ( )

inline

Definition at line 105 of file TermIndex.hpp.

: term_pointers() {}

~TermIndex()

TermIndex::~TermIndex

(

)

Definition at line 51 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 73 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);
#ifdef HASHCONSTERMS
    index.insert(pair<Term, Term*>(t, p));
#endif
    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 56 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);
#ifdef HASHCONSTERMS
    index.insert(pair<Term, Term*>(t, p));
#endif
    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 40 of file TermIndex.cpp.

                                   {
  for (size_t i = 0; i < term_pointers.size(); i++) {
    if (*(term_pointers[i]) == t) {
      return term_pointers[i];
    }
  }
  return nullptr;
}

get_size()

size_t TermIndex::get_size ( ) const

inline

Basic get method.

Definition at line 121 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 93 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 114 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 133 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

term_pointers

vector<Term*> TermIndex::term_pointers

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.

Used (1) by the alternative storage method, not doing full hash consing; and (2) to make destruction easy.

Definition at line 93 of file TermIndex.hpp.

---

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

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