convert_fof_atomic_formula Struct Reference

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

#include <TPTPParser.hpp>

Inheritance diagram for convert_fof_atomic_formula:

Collaboration diagram for convert_fof_atomic_formula:

Public Member Functions
Literal	operator() (const fof_plain_term_struct &) const
Literal	operator() (const infix_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 predicate. Then a different one to get the functions.

Definition at line 531 of file TPTPParser.hpp.

Member Function Documentation

operator()() [1/2]

Literal convert_fof_atomic_formula::operator()

(

const fof_plain_term_struct &

f

)

const

Definition at line 1113 of file TPTPParser.cpp.

                                           {
    Literal result;
    size_t arity = f.args.size();
    Predicate* new_P =
      p_index_p->add_predicate(f.functor, arity);
    vector<Term*> args;
    for (size_t i = 0; i < arity; i++) {
      Term* new_t =
        boost::apply_visitor(convert_fof_arguments_struct(),
                              f.args[i]);
      args.push_back(new_t);
    }
    // neg_lit is set by a semantic action.
    return Literal(new_P, args, arity, !neg_lit);
  }

operator()() [2/2]

Literal convert_fof_atomic_formula::operator()

(

const infix_struct &

f

)

const

Definition at line 1130 of file TPTPParser.cpp.

                                  {
    size_t arity = 2;
    if (!equals_added) {
      equals_added = true;
      equals_p = p_index_p->add_predicate("=", arity);
    }
    bool polarity = true;
    if (f.connective == "!=")
      polarity = false;
      vector<Term*> args;
      Term* new_t =
        boost::apply_visitor(convert_fof_arguments_struct(),
                              f.left);
      args.push_back(new_t);
      new_t =
        boost::apply_visitor(convert_fof_arguments_struct(),
                              f.right);
      args.push_back(new_t);
      return Literal(equals_p, args, arity, polarity);
  }

---

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

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