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

More complex semantic actions, now functions etc to make a literal. More...

#include <TPTPParser.hpp>

Inheritance diagram for convert_fof_arguments_struct:
Collaboration diagram for convert_fof_arguments_struct:

Public Member Functions

Termoperator() (const string &) const
 
Termoperator() (const fof_plain_term_struct &) const
 

Detailed Description

More complex semantic actions, now functions etc to make a literal.

This is complicated by the need to be very careful to distinguish predicates from functions. So we have one function to deal with fof_plain_term the first time it's seen, to get a prodicate. Then a different one to get the functions.

Definition at line 544 of file TPTPParser.hpp.

Member Function Documentation

◆ operator()() [1/2]

Term * convert_fof_arguments_struct::operator() ( const fof_plain_term_struct & t) const

Definition at line 1098 of file TPTPParser.cpp.

1099 {
1100 // See comment for companion function: this must be a function.
1101 Arity arity = t.args.size();
1102 vector<Term*> args;
1103 for (size_t i = 0; i < arity; i++) {
1104 Term* new_t =
1105 boost::apply_visitor(convert_fof_arguments_struct(),
1106 t.args[i]);
1107 args.push_back(new_t);
1108 }
1109 Function* f = fun_index_p->add_function(t.functor, arity);
1110 return t_index_p->add_function_term(f, args);
1111 }
Basic representation of functions.
Definition Function.hpp:54
Function * add_function(const string &, Arity)
Add a new function to the index.
General representation of terms.
Definition Term.hpp:62
Term * add_function_term(Function *, const vector< Term * > &)
Self-explanatory: add a Term containing a function to the index.
Definition TermIndex.cpp:56
More complex semantic actions, now functions etc to make a literal.

◆ operator()() [2/2]

Term * convert_fof_arguments_struct::operator() ( const string & s) const

Definition at line 1089 of file TPTPParser.cpp.

1090 {
1091 // The only rule that makes a variable is fof_term, and that's the
1092 // only thing that produces an fof_arguments_struct. So if there is
1093 // a string here then it must be a variable.
1094 Variable* new_var = var_index_p->add_named_var(s);
1095 return t_index_p->add_variable_term(new_var);
1096 }
Term * add_variable_term(Variable *)
Self-explanatory: add a Term containing a variable to the index.
Definition TermIndex.cpp:41
Basic representation of variables.
Definition Variable.hpp:58
Variable * add_named_var(const string &)
Add a variable with the specified name to the index.

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