Connect++ 0.7.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 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
 
TPTPRecords * records_p
 
vector< FileIncludeItem > file_includes
 
set< string > to_include
 
bool include_this_item
 
fs::path include_file_path
 
fs::path include_file_name
 
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_name
 
string current_clause_role
 
vector< string > clause_names
 
vector< string > clause_roles
 
vector< vector< string > > fof_clause_names
 
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 92 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 121 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 1982 of file TPTPParser.cpp.

1983 {
1984
1985 bool in_comment = false;
1986 char c;
1987
1988 ifstream file;
1989 file.unsetf(std::ios_base::skipws);
1990 file.open(file_name);
1991 if (file.fail()) {
1992 throw (file_open_exception(file_name));
1993 }
1994 file.get(c);
1995 while (file.good()) {
1996 // Detect the start of a comment.
1997 if (!in_comment && c == '/') {
1998 if (file.peek() == '*') {
1999 file.get(c);
2000 in_comment = true;
2001 }
2002 else file_contents += c;
2003 }
2004 // Detect the end of a comment.
2005 else if (in_comment && c == '*') {
2006 if (file.peek() == '/') {
2007 file.get(c);
2008 in_comment = false;
2009 }
2010 }
2011 // Nothings to see. We're just adding to the
2012 // relevant output.
2013 else if (!in_comment)
2014 file_contents += c;
2015
2016 file.get(c);
2017 }
2018 file.close();
2019}
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 2027 of file TPTPParser.cpp.

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

Variable Documentation

◆ all_clauses

vector<Clause> tptp_parser::all_clauses

Definition at line 156 of file TPTPParser.cpp.

◆ all_defined

vector<string> tptp_parser::all_defined

Definition at line 112 of file TPTPParser.cpp.

◆ all_formulas

vector<FOF> tptp_parser::all_formulas

Definition at line 161 of file TPTPParser.cpp.

◆ all_system

vector<string> tptp_parser::all_system

Definition at line 113 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 222 of file TPTPParser.cpp.

◆ arrow

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

Definition at line 288 of file TPTPParser.cpp.

◆ assoc_connective

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

Definition at line 484 of file TPTPParser.cpp.

◆ atomic_defined_word

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

Definition at line 385 of file TPTPParser.cpp.

◆ atomic_system_word

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

Definition at line 387 of file TPTPParser.cpp.

◆ atomic_word

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

Definition at line 398 of file TPTPParser.cpp.

◆ clause_names

vector<string> tptp_parser::clause_names

Definition at line 140 of file TPTPParser.cpp.

◆ clause_roles

vector<string> tptp_parser::clause_roles

Definition at line 141 of file TPTPParser.cpp.

◆ cnf_only

bool tptp_parser::cnf_only = false

Definition at line 132 of file TPTPParser.cpp.

◆ comment

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

Definition at line 383 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 378 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 369 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 347 of file TPTPParser.cpp.

◆ conjecture_false

bool tptp_parser::conjecture_false = false

Definition at line 126 of file TPTPParser.cpp.

◆ conjecture_found

bool tptp_parser::conjecture_found = false

Definition at line 123 of file TPTPParser.cpp.

◆ conjecture_true

bool tptp_parser::conjecture_true = false

Definition at line 125 of file TPTPParser.cpp.

◆ constant

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

Definition at line 405 of file TPTPParser.cpp.

◆ current_clause

Clause tptp_parser::current_clause

Definition at line 155 of file TPTPParser.cpp.

◆ current_clause_name

string tptp_parser::current_clause_name

Definition at line 138 of file TPTPParser.cpp.

◆ current_clause_role

string tptp_parser::current_clause_role

Definition at line 139 of file TPTPParser.cpp.

◆ current_formula_name

string tptp_parser::current_formula_name

Definition at line 148 of file TPTPParser.cpp.

◆ current_formula_role

string tptp_parser::current_formula_role

Definition at line 146 of file TPTPParser.cpp.

◆ current_lit

Literal tptp_parser::current_lit

Definition at line 154 of file TPTPParser.cpp.

◆ decimal

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

Definition at line 253 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 257 of file TPTPParser.cpp.

◆ decimal_fraction

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

Definition at line 255 of file TPTPParser.cpp.

◆ defined_constant

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

Definition at line 452 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 433 of file TPTPParser.cpp.

◆ defined_infix_pred

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

Definition at line 460 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 411 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 425 of file TPTPParser.cpp.

◆ defined_term

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

Definition at line 454 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 330 of file TPTPParser.cpp.

◆ distinct_objects

set<string> tptp_parser::distinct_objects

Definition at line 114 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 190 of file TPTPParser.cpp.

◆ dollar

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

Definition at line 227 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 323 of file TPTPParser.cpp.

◆ dollar_word

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

Definition at line 327 of file TPTPParser.cpp.

◆ dot

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

Definition at line 204 of file TPTPParser.cpp.

◆ dot_decimal

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

Definition at line 249 of file TPTPParser.cpp.

◆ double_quote

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

Definition at line 188 of file TPTPParser.cpp.

◆ equals_added

bool tptp_parser::equals_added

Definition at line 118 of file TPTPParser.cpp.

◆ equals_p

Predicate* tptp_parser::equals_p

Definition at line 119 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 246 of file TPTPParser.cpp.

◆ exponent

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

Definition at line 206 of file TPTPParser.cpp.

◆ file_includes

vector<FileIncludeItem> tptp_parser::file_includes

Definition at line 90 of file TPTPParser.cpp.

◆ file_name

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

Definition at line 342 of file TPTPParser.cpp.

◆ fof_clause_names

vector<vector<string> > tptp_parser::fof_clause_names

Definition at line 142 of file TPTPParser.cpp.

◆ fof_quantifier

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

Definition at line 472 of file TPTPParser.cpp.

◆ formula_names

vector<string> tptp_parser::formula_names

Definition at line 149 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 299 of file TPTPParser.cpp.

◆ formula_roles

vector<string> tptp_parser::formula_roles

Definition at line 147 of file TPTPParser.cpp.

◆ found_false_axiom

bool tptp_parser::found_false_axiom = false

Definition at line 128 of file TPTPParser.cpp.

◆ found_true_axiom

bool tptp_parser::found_true_axiom = false

Definition at line 127 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 403 of file TPTPParser.cpp.

◆ has_axioms

bool tptp_parser::has_axioms = false

Definition at line 130 of file TPTPParser.cpp.

◆ has_axioms_remaining

bool tptp_parser::has_axioms_remaining = false

Definition at line 131 of file TPTPParser.cpp.

◆ hash

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

Definition at line 292 of file TPTPParser.cpp.

◆ include_file_name

fs::path tptp_parser::include_file_name

Definition at line 105 of file TPTPParser.cpp.

◆ include_file_path

fs::path tptp_parser::include_file_path

Definition at line 104 of file TPTPParser.cpp.

◆ include_this_item

bool tptp_parser::include_this_item

Definition at line 100 of file TPTPParser.cpp.

◆ infix_equality

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

Definition at line 456 of file TPTPParser.cpp.

◆ infix_inequality

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

Definition at line 458 of file TPTPParser.cpp.

◆ integer

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

Definition at line 263 of file TPTPParser.cpp.

◆ is_first_status

bool tptp_parser::is_first_status = true

Definition at line 109 of file TPTPParser.cpp.

◆ less_sign

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

Definition at line 290 of file TPTPParser.cpp.

◆ lower_alpha

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

Definition at line 218 of file TPTPParser.cpp.

◆ lower_word

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

Definition at line 297 of file TPTPParser.cpp.

◆ name

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

Definition at line 409 of file TPTPParser.cpp.

◆ neg_lit

bool tptp_parser::neg_lit

Definition at line 153 of file TPTPParser.cpp.

◆ negated_conjecture_exists

bool tptp_parser::negated_conjecture_exists = false

Definition at line 129 of file TPTPParser.cpp.

◆ negated_conjecture_found

bool tptp_parser::negated_conjecture_found = false

Definition at line 124 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 214 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 476 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 372 of file TPTPParser.cpp.

◆ null

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

Definition at line 344 of file TPTPParser.cpp.

◆ number

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

Definition at line 393 of file TPTPParser.cpp.

◆ number_of_negated_conjecture_clauses

size_t tptp_parser::number_of_negated_conjecture_clauses = 0

Definition at line 133 of file TPTPParser.cpp.

◆ number_of_simplified_negated_conjecture_clauses

size_t tptp_parser::number_of_simplified_negated_conjecture_clauses = 0

Definition at line 134 of file TPTPParser.cpp.

◆ numeric

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

Definition at line 216 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 186 of file TPTPParser.cpp.

◆ plus

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

Definition at line 286 of file TPTPParser.cpp.

◆ positive_decimal

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

Definition at line 251 of file TPTPParser.cpp.

◆ predicate

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

Definition at line 401 of file TPTPParser.cpp.

◆ printable_char

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

Definition at line 229 of file TPTPParser.cpp.

◆ proposition

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

Definition at line 407 of file TPTPParser.cpp.

◆ rational

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

Definition at line 269 of file TPTPParser.cpp.

◆ real

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

Definition at line 275 of file TPTPParser.cpp.

◆ records_p

TPTPRecords* tptp_parser::records_p

Definition at line 85 of file TPTPParser.cpp.

◆ sign

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

Definition at line 202 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 244 of file TPTPParser.cpp.

◆ signed_integer

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

Definition at line 261 of file TPTPParser.cpp.

◆ signed_rational

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

Definition at line 267 of file TPTPParser.cpp.

◆ signed_real

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

Definition at line 273 of file TPTPParser.cpp.

◆ single_quote

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

Definition at line 195 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 337 of file TPTPParser.cpp.

◆ slash

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

Definition at line 237 of file TPTPParser.cpp.

◆ slash_char

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

Definition at line 208 of file TPTPParser.cpp.

◆ slosh

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

Definition at line 239 of file TPTPParser.cpp.

◆ slosh_char

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

Definition at line 210 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 197 of file TPTPParser.cpp.

◆ standard_comment

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

Definition at line 364 of file TPTPParser.cpp.

◆ star

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

Definition at line 284 of file TPTPParser.cpp.

◆ status

string tptp_parser::status

Definition at line 110 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:444

Definition at line 356 of file TPTPParser.cpp.

◆ system_constant

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

Definition at line 391 of file TPTPParser.cpp.

◆ system_functor

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

Definition at line 389 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 99 of file TPTPParser.cpp.

◆ unary_connective

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

Definition at line 488 of file TPTPParser.cpp.

◆ unsigned_exp_integer

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

Definition at line 242 of file TPTPParser.cpp.

◆ unsigned_integer

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

Definition at line 259 of file TPTPParser.cpp.

◆ unsigned_rational

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

Definition at line 265 of file TPTPParser.cpp.

◆ unsigned_real

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

Definition at line 271 of file TPTPParser.cpp.

◆ upper_alpha

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

Definition at line 220 of file TPTPParser.cpp.

◆ upper_word

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

Definition at line 318 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 321 of file TPTPParser.cpp.

◆ viewable_char

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

Definition at line 232 of file TPTPParser.cpp.

◆ vline

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

Definition at line 282 of file TPTPParser.cpp.

◆ zero_numeric

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

Definition at line 212 of file TPTPParser.cpp.