TermIndex Class Reference

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

#include <TermIndex.hpp>

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.

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.s

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.

Constructor & Destructor Documentation

TermIndex()

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.

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

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.

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.

---

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

• TermIndex.hpp
• TermIndex.cpp