Wrap up everything the TPTP parser needs to do inside a single class. More...

#include <TPTPParser.hpp>

Public Member Functions
	TPTPParser ()=delete
	You definitely don't want this constructor.

	TPTPParser (VariableIndex , FunctionIndex , TermIndex , PredicateIndex , Matrix *)
	The only constructor that makes sense.

bool	parse_tptp_from_file (const string &)
	Main method to parse from a TPTP file to the data structures needed by the prover.

void	show_file_includes ()
	Show any includes present in the TPTP file.

void	clear ()
	Clear everything associated with the TPTP parser.

vector< string >	get_defined_items ()
	Get a copy of tptp_parser::all_defined.

vector< string >	get_system_items ()
	Get a copy of tptp_parser::all_system.

bool	equality_used ()
	Did equality turn up anywhere in the parse?

bool	conjecture_present () const
	Did a conjecture turn up anywhere in the parse?

size_t	number_of_fof_formulas () const
	How many first-order formulas turned up in the parse?

string	get_problem_status ()
	The parse tries to identify the problem status.

Predicate *	get_equals_predicate () const
	If equality turned up anywhere in the parse it will have been turned into an actual Predicate, so this will give you a pointer to it.

Detailed Description

Wrap up everything the TPTP parser needs to do inside a single class.

This class needs access to the assorted indices employed by the prover because they are the only things anyone should be using to make Terms, Variables etc.

If you construct this properly and use parse_tptp_from_file, then after a successful parse the indices have everything ready to go.

Member Function Documentation

◆ clear()

void TPTPParser::clear ( )

Clear everything associated with the TPTP parser.

Note that this is slightly messy because it also clears all the supporting stuff that's global in the tptp_parser namespace. Yes, very ugly. What ya gonna do about it!!??

◆ get_defined_items()

vector< string > TPTPParser::get_defined_items ( )

Get a copy of tptp_parser::all_defined.

These are gathered during the parse and may be useful.

◆ get_system_items()

vector< string > TPTPParser::get_system_items ( )

Get a copy of tptp_parser::all_system.

These are gathered during the parse and may be useful.

◆ parse_tptp_from_file()

bool TPTPParser::parse_tptp_from_file ( const string & file_name )

Main method to parse from a TPTP file to the data structures needed by the prover.

This first uses read_tptp_from_file to strip out comments. It then uses TPTP_file_grammar with qi::phrase_parse to parse the file.

As a side effect of that, a bunch of things such as all_clauses and clause_roles, which are global in the tptp_parser namespace, get set up. These are then used to populate the matrix etc.

Parameters

file_name Reference to string containing the file name.

◆ show_file_includes()

void TPTPParser::show_file_includes ( )

Show any includes present in the TPTP file.

These are collected as part of the parse.

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

TPTPParser.hpp
TPTPParser.cpp