Connect++ 0.5.0
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
Classes | Typedefs | Functions | Variables
tptp_parser Namespace Reference

The tptp_parser namespace contains a lot of stuff that's essentially just global. More...

Classes

struct  cnf_annotated_grammar
 
struct  cnf_annotated_struct
 Parser's representation of a Clause. More...
 
struct  cnf_formula_grammar
 
struct  fof_annotated_grammar
 
struct  fof_atomic_formula_grammar
 
struct  fof_defined_infix_formula_grammar
 
struct  fof_formula_grammar
 
struct  fof_infix_unary_grammar
 
struct  fof_plain_term_struct
 Recursive data structure for Terms. More...
 
struct  fof_term_grammar
 
struct  include_grammar
 
struct  infix_struct
 Structure for fof_defined_infix_formula and fof_infix_unary. More...
 
struct  literal_grammar
 
struct  TPTP_file_grammar
 

Typedefs

using Iter = string::const_iterator
 Iterator type for parser rules and grammars.
 
using fof_arguments_struct
 Variant - Term arguments can be Variables or other Terms.
 
using fof_atomic_formula_type
 An atomic formula can be infix as well.
 

Functions

void read_tptp_from_file_simple (const string &file_name, string &file_contents)
 
void recursive_tptp_include (const FileIncludeItem &include_item)
 

Variables

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
 
fs::path include_file_path
 
bool is_first_status = true
 
string status
 
vector< string > all_defined
 
vector< string > all_system
 
set< string > distinct_objects
 
bool equals_added
 
Predicate * equals_p
 
bool conjecture_found = false
 
bool negated_conjecture_found = false
 
bool conjecture_true = false
 
bool conjecture_false = false
 
bool found_true_axiom = false
 
bool found_false_axiom = false
 
bool negated_conjecture_exists = false
 
bool has_axioms = false
 
bool has_axioms_remaining = false
 
bool cnf_only = false
 
size_t number_of_negated_conjecture_clauses = 0
 
size_t number_of_simplified_negated_conjecture_clauses = 0
 
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
 

Detailed Description

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.

Typedef Documentation

◆ fof_arguments_struct

using tptp_parser::fof_arguments_struct
Initial value:
boost::variant<
string,
boost::recursive_wrapper<fof_plain_term_struct>
>

Variant - Term arguments can be Variables or other Terms.

Definition at line 89 of file TPTPParser.hpp.

◆ fof_atomic_formula_type

using tptp_parser::fof_atomic_formula_type
Initial value:
boost::variant<
fof_plain_term_struct,
infix_struct
>

An atomic formula can be infix as well.

Definition at line 118 of file TPTPParser.hpp.

◆ Iter

using tptp_parser::Iter = string::const_iterator

Iterator type for parser rules and grammars.

Definition at line 79 of file TPTPParser.hpp.

Function Documentation

◆ read_tptp_from_file_simple()

void tptp_parser::read_tptp_from_file_simple ( const string & file_name,
string & file_contents )

Definition at line 1963 of file TPTPParser.cpp.

1964 {
1965
1966 bool in_comment = false;
1967 char c;
1968
1969 ifstream file;
1970 file.unsetf(std::ios_base::skipws);
1971 file.open(file_name);
1972 if (file.fail()) {
1973 throw (file_open_exception(file_name));
1974 }
1975 file.get(c);
1976 while (file.good()) {
1977 // Detect the start of a comment.
1978 if (!in_comment && c == '/') {
1979 if (file.peek() == '*') {
1980 file.get(c);
1981 in_comment = true;
1982 }
1983 else file_contents += c;
1984 }
1985 // Detect the end of a comment.
1986 else if (in_comment && c == '*') {
1987 if (file.peek() == '/') {
1988 file.get(c);
1989 in_comment = false;
1990 }
1991 }
1992 // Nothings to see. We're just adding to the
1993 // relevant output.
1994 else if (!in_comment)
1995 file_contents += c;
1996
1997 file.get(c);
1998 }
1999 file.close();
2000}
file_open_exception
Exception used by the application in main(...).
Definition Exceptions.hpp:36

◆ recursive_tptp_include()

void tptp_parser::recursive_tptp_include ( const FileIncludeItem & include_item)

Definition at line 2008 of file TPTPParser.cpp.

2008 {
2009
2010 verbose_print::VPrint show(params::verbosity);
2011
2012 // The file to include, as stated in the current TPTP file.
2013 fs::path file_name(include_item.first);
2014 fs::path actual_include_path(include_item.first);
2015 fs::path initial_path(include_file_path);
2016 // Is it absolute? If so, life is easy!
2017 if (actual_include_path.is_absolute()) {
2018 if (!fs::exists(actual_include_path)) {
2019 cout << "% SZS status Error for "
2020 << params::problem_name
2021 << " : include file missing." << endl;
2022 exit(EXIT_FAILURE);
2023 }
2024 }
2025 // It must be relative - let's try to find it...
2026 else {
2027 //...relative to the current file's path...
2028 file_name = initial_path / actual_include_path;
2029 if (!fs::exists(file_name)) {
2030 fs::path tptp(params::tptp_path);
2031 file_name = tptp / actual_include_path;
2032 //...or relative to the TPTP path.
2033 if (!fs::exists(file_name)) {
2034 cout << "% SZS status Error for "
2035 << params::problem_name
2036 << " : include file missing." << endl;
2037 exit(EXIT_FAILURE);
2038 }
2039 }
2040 }
2041
2042 // Save the path for the current part of the recursion and
2043 // set it to the new path.
2044 fs::path saved_path = include_file_path;
2045 include_file_path = file_name;
2046 include_file_path.remove_filename();
2047
2048 if (params::first_parse) {
2049 show(1,string("Including: "));
2050 show(1,file_name, true);
2051 }
2052
2053 // Remember the current include formulas.
2054 set<string> saved_includes = to_include;
2055
2056 // This was deleted to take account of the TPTP's slightly
2057 // cryptic "...(this filter also applies to formulae that
2058 // have been recursively included into the named file)...".
2059 // I interpreted this as meaning that you have to pass
2060 // the names of things to include along each time you
2061 // recurse. However Geoff says this is not the case!
2062 to_include.clear();
2063
2064 // Set up the new include formulas.
2065 if (include_item.second.empty() ||
2066 (include_item.second.size() == 1 && include_item.second[0] == string("all"))) {
2067 if (params::first_parse) {
2068 show(1,string("All"),true);
2069 }
2070 }
2071 else {
2072 for (string s : include_item.second) {
2073 to_include.insert(s);
2074 if (params::first_parse) {
2075 show(1, s, true);
2076 }
2077 }
2078 }
2079
2080 // Get the file you want to include.
2081 string file_contents;
2082 read_tptp_from_file_simple(file_name, file_contents);
2083
2084 // Use the existing parser.
2085 Iter start = file_contents.begin();
2086 Iter end = file_contents.end();
2087
2088 TPTP_file_grammar<Iter> g;
2089 bool result = qi::phrase_parse(start, end, g, ascii::space);
2090
2091 if (start != end || !result)
2092 throw (file_parse_exception(file_name));
2093
2094 // Restore previous include formulas.
2095 to_include = saved_includes;
2096 if (to_include.empty())
2097 include_this_item = true;
2098
2099 // Restore include file path.
2100 include_file_path = saved_path;
2101}
file_parse_exception
Exception used by the application in main(...).
Definition Exceptions.hpp:58
verbose_print::VPrint
Definition vic_strings.hpp:237

Variable Documentation

◆ all_clauses

vector<Clause> tptp_parser::all_clauses

Definition at line 151 of file TPTPParser.cpp.

◆ all_defined

vector<string> tptp_parser::all_defined

Definition at line 110 of file TPTPParser.cpp.

◆ all_formulas

vector<FOF> tptp_parser::all_formulas

Definition at line 156 of file TPTPParser.cpp.

◆ all_system

vector<string> tptp_parser::all_system

Definition at line 111 of file TPTPParser.cpp.

◆ alpha_numeric

qi::rule<Iter, char()> tptp_parser::alpha_numeric
Initial value:
=
lower_alpha
| upper_alpha
| numeric
| qi::char_('_')

Definition at line 217 of file TPTPParser.cpp.

◆ arrow

qi::rule<Iter, string()> tptp_parser::arrow
Initial value:
=
ascii::string(">")

Definition at line 283 of file TPTPParser.cpp.

◆ assoc_connective

qi::rule<Iter, string()> tptp_parser::assoc_connective
Initial value:
=
vline
| ascii::string("&")

Definition at line 479 of file TPTPParser.cpp.

◆ atomic_defined_word

qi::rule<Iter, string()> tptp_parser::atomic_defined_word
Initial value:
=
dollar_word

Definition at line 380 of file TPTPParser.cpp.

◆ atomic_system_word

qi::rule<Iter, string()> tptp_parser::atomic_system_word
Initial value:
=
dollar_dollar_word

Definition at line 382 of file TPTPParser.cpp.

◆ atomic_word

qi::rule<Iter, string()> tptp_parser::atomic_word
Initial value:
=
lower_word
| single_quoted

Definition at line 393 of file TPTPParser.cpp.

◆ clause_roles

vector<string> tptp_parser::clause_roles

Definition at line 137 of file TPTPParser.cpp.

◆ cnf_only

bool tptp_parser::cnf_only = false

Definition at line 130 of file TPTPParser.cpp.

◆ comment

qi::rule<Iter, string(), ascii::space_type> tptp_parser::comment
Initial value:
=
comment_line | comment_block

Definition at line 378 of file TPTPParser.cpp.

◆ comment_block

qi::rule<Iter, string()> tptp_parser::comment_block
Initial value:
=
qi::char_('/')
>> qi::char_('*')
>> not_star_slash
>> qi::char_('*') >> *(qi::char_('*')) >> qi::char_('/')

Definition at line 373 of file TPTPParser.cpp.

◆ comment_line

qi::rule<Iter, string(), ascii::space_type> tptp_parser::comment_line
Initial value:
=
status_comment
| standard_comment

Definition at line 364 of file TPTPParser.cpp.

◆ comment_status

qi::rule<Iter, string()> tptp_parser::comment_status
Initial value:
=
ascii::string("Theorem")
| ascii::string("ContradictoryAxioms")
| ascii::string("CounterSatisfiable")
| ascii::string("Satisfiable")
| ascii::string("Unsatisfiable")
| ascii::string("Unknown")
| ascii::string("Open")

Definition at line 342 of file TPTPParser.cpp.

◆ conjecture_false

bool tptp_parser::conjecture_false = false

Definition at line 124 of file TPTPParser.cpp.

◆ conjecture_found

bool tptp_parser::conjecture_found = false

Definition at line 121 of file TPTPParser.cpp.

◆ conjecture_true

bool tptp_parser::conjecture_true = false

Definition at line 123 of file TPTPParser.cpp.

◆ constant

qi::rule<Iter, string()> tptp_parser::constant
Initial value:
=
functor

Definition at line 400 of file TPTPParser.cpp.

◆ current_clause

Clause tptp_parser::current_clause

Definition at line 150 of file TPTPParser.cpp.

◆ current_clause_role

string tptp_parser::current_clause_role

Definition at line 136 of file TPTPParser.cpp.

◆ current_formula_name

string tptp_parser::current_formula_name

Definition at line 143 of file TPTPParser.cpp.

◆ current_formula_role

string tptp_parser::current_formula_role

Definition at line 141 of file TPTPParser.cpp.

◆ current_lit

Literal tptp_parser::current_lit

Definition at line 149 of file TPTPParser.cpp.

◆ decimal

qi::rule<Iter, string()> tptp_parser::decimal
Initial value:
=
zero_numeric | positive_decimal

Definition at line 248 of file TPTPParser.cpp.

◆ decimal_exponent

qi::rule<Iter, string()> tptp_parser::decimal_exponent
Initial value:
=
(decimal | decimal_fraction) >> exponent >> exp_integer

Definition at line 252 of file TPTPParser.cpp.

◆ decimal_fraction

qi::rule<Iter, string()> tptp_parser::decimal_fraction
Initial value:
=
decimal >> dot_decimal

Definition at line 250 of file TPTPParser.cpp.

◆ defined_constant

qi::rule<Iter, string()> tptp_parser::defined_constant
Initial value:
=
defined_functor

Definition at line 447 of file TPTPParser.cpp.

◆ defined_functor

qi::rule<Iter, string()> tptp_parser::defined_functor
Initial value:
=
ascii::string("$uminus")
| ascii::string("$sum")
| ascii::string("$difference")
| ascii::string("$product")
| ascii::string("$quotient")
| ascii::string("$quotient_e")
| ascii::string("$quotient_t")
| ascii::string("$quotient_f")
| ascii::string("$remainder_e")
| ascii::string("$remainder_t")
| ascii::string("$remainder_f")
| ascii::string("$floor")
| ascii::string("$ceiling")
| ascii::string("$truncate")
| ascii::string("$round")
| ascii::string("$to_int")
| ascii::string("$to_rat")
| ascii::string("$to_real")

Definition at line 428 of file TPTPParser.cpp.

◆ defined_infix_pred

qi::rule<Iter, string()> tptp_parser::defined_infix_pred
Initial value:
=
infix_equality

Definition at line 455 of file TPTPParser.cpp.

◆ defined_predicate

qi::rule<Iter, string()> tptp_parser::defined_predicate
Initial value:
=
ascii::string("$distinct")
| ascii::string("$less")
| ascii::string("$lesseq")
| ascii::string("$greater")
| ascii::string("$greatereq")
| ascii::string("$box_P")
| ascii::string("$box_int")
| ascii::string("$greater")
| ascii::string("$box")
| ascii::string("$dia_P")
| ascii::string("$dia_i")
| ascii::string("$dia_int")
| ascii::string("$dia")

Definition at line 406 of file TPTPParser.cpp.

◆ defined_proposition

qi::rule<Iter, string()> tptp_parser::defined_proposition
Initial value:
=
ascii::string("$true")
| ascii::string("$false")
| defined_predicate

Definition at line 420 of file TPTPParser.cpp.

◆ defined_term

qi::rule<Iter, string()> tptp_parser::defined_term
Initial value:
=
number | distinct_object

Definition at line 449 of file TPTPParser.cpp.

◆ distinct_object

qi::rule<Iter, string()> tptp_parser::distinct_object
Initial value:
=
double_quote
>> *(do_char)
>> double_quote

Definition at line 325 of file TPTPParser.cpp.

◆ distinct_objects

set<string> tptp_parser::distinct_objects

Definition at line 112 of file TPTPParser.cpp.

◆ do_char

qi::rule<Iter, char()> tptp_parser::do_char
Initial value:
=
qi::char_(' ', '!')
| qi::char_('#', '[')
| qi::char_(']', '~')
| ( lit('\\') >> ( qi::char_('"') | qi::char_('\\') ) )

Definition at line 185 of file TPTPParser.cpp.

◆ dollar

qi::rule<Iter, char()> tptp_parser::dollar
Initial value:
=
qi::char_('$')

Definition at line 222 of file TPTPParser.cpp.

◆ dollar_dollar_word

qi::rule<Iter, string()> tptp_parser::dollar_dollar_word
Initial value:
=
dollar
>> dollar
>> *(alpha_numeric)

Definition at line 318 of file TPTPParser.cpp.

◆ dollar_word

qi::rule<Iter, string()> tptp_parser::dollar_word
Initial value:
=
dollar
>> *(alpha_numeric)

Definition at line 322 of file TPTPParser.cpp.

◆ dot

qi::rule<Iter, char()> tptp_parser::dot
Initial value:
=
qi::char_('.')

Definition at line 199 of file TPTPParser.cpp.

◆ dot_decimal

qi::rule<Iter, string()> tptp_parser::dot_decimal
Initial value:
=
dot >> +(numeric)

Definition at line 244 of file TPTPParser.cpp.

◆ double_quote

qi::rule<Iter, char()> tptp_parser::double_quote
Initial value:
=
qi::char_('"')

Definition at line 183 of file TPTPParser.cpp.

◆ equals_added

bool tptp_parser::equals_added

Definition at line 116 of file TPTPParser.cpp.

◆ equals_p

Predicate* tptp_parser::equals_p

Definition at line 117 of file TPTPParser.cpp.

◆ exp_integer

qi::rule<Iter, string()> tptp_parser::exp_integer
Initial value:
=
signed_exp_integer
| unsigned_exp_integer

Definition at line 241 of file TPTPParser.cpp.

◆ exponent

qi::rule<Iter, char()> tptp_parser::exponent
Initial value:
=
qi::char_("Ee")

Definition at line 201 of file TPTPParser.cpp.

◆ file_includes

vector<FileIncludeItem> tptp_parser::file_includes

Definition at line 89 of file TPTPParser.cpp.

◆ file_name

qi::rule<Iter, string()> tptp_parser::file_name
Initial value:
=
single_quoted

Definition at line 337 of file TPTPParser.cpp.

◆ fof_quantifier

qi::rule<Iter, string()> tptp_parser::fof_quantifier
Initial value:
=
ascii::string("!")
| ascii::string("?")

Definition at line 467 of file TPTPParser.cpp.

◆ formula_names

vector<string> tptp_parser::formula_names

Definition at line 144 of file TPTPParser.cpp.

◆ formula_role

qi::rule<Iter, string()> tptp_parser::formula_role
Initial value:
=
ascii::string("axiom")
| ascii::string("hypothesis")
| ascii::string("definition")
| ascii::string("assumption")
| ascii::string("lemma")
| ascii::string("theorem")
| ascii::string("corollary")
| ascii::string("conjecture")
| ascii::string("negated_conjecture")
| ascii::string("plain")
| ascii::string("type")
| ascii::string("fi_domain")
| ascii::string("fi_functors")
| ascii::string("fi_predicates")
| ascii::string("unknown")

Definition at line 294 of file TPTPParser.cpp.

◆ formula_roles

vector<string> tptp_parser::formula_roles

Definition at line 142 of file TPTPParser.cpp.

◆ found_false_axiom

bool tptp_parser::found_false_axiom = false

Definition at line 126 of file TPTPParser.cpp.

◆ found_true_axiom

bool tptp_parser::found_true_axiom = false

Definition at line 125 of file TPTPParser.cpp.

◆ fun_index_p

FunctionIndex* tptp_parser::fun_index_p

Definition at line 82 of file TPTPParser.cpp.

◆ functor

qi::rule<Iter, string()> tptp_parser::functor
Initial value:
=
atomic_word

Definition at line 398 of file TPTPParser.cpp.

◆ has_axioms

bool tptp_parser::has_axioms = false

Definition at line 128 of file TPTPParser.cpp.

◆ has_axioms_remaining

bool tptp_parser::has_axioms_remaining = false

Definition at line 129 of file TPTPParser.cpp.

◆ hash

qi::rule<Iter, string()> tptp_parser::hash
Initial value:
=
ascii::string("#")

Definition at line 287 of file TPTPParser.cpp.

◆ include_file_path

fs::path tptp_parser::include_file_path

Definition at line 103 of file TPTPParser.cpp.

◆ include_this_item

bool tptp_parser::include_this_item

Definition at line 99 of file TPTPParser.cpp.

◆ infix_equality

qi::rule<Iter, string()> tptp_parser::infix_equality
Initial value:
=
ascii::string("=")

Definition at line 451 of file TPTPParser.cpp.

◆ infix_inequality

qi::rule<Iter, string()> tptp_parser::infix_inequality
Initial value:
=
ascii::string("!=")

Definition at line 453 of file TPTPParser.cpp.

◆ integer

qi::rule<Iter, string()> tptp_parser::integer
Initial value:
=
signed_integer | unsigned_integer

Definition at line 258 of file TPTPParser.cpp.

◆ is_first_status

bool tptp_parser::is_first_status = true

Definition at line 107 of file TPTPParser.cpp.

◆ less_sign

qi::rule<Iter, string()> tptp_parser::less_sign
Initial value:
=
ascii::string("<")

Definition at line 285 of file TPTPParser.cpp.

◆ lower_alpha

qi::rule<Iter, char()> tptp_parser::lower_alpha
Initial value:
=
qi::char_('a','z')

Definition at line 213 of file TPTPParser.cpp.

◆ lower_word

qi::rule<Iter, string()> tptp_parser::lower_word
Initial value:
=
lower_alpha >> *(alpha_numeric)

Definition at line 292 of file TPTPParser.cpp.

◆ name

qi::rule<Iter, string()> tptp_parser::name
Initial value:
=
atomic_word | integer

Definition at line 404 of file TPTPParser.cpp.

◆ neg_lit

bool tptp_parser::neg_lit

Definition at line 148 of file TPTPParser.cpp.

◆ negated_conjecture_exists

bool tptp_parser::negated_conjecture_exists = false

Definition at line 127 of file TPTPParser.cpp.

◆ negated_conjecture_found

bool tptp_parser::negated_conjecture_found = false

Definition at line 122 of file TPTPParser.cpp.

◆ non_zero_numeric

qi::rule<Iter, char()> tptp_parser::non_zero_numeric
Initial value:
=
qi::char_('1','9')

Definition at line 209 of file TPTPParser.cpp.

◆ nonassoc_connective

qi::rule<Iter, string()> tptp_parser::nonassoc_connective
Initial value:
=
ascii::string("<=>")
| ascii::string("=>")
| ascii::string("<=")
| ascii::string("<~>")
| lexeme[ ascii::string("~") >> vline ]
| ascii::string("~&")

Definition at line 471 of file TPTPParser.cpp.

◆ not_star_slash

qi::rule<Iter, string()> tptp_parser::not_star_slash
Initial value:
=
*(*(qi::char_ - qi::char_('*'))
>> qi::char_('*')
>> *(qi::char_('*'))
>> (qi::char_ - (qi::char_('/') | qi::char_('*'))))
>> *(qi::char_ - qi::char_('*'))

Definition at line 367 of file TPTPParser.cpp.

◆ null

qi::rule<Iter> tptp_parser::null
Initial value:
=
eps

Definition at line 339 of file TPTPParser.cpp.

◆ number

qi::rule<Iter, string()> tptp_parser::number
Initial value:
=
integer | rational | real

Definition at line 388 of file TPTPParser.cpp.

◆ number_of_negated_conjecture_clauses

size_t tptp_parser::number_of_negated_conjecture_clauses = 0

Definition at line 131 of file TPTPParser.cpp.

◆ number_of_simplified_negated_conjecture_clauses

size_t tptp_parser::number_of_simplified_negated_conjecture_clauses = 0

Definition at line 132 of file TPTPParser.cpp.

◆ numeric

qi::rule<Iter, char()> tptp_parser::numeric
Initial value:
=
qi::char_('0','9')

Definition at line 211 of file TPTPParser.cpp.

◆ p_index_p

PredicateIndex* tptp_parser::p_index_p

Definition at line 84 of file TPTPParser.cpp.

◆ percentage_sign

qi::rule<Iter, char()> tptp_parser::percentage_sign
Initial value:
=
qi::char_('%')

Definition at line 181 of file TPTPParser.cpp.

◆ plus

qi::rule<Iter, string()> tptp_parser::plus
Initial value:
=
ascii::string("+")

Definition at line 281 of file TPTPParser.cpp.

◆ positive_decimal

qi::rule<Iter, string()> tptp_parser::positive_decimal
Initial value:
=
non_zero_numeric >> *(numeric)

Definition at line 246 of file TPTPParser.cpp.

◆ predicate

qi::rule<Iter, string()> tptp_parser::predicate
Initial value:
=
atomic_word

Definition at line 396 of file TPTPParser.cpp.

◆ printable_char

qi::rule<Iter, char()> tptp_parser::printable_char
Initial value:
=
qi::char_(' ', '~')

Definition at line 224 of file TPTPParser.cpp.

◆ proposition

qi::rule<Iter, string()> tptp_parser::proposition
Initial value:
=
predicate

Definition at line 402 of file TPTPParser.cpp.

◆ rational

qi::rule<Iter, string()> tptp_parser::rational
Initial value:
=
signed_rational | unsigned_rational

Definition at line 264 of file TPTPParser.cpp.

◆ real

qi::rule<Iter, string()> tptp_parser::real
Initial value:
=
signed_real | unsigned_real

Definition at line 270 of file TPTPParser.cpp.

◆ sign

qi::rule<Iter, char()> tptp_parser::sign
Initial value:
=
qi::char_("+-")

Definition at line 197 of file TPTPParser.cpp.

◆ signed_exp_integer

qi::rule<Iter, string()> tptp_parser::signed_exp_integer
Initial value:
=
sign >> unsigned_exp_integer

Definition at line 239 of file TPTPParser.cpp.

◆ signed_integer

qi::rule<Iter, string()> tptp_parser::signed_integer
Initial value:
=
sign >> unsigned_integer

Definition at line 256 of file TPTPParser.cpp.

◆ signed_rational

qi::rule<Iter, string()> tptp_parser::signed_rational
Initial value:
=
sign >> unsigned_rational

Definition at line 262 of file TPTPParser.cpp.

◆ signed_real

qi::rule<Iter, string()> tptp_parser::signed_real
Initial value:
=
sign >> unsigned_real

Definition at line 268 of file TPTPParser.cpp.

◆ single_quote

qi::rule<Iter, char()> tptp_parser::single_quote
Initial value:
=
qi::char_('\'')

Definition at line 190 of file TPTPParser.cpp.

◆ single_quoted

qi::rule<Iter, string()> tptp_parser::single_quoted
Initial value:
=
lit('\'')
>> sq_char
>> *(sq_char)
>> lit('\'')

Definition at line 332 of file TPTPParser.cpp.

◆ slash

qi::rule<Iter, string()> tptp_parser::slash
Initial value:
=
slash_char

Definition at line 232 of file TPTPParser.cpp.

◆ slash_char

qi::rule<Iter, char()> tptp_parser::slash_char
Initial value:
=
qi::char_('/')

Definition at line 203 of file TPTPParser.cpp.

◆ slosh

qi::rule<Iter, string()> tptp_parser::slosh
Initial value:
=
slosh_char

Definition at line 234 of file TPTPParser.cpp.

◆ slosh_char

qi::rule<Iter, char()> tptp_parser::slosh_char
Initial value:
=
qi::char_('\\')

Definition at line 205 of file TPTPParser.cpp.

◆ sq_char

qi::rule<Iter, char()> tptp_parser::sq_char
Initial value:
=
qi::char_(' ', '&')
| qi::char_('(', '[')
| qi::char_(']', '~')
| ( lit('\\') >> ( qi::char_('\'') | qi::char_('\\') ) )

Definition at line 192 of file TPTPParser.cpp.

◆ standard_comment

qi::rule<Iter, string()> tptp_parser::standard_comment
Initial value:
=
qi::char_('%')
>> *(printable_char)
>> eol

Definition at line 359 of file TPTPParser.cpp.

◆ star

qi::rule<Iter, string()> tptp_parser::star
Initial value:
=
ascii::string("*")

Definition at line 279 of file TPTPParser.cpp.

◆ status

string tptp_parser::status

Definition at line 108 of file TPTPParser.cpp.

◆ status_comment

qi::rule<Iter, string(), ascii::space_type> tptp_parser::status_comment
Initial value:
=
qi::char_('%')
>> ascii::string("Status")
>> qi::char_(':')
>> comment_status[CommentStatus()]
>> lexeme[*(printable_char)]
>> eol
CommentStatus
One of several basic semantic actions.
Definition TPTPParser.hpp:441

Definition at line 351 of file TPTPParser.cpp.

◆ system_constant

qi::rule<Iter, string()> tptp_parser::system_constant
Initial value:
=
system_functor

Definition at line 386 of file TPTPParser.cpp.

◆ system_functor

qi::rule<Iter, string()> tptp_parser::system_functor
Initial value:
=
atomic_system_word

Definition at line 384 of file TPTPParser.cpp.

◆ t_index_p

TermIndex* tptp_parser::t_index_p

Definition at line 83 of file TPTPParser.cpp.

◆ to_include

set<string> tptp_parser::to_include

Definition at line 98 of file TPTPParser.cpp.

◆ unary_connective

qi::rule<Iter, string()> tptp_parser::unary_connective
Initial value:
=
ascii::string("~")

Definition at line 483 of file TPTPParser.cpp.

◆ unsigned_exp_integer

qi::rule<Iter, string()> tptp_parser::unsigned_exp_integer
Initial value:
=
+(numeric)

Definition at line 237 of file TPTPParser.cpp.

◆ unsigned_integer

qi::rule<Iter, string()> tptp_parser::unsigned_integer
Initial value:
=
decimal

Definition at line 254 of file TPTPParser.cpp.

◆ unsigned_rational

qi::rule<Iter, string()> tptp_parser::unsigned_rational
Initial value:
=
decimal >> slash >> positive_decimal

Definition at line 260 of file TPTPParser.cpp.

◆ unsigned_real

qi::rule<Iter, string()> tptp_parser::unsigned_real
Initial value:
=
decimal_fraction | decimal_exponent

Definition at line 266 of file TPTPParser.cpp.

◆ upper_alpha

qi::rule<Iter, char()> tptp_parser::upper_alpha
Initial value:
=
qi::char_('A','Z')

Definition at line 215 of file TPTPParser.cpp.

◆ upper_word

qi::rule<Iter, string()> tptp_parser::upper_word
Initial value:
=
upper_alpha
>> *(alpha_numeric)

Definition at line 313 of file TPTPParser.cpp.

◆ var_index_p

VariableIndex* tptp_parser::var_index_p

Definition at line 81 of file TPTPParser.cpp.

◆ variable

qi::rule<Iter, string()> tptp_parser::variable
Initial value:
=
upper_word

Definition at line 316 of file TPTPParser.cpp.

◆ viewable_char

qi::rule<Iter, char()> tptp_parser::viewable_char
Initial value:
=
printable_char | eol

Definition at line 227 of file TPTPParser.cpp.

◆ vline

qi::rule<Iter, string()> tptp_parser::vline
Initial value:
=
ascii::string("|")

Definition at line 277 of file TPTPParser.cpp.

◆ zero_numeric

qi::rule<Iter, char()> tptp_parser::zero_numeric
Initial value:
=
qi::char_('0')

Definition at line 207 of file TPTPParser.cpp.