Connect++ 0.6.0
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
Function Class Reference

Basic representation of functions. More...

#include <Function.hpp>

Collaboration diagram for Function:

Public Member Functions

 Function (const Function &)=delete
 You want to inforce sharing, so don't allow copies to be made.
 
 Function (const Function &&)=delete
 
Functionoperator= (const Function &)=delete
 
Functionoperator= (const Function &&)=delete
 
string get_name () const
 Most basic access function.
 
Arity get_arity () const
 Most basic access function.
 
string to_string () const
 Make a useable string representation.
 
string make_LaTeX () const
 Make a useable LaTeX version.
 

Private Member Functions

 Function ()
 Constructors are private as you only want the FunctionIndex to make these, and it's a friend.
 
 Function (ID new_id)
 
 Function (ID new_id, const string &new_name)
 
 Function (ID new_id, const string &new_name, Arity new_arity)
 

Private Attributes

ID id
 
string name
 
Arity arity
 

Friends

class FunctionIndex
 
ostream & operator<< (ostream &, const Function &)
 Really only for debugging.
 

Detailed Description

Basic representation of functions.

As with Variables, these are ultimately wrapped in a Term. These are also ultimately looked after by a FunctionIndex (which is a friend), so there should not be any need to mess with them directly. (This is why the constructors are private.)

Note that this is somewhat simpler than Variable because you are not dealing with substitutions: you only need id, name and arity.

Definition at line 54 of file Function.hpp.

Constructor & Destructor Documentation

◆ Function() [1/5]

Function::Function ( )
inlineprivate

Constructors are private as you only want the FunctionIndex to make these, and it's a friend.

Definition at line 63 of file Function.hpp.

63: id(0), name(), arity(0) {}

◆ Function() [2/5]

Function::Function ( ID new_id)
inlineprivate

Definition at line 64 of file Function.hpp.

64: id(new_id), name(), arity(0) {}

◆ Function() [3/5]

Function::Function ( ID new_id,
const string & new_name )
inlineprivate

Definition at line 65 of file Function.hpp.

66 : id(new_id), name(new_name), arity(0) {}

◆ Function() [4/5]

Function::Function ( ID new_id,
const string & new_name,
Arity new_arity )
inlineprivate

Definition at line 67 of file Function.hpp.

68 : id(new_id), name(new_name), arity(new_arity) {}

◆ Function() [5/5]

Function::Function ( const Function & )
delete

You want to inforce sharing, so don't allow copies to be made.

It should never be necessary to make copies, so this is to help the compiler to detect errors.

Member Function Documentation

◆ get_arity()

Arity Function::get_arity ( ) const
inline

Most basic access function.

Definition at line 88 of file Function.hpp.

88{ return arity; }

◆ get_name()

string Function::get_name ( ) const
inline

Most basic access function.

Definition at line 84 of file Function.hpp.

84{ return name; }

◆ make_LaTeX()

string Function::make_LaTeX ( ) const

Make a useable LaTeX version.

Assumes you are typesetting in Math Mode. Makes a limited attempt to deal with special characters in the function name, but if your name is too fancy it's likely to produce something either ugly or unacceptable to LaTeX.

Definition at line 33 of file Function.cpp.

33 {
34 string s ("\\text{");
35 s += latex_escape_characters(name);
36 s += "}";
37 return s;
38}

◆ to_string()

string Function::to_string ( ) const

Make a useable string representation.

Definition at line 28 of file Function.cpp.

28 {
29 colour_string::ColourString cs(params::use_colours);
30 return cs(name).green();
31}
Simple addition of colour to strings and ostreams.

Friends And Related Symbol Documentation

◆ FunctionIndex

friend class FunctionIndex
friend

Definition at line 103 of file Function.hpp.

◆ operator<<

ostream & operator<< ( ostream & out,
const Function & f )
friend

Really only for debugging.

Use Function::to_string if you want something pretty.

Definition at line 45 of file Function.cpp.

45 {
46 out << "Function: " << setw(params::output_width) << f.id
47 << " Name: " << setw(params::output_width + 20) << f.name
48 << " Arity: " << setw(params::output_width) << f.arity;
49 return out;
50}

Member Data Documentation

◆ arity

Arity Function::arity
private

Definition at line 58 of file Function.hpp.

◆ id

ID Function::id
private

Definition at line 56 of file Function.hpp.

◆ name

string Function::name
private

Definition at line 57 of file Function.hpp.


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