Inheritance diagram for tptp_parser::fof_formula_grammar< It >:

Collaboration diagram for tptp_parser::fof_formula_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_binary_struct(), ascii::space_type >	fof_binary_nonassoc

qi::rule< It, fof_andor_struct(), ascii::space_type >	fof_binary_assoc

qi::rule< It, vector< string >(), ascii::space_type >	fof_variable_list

qi::rule< It, fof_quantifier_struct(), ascii::space_type >	fof_quantified_formula

qi::rule< It, fof_andor_struct(), ascii::space_type >	fof_or_formula

qi::rule< It, fof_andor_struct(), ascii::space_type >	fof_and_formula

qi::rule< It, fof_formula_type(), ascii::space_type >	fof_binary_formula

qi::rule< It, fof_formula_type(), ascii::space_type >	fof_unit_formula

qi::rule< It, fof_formula_type(), ascii::space_type >	fof_unary_formula

qi::rule< It, fof_formula_type(), ascii::space_type >	fof_unitary_formula

qi::rule< It, fof_formula_type(), ascii::space_type >	fof_logic_formula

qi::rule< It, fof_formula_type(), ascii::space_type >	fof_formula

Detailed Description

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

Definition at line 783 of file TPTPParser.cpp.

Constructor & Destructor Documentation

◆ fof_formula_grammar()

template<typename It >

tptp_parser::fof_formula_grammar< It >::fof_formula_grammar ( )

inline

Definition at line 787 of file TPTPParser.cpp.

      : fof_formula_grammar::base_type(fof_formula) {
 
        fof_binary_formula %=
          fof_binary_nonassoc
          | fof_binary_assoc;
 
        fof_binary_nonassoc %=
          (fof_unit_formula >> nonassoc_connective >> fof_unit_formula);
 
        fof_binary_assoc %=
          fof_or_formula
          | fof_and_formula;
 
        fof_or_formula %=
          fof_unit_formula >> vline >> (fof_unit_formula % '|');
 
        fof_and_formula %=
          fof_unit_formula >> ascii::string("&") >> (fof_unit_formula % '&');
 
        fof_quantified_formula %=
          fof_quantifier
          >> '[' >> fof_variable_list >> ']'
          >> ':' >> fof_unit_formula;
 
        fof_variable_list %=
          variable % ',';
 
        fof_unitary_formula %=
          fof_quantified_formula
          | fof_atomic_formula
          | ('(' >> fof_logic_formula >> ')');
 
        fof_unary_formula %=
          (unary_connective >> fof_unit_formula)
          | fof_infix_unary;
 
        // Similar issue here as with the literal grammar. I think
        // you need to be very careful with the TPTP definition and the 
        // distinction between terms and atomic formulas, f(X) = ... 
        // and f(X) != ... fail because the f(X) gets parsed as the latter in
        // fof_unitary_formula. I have added fof_defined_infix_formula
        // and fof_infix_unary here to fix that.
        fof_unit_formula %=
          fof_defined_infix_formula
          | fof_infix_unary
          | fof_unitary_formula
          | fof_unary_formula;
 
        fof_logic_formula %=
          fof_binary_formula
          | fof_unary_formula
          | fof_unitary_formula;
 
        fof_formula %=
          fof_logic_formula [make_fof_formula()];
      }

Member Data Documentation

◆ fof_and_formula

template<typename It >

qi::rule<It, fof_andor_struct(), ascii::space_type> tptp_parser::fof_formula_grammar< It >::fof_and_formula

Definition at line 861 of file TPTPParser.cpp.

◆ fof_atomic_formula

template<typename It >

fof_atomic_formula_grammar<It> tptp_parser::fof_formula_grammar< It >::fof_atomic_formula

Definition at line 846 of file TPTPParser.cpp.

◆ fof_binary_assoc

template<typename It >

qi::rule<It, fof_andor_struct(), ascii::space_type> tptp_parser::fof_formula_grammar< It >::fof_binary_assoc

Definition at line 851 of file TPTPParser.cpp.

◆ fof_binary_formula

template<typename It >

qi::rule<It, fof_formula_type(), ascii::space_type> tptp_parser::fof_formula_grammar< It >::fof_binary_formula

Definition at line 864 of file TPTPParser.cpp.

◆ fof_binary_nonassoc

template<typename It >

qi::rule<It, fof_binary_struct(), ascii::space_type> tptp_parser::fof_formula_grammar< It >::fof_binary_nonassoc

Definition at line 849 of file TPTPParser.cpp.

◆ fof_defined_infix_formula

template<typename It >

fof_defined_infix_formula_grammar<It> tptp_parser::fof_formula_grammar< It >::fof_defined_infix_formula

Definition at line 844 of file TPTPParser.cpp.

◆ fof_formula

template<typename It >

qi::rule<It, fof_formula_type(), ascii::space_type> tptp_parser::fof_formula_grammar< It >::fof_formula

Definition at line 876 of file TPTPParser.cpp.

◆ fof_infix_unary

template<typename It >

fof_infix_unary_grammar<It> tptp_parser::fof_formula_grammar< It >::fof_infix_unary

Definition at line 845 of file TPTPParser.cpp.

◆ fof_logic_formula

template<typename It >

qi::rule<It, fof_formula_type(), ascii::space_type> tptp_parser::fof_formula_grammar< It >::fof_logic_formula

Definition at line 873 of file TPTPParser.cpp.

◆ fof_or_formula

template<typename It >

qi::rule<It, fof_andor_struct(), ascii::space_type> tptp_parser::fof_formula_grammar< It >::fof_or_formula

Definition at line 859 of file TPTPParser.cpp.

◆ fof_quantified_formula

template<typename It >

qi::rule<It, fof_quantifier_struct(), ascii::space_type> tptp_parser::fof_formula_grammar< It >::fof_quantified_formula

Definition at line 857 of file TPTPParser.cpp.

◆ fof_unary_formula

template<typename It >

qi::rule<It, fof_formula_type(), ascii::space_type> tptp_parser::fof_formula_grammar< It >::fof_unary_formula

Definition at line 868 of file TPTPParser.cpp.

◆ fof_unit_formula

template<typename It >

qi::rule<It, fof_formula_type(), ascii::space_type> tptp_parser::fof_formula_grammar< It >::fof_unit_formula

Definition at line 866 of file TPTPParser.cpp.

◆ fof_unitary_formula

template<typename It >

qi::rule<It, fof_formula_type(), ascii::space_type> tptp_parser::fof_formula_grammar< It >::fof_unitary_formula

Definition at line 870 of file TPTPParser.cpp.

◆ fof_variable_list

template<typename It >

qi::rule<It, vector<string>(), ascii::space_type> tptp_parser::fof_formula_grammar< It >::fof_variable_list

Definition at line 854 of file TPTPParser.cpp.

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

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

Public Attributes

Detailed Description

Constructor & Destructor Documentation

◆ fof_formula_grammar()

Member Data Documentation

◆ fof_and_formula

◆ fof_atomic_formula

◆ fof_binary_assoc

◆ fof_binary_formula

◆ fof_binary_nonassoc

◆ fof_defined_infix_formula

◆ fof_formula

◆ fof_infix_unary

◆ fof_logic_formula

◆ fof_or_formula

◆ fof_quantified_formula

◆ fof_unary_formula

◆ fof_unit_formula

◆ fof_unitary_formula

◆ fof_variable_list