|
|
VariableIndex * | var_index_p |
| |
|
FunctionIndex * | fun_index_p |
| |
|
TermIndex * | t_index_p |
| |
|
PredicateIndex * | p_index_p |
| |
|
vector< FileIncludeItem > | file_includes |
| |
|
set< string > | to_include |
| |
|
bool | include_this_item |
| |
|
bool | is_first_status = true |
| |
|
string | status |
| |
|
vector< string > | all_defined |
| |
|
vector< string > | all_system |
| |
|
bool | equals_added |
| |
|
Predicate * | equals_p |
| |
|
bool | conjecture_found = false |
| |
|
string | current_clause_role |
| |
|
vector< string > | clause_roles |
| |
|
string | current_formula_role |
| |
|
vector< string > | formula_roles |
| |
|
string | current_formula_name |
| |
|
vector< string > | formula_names |
| |
|
bool | neg_lit |
| |
|
Literal | current_lit |
| |
|
Clause | current_clause |
| |
|
vector< Clause > | all_clauses |
| |
|
FOF | current_formula (FOFType::Empty) |
| |
|
vector< FOF > | all_formulas |
| |
| qi::rule< Iter, char()> | percentage_sign |
| |
| qi::rule< Iter, char()> | double_quote |
| |
| qi::rule< Iter, char()> | do_char |
| |
| qi::rule< Iter, char()> | single_quote |
| |
| qi::rule< Iter, char()> | sq_char |
| |
| qi::rule< Iter, char()> | sign |
| |
| qi::rule< Iter, char()> | dot |
| |
| qi::rule< Iter, char()> | exponent |
| |
| qi::rule< Iter, char()> | slash_char |
| |
| qi::rule< Iter, char()> | slosh_char |
| |
| qi::rule< Iter, char()> | zero_numeric |
| |
| qi::rule< Iter, char()> | non_zero_numeric |
| |
| qi::rule< Iter, char()> | numeric |
| |
| qi::rule< Iter, char()> | lower_alpha |
| |
| qi::rule< Iter, char()> | upper_alpha |
| |
| qi::rule< Iter, char()> | alpha_numeric |
| |
| qi::rule< Iter, char()> | dollar |
| |
| qi::rule< Iter, char()> | printable_char |
| |
| qi::rule< Iter, char()> | viewable_char |
| |
| qi::rule< Iter, string()> | slash |
| |
| qi::rule< Iter, string()> | slosh |
| |
| qi::rule< Iter, string()> | unsigned_exp_integer |
| |
| qi::rule< Iter, string()> | signed_exp_integer |
| |
| qi::rule< Iter, string()> | exp_integer |
| |
| qi::rule< Iter, string()> | dot_decimal |
| |
| qi::rule< Iter, string()> | positive_decimal |
| |
| qi::rule< Iter, string()> | decimal |
| |
| qi::rule< Iter, string()> | decimal_fraction |
| |
| qi::rule< Iter, string()> | decimal_exponent |
| |
| qi::rule< Iter, string()> | unsigned_integer |
| |
| qi::rule< Iter, string()> | signed_integer |
| |
| qi::rule< Iter, string()> | integer |
| |
| qi::rule< Iter, string()> | unsigned_rational |
| |
| qi::rule< Iter, string()> | signed_rational |
| |
| qi::rule< Iter, string()> | rational |
| |
| qi::rule< Iter, string()> | unsigned_real |
| |
| qi::rule< Iter, string()> | signed_real |
| |
| qi::rule< Iter, string()> | real |
| |
| qi::rule< Iter, string()> | vline |
| |
| qi::rule< Iter, string()> | star |
| |
| qi::rule< Iter, string()> | plus |
| |
| qi::rule< Iter, string()> | arrow |
| |
| qi::rule< Iter, string()> | less_sign |
| |
| qi::rule< Iter, string()> | hash |
| |
| qi::rule< Iter, string()> | lower_word |
| |
| qi::rule< Iter, string()> | formula_role |
| |
| qi::rule< Iter, string()> | upper_word |
| |
| qi::rule< Iter, string()> | variable |
| |
| qi::rule< Iter, string()> | dollar_dollar_word |
| |
| qi::rule< Iter, string()> | dollar_word |
| |
| qi::rule< Iter, string()> | distinct_object |
| |
| qi::rule< Iter, string()> | single_quoted |
| |
| qi::rule< Iter, string()> | file_name |
| |
| qi::rule< Iter > | null |
| |
| qi::rule< Iter, string()> | comment_status |
| |
| qi::rule< Iter, string(), ascii::space_type > | status_comment |
| |
| qi::rule< Iter, string()> | standard_comment |
| |
| qi::rule< Iter, string(), ascii::space_type > | comment_line |
| |
| qi::rule< Iter, string()> | not_star_slash |
| |
| qi::rule< Iter, string()> | comment_block |
| |
| qi::rule< Iter, string(), ascii::space_type > | comment |
| |
| qi::rule< Iter, string()> | atomic_defined_word |
| |
| qi::rule< Iter, string()> | atomic_system_word |
| |
| qi::rule< Iter, string()> | system_functor |
| |
| qi::rule< Iter, string()> | system_constant |
| |
| qi::rule< Iter, string()> | number |
| |
| qi::rule< Iter, string()> | atomic_word |
| |
| qi::rule< Iter, string()> | predicate |
| |
| qi::rule< Iter, string()> | functor |
| |
| qi::rule< Iter, string()> | constant |
| |
| qi::rule< Iter, string()> | proposition |
| |
| qi::rule< Iter, string()> | name |
| |
| qi::rule< Iter, string()> | defined_predicate |
| |
| qi::rule< Iter, string()> | defined_proposition |
| |
| qi::rule< Iter, string()> | defined_functor |
| |
| qi::rule< Iter, string()> | defined_constant |
| |
| qi::rule< Iter, string()> | defined_term |
| |
| qi::rule< Iter, string()> | infix_equality |
| |
| qi::rule< Iter, string()> | infix_inequality |
| |
| qi::rule< Iter, string()> | defined_infix_pred |
| |
| qi::rule< Iter, string()> | fof_quantifier |
| |
| qi::rule< Iter, string()> | nonassoc_connective |
| |
| qi::rule< Iter, string()> | assoc_connective |
| |
| qi::rule< Iter, string()> | unary_connective |
| |
The tptp_parser namespace contains a lot of stuff that's essentially just global.
Corresponds to v8.1.0.0 of the TPTP definition on 2-8-22.
WARNING!
You should probably REALLY not touch this unless you're very familiar indeed with the Spirit library in Boost, which is what's used to build the parser.
The good news is that you should never have to, because I'm a lovely man and have done all the hard work so you don't have to. Essentially the class TPTPParser wraps everything up and a call to TPTPParser::parse_tptp_from_file does a great deal (all!) of the work for you. This happens in StackProver::read_from_tptp_file, and at that point all the indices for Terms etc and the Matrix should be built.
Final note: yes this could be simpler, but the aim is to follow the actual TPTP specification as closely as possible. The naming should support this – names are chosen as much as possible to correspond to the TPTP documentation.
"What is this madness!?" I hear you cry.
Well, writing this is made very straightforward if you allow semantic actions to construct the results of the parse in what are essentially global data structures. Hiding them in a namespace takes some of the sting and uglyness away. Doing it differently is, I claim, just making life more difficult – this way, the TPTPParser class can just pull things out of the eventual globals – the user doesn't have to be any the wiser and they end up using the TermIndex, Matrix and so on quite happily, because those are the actual end result.
The boost library does actually have good support for doing all this in a nice OO way. Yes, I've tried that too. I came to the conclusion that the current approach yields much more readable code.
