FunctionIndex Class Reference

Mechanism for looking after functions. More...

#include <FunctionIndex.hpp>

Collaboration diagram for FunctionIndex:

Public Member Functions
	FunctionIndex (const FunctionIndex &)=delete
	As usual, trying to copy one of these is a really bad idea.
	FunctionIndex (const FunctionIndex &&)=delete
FunctionIndex &	operator= (const FunctionIndex &)=delete
FunctionIndex &	operator= (const FunctionIndex &&)=delete
size_t	get_size () const
	Self-explanatory.
Function *	add_function (const string &, Arity)
	Add a new function to the index.
Function *	make_skolem_function (Arity)
	Add a new Skolem function. Naming is automatic.
Function *	find_function (const string &, Arity)
	Look up a stored Function by name and arity.
Arity	find_maximum_arity () const
	Find the largest arity appearing for any Function in the index.
Arity	find_minimum_arity () const
	Find the smallest arity appearing for any Function in the index.
Function *	operator[] (size_t i)
	Access to pointers to Functions, but don't mess with them!

Private Attributes
vector< Function * >	funs
	Pointers to all the Functions used.
unordered_map< pair< string, Arity >, Function *, fun_hash >	name_index
	Fast lookup from name/arity to pointer to the Function.
ID	next_index
	Keep track of ids for adding new Functions.
uint32_t	skolem_function_number
	Automate the naming of Skolem functions.

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

Detailed Description

Mechanism for looking after functions.

Function names are only stored once, but functions can have the same name and a different arity.

Somewhat more straightforward than looking after variables as there is no need for anonymous functions other than Skolem functions, and those do not get recycled. For the same reason, there is no need to take account of backtracking.

You should only use this to make new Functions. As long as you do, it will take care of allocation and deallocation for you.

Definition at line 64 of file FunctionIndex.hpp.

Constructor & Destructor Documentation

FunctionIndex()

FunctionIndex::FunctionIndex

(

)

Definition at line 27 of file FunctionIndex.cpp.

: funs()
, name_index()
, next_index(0)
, skolem_function_number(1)
{}

~FunctionIndex()

FunctionIndex::~FunctionIndex

(

)

Definition at line 34 of file FunctionIndex.cpp.

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

Member Function Documentation

add_function()

Function * FunctionIndex::add_function	(	const string &	name,
		Arity	arity )

Add a new function to the index.

If you add twice, the original will get re-used.

Parameters

name	The name of the Function.
arity	The arity of the Function.

Definition at line 39 of file FunctionIndex.cpp.

                                                                     {
    Function* new_fun = nullptr;
    auto i = name_index.find(FunIndexType(name, arity));
    if (i == name_index.end()) {
        new_fun = new Function(next_index++, name, arity);
        funs.push_back(new_fun);
        name_index.insert(FunMapType(FunIndexType(name, arity),
                                     new_fun));
    }
    else {
        new_fun = i->second;
    }
    return new_fun;
}

find_function()

Function * FunctionIndex::find_function	(	const string &	fun_name,
		Arity	arity )

Look up a stored Function by name and arity.

Parameters

fun_name	Name of Function to find.
arity	Arity of Function to find.

Definition at line 60 of file FunctionIndex.cpp.

                                                    {
    Function* fun = nullptr;
    auto i = name_index.find(FunIndexType(fun_name, arity));
    if (i != name_index.end())
        fun = i->second;
    else
        cerr << "That function name doesn't exist" << endl;
    return fun;
}

find_maximum_arity()

Arity FunctionIndex::find_maximum_arity

(

)

const

Find the largest arity appearing for any Function in the index.

Definition at line 71 of file FunctionIndex.cpp.

                                              {
  Arity result = 0;
  for (size_t i = 0; i < funs.size(); i++) {
    Arity current = funs[i]->get_arity();
    if (current > result)
      result = current;
  }
  return result;
}

find_minimum_arity()

Arity FunctionIndex::find_minimum_arity

(

)

const

Find the smallest arity appearing for any Function in the index.

Definition at line 81 of file FunctionIndex.cpp.

                                              {
  Arity result = UINT32_MAX;
  for (size_t i = 0; i < funs.size(); i++) {
    Arity current = funs[i]->get_arity();
    if (current < result)
      result = current;
  }
  return result;
}

get_size()

size_t FunctionIndex::get_size ( ) const

inline

Self-explanatory.

Definition at line 96 of file FunctionIndex.hpp.

{ return funs.size(); }

make_skolem_function()

Function * FunctionIndex::make_skolem_function

(

Arity

arity

)

Add a new Skolem function. Naming is automatic.

Parameters

arity

The arity of the new Skolem function.

Definition at line 54 of file FunctionIndex.cpp.

                                                         {
  string name(params::unique_skolem_prefix);
  name += std::to_string(skolem_function_number++);
  return add_function(name, arity);
}

operator[]()

Function * FunctionIndex::operator[] ( size_t i )

inline

Access to pointers to Functions, but don't mess with them!

Definition at line 133 of file FunctionIndex.hpp.

{ return funs[i]; }

Friends And Related Symbol Documentation

operator<<

ostream & operator<< ( ostream & out, const FunctionIndex & fi )

friend

Definition at line 91 of file FunctionIndex.cpp.

                                                           {
    out << "Function Index" << endl;
    out << "--------------" << endl;
    for (Function* f : fi.funs) {
        out << *f << endl;
    }
    return out;
}

Member Data Documentation

funs

vector<Function*> FunctionIndex::funs

private

Pointers to all the Functions used.

Definition at line 69 of file FunctionIndex.hpp.

name_index

unordered_map<pair<string, Arity>, Function*, fun_hash> FunctionIndex::name_index

private

Fast lookup from name/arity to pointer to the Function.

Definition at line 73 of file FunctionIndex.hpp.

next_index

ID FunctionIndex::next_index

private

Keep track of ids for adding new Functions.

Definition at line 77 of file FunctionIndex.hpp.

skolem_function_number

uint32_t FunctionIndex::skolem_function_number

private

Automate the naming of Skolem functions.

Definition at line 81 of file FunctionIndex.hpp.

---

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

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