tptp_parser::literal_grammar< It > Struct Template Reference

Inheritance diagram for tptp_parser::literal_grammar< It >:

Collaboration diagram for tptp_parser::literal_grammar< It >:

Public Attributes
fof_defined_infix_formula_grammar< It >	fof_defined_infix_formula
fof_infix_unary_grammar< It >	fof_infix_unary
fof_atomic_formula_grammar< It >	fof_atomic_formula
qi::rule< It, fof_atomic_formula_type(), ascii::space_type >	literal

Detailed Description

template<typename It>
struct tptp_parser::literal_grammar< It >

Definition at line 720 of file TPTPParser.cpp.

Constructor & Destructor Documentation

literal_grammar()

template<typename It >

tptp_parser::literal_grammar< It >::literal_grammar ( )

inline

Definition at line 723 of file TPTPParser.cpp.

      : literal_grammar::base_type(literal) {
          /*
          * NOTE: the line for fof_defined_infix_formula should not be here
          * according to the syntax. However for reasons that are not clear
          * f(X) = ... does not get parsed if it's left out. (X = ... is just
          * fine.) The syntax treats ... = ... differently from ... != ... 
          * with the former being handled by fof_atomic_formula.
          *
          * NOTE 2: I wonder what the intended behaviour is for
          * - X = Y .
          *
          * NOTE 3: In the TPTP definition fof_infix_unary comes last,
          * however that causes problems with f(X) != ...
          * I think all that is happening here is that the f(X) gets
          * parsed as an atomic formula if you use the definition
          * exactly.
          */
          // Types are slightly out of line here, but seems
          // fine.
          literal %=
            fof_defined_infix_formula [to_lit()]
            | fof_infix_unary [to_lit()]
            | (eps[unset_neg_lit()] >> fof_atomic_formula) [to_lit()]
            | (lit('~') >> eps[set_neg_lit()] >> fof_atomic_formula) [to_lit()];
      }

Member Data Documentation

fof_atomic_formula

template<typename It >

fof_atomic_formula_grammar<It> tptp_parser::literal_grammar< It >::fof_atomic_formula

Definition at line 751 of file TPTPParser.cpp.

fof_defined_infix_formula

template<typename It >

fof_defined_infix_formula_grammar<It> tptp_parser::literal_grammar< It >::fof_defined_infix_formula

Definition at line 749 of file TPTPParser.cpp.

fof_infix_unary

template<typename It >

fof_infix_unary_grammar<It> tptp_parser::literal_grammar< It >::fof_infix_unary

Definition at line 750 of file TPTPParser.cpp.

literal

template<typename It >

qi::rule<It, fof_atomic_formula_type(), ascii::space_type> tptp_parser::literal_grammar< It >::literal

Definition at line 754 of file TPTPParser.cpp.

---

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

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