TPTPParser Class Reference

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

#include <TPTPParser.hpp>

Collaboration diagram for TPTPParser:

Public Member Functions
	TPTPParser ()=delete
	You definitely don't want this constructor.
	TPTPParser (VariableIndex *, FunctionIndex *, TermIndex *, PredicateIndex *, Matrix *, TPTPRecords *)
	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?
bool	negated_conjecture_present () const
	Did a negated conjecture turn up anywhere in the parse?
bool	no_conjecture_clause () const
	When you analysed the original problem, did you conclude that it has no conjecture clauses that can be used as a starting point?
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.
bool	problem_is_cnf_only () const
	Self-explanatory.
bool	fof_conjecture_is_true () const
	Self-explanatory.
bool	fof_conjecture_is_false () const
	Self-explanatory.
bool	fof_conjecture_is_missing () const
	Was there a conjecture clause in the problem file?
bool	fof_negated_conjecture_removed () const
	Was there a conjecture clause that got simplified away?
bool	simplified_fof_has_axioms () const
	Where there any axioms for an FOF problem after simplification?
bool	fof_has_axioms () const
	Where there any axioms for an FOF problem before simplification?

Private Member Functions
void	read_tptp_from_file (const string &)
	Read the file into a string, while stripping out and collecting comment blocks.
void	check_timeout ()

Private Attributes
string	file_contents
	Contents of the TPTP file, with comments removed.
vector< string >	comment_blocks
	Each comment is stored here.
VariableIndex *	vip
	The class has pointers to all the relevant indices.
FunctionIndex *	fip
	The class has pointers to all the relevant indices.
TermIndex *	tip
	The class has pointers to all the relevant indices.
PredicateIndex *	pip
	The class has pointers to all the relevant indices.
Matrix *	matrix
	The class has a pointer to the matrix, and can therefore construct it as it parses.
TPTPRecords *	tptp_proof_output_p
	Used to build the complete TPTP description of the proof process that's completed by the parser.

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.

Definition at line 661 of file TPTPParser.hpp.

Constructor & Destructor Documentation

TPTPParser()

TPTPParser::TPTPParser	(	VariableIndex *	new_vip,
		FunctionIndex *	new_fip,
		TermIndex *	new_tip,
		PredicateIndex *	new_pip,
		Matrix *	new_matrix,
		TPTPRecords *	_records_p )

The only constructor that makes sense.

Definition at line 1421 of file TPTPParser.cpp.

:
file_contents(),
comment_blocks(),
vip(new_vip),
fip(new_fip),
tip(new_tip),
pip(new_pip),
matrix(new_matrix),
tptp_proof_output_p(_records_p) {
  // var_index_p is global in the tptp_parser namespace. It is
  // used by semantic actions.
  var_index_p = new_vip;
  // Similar for fun_index_p and so on...
  fun_index_p = new_fip;
  t_index_p = new_tip;
  p_index_p = new_pip;
  records_p =  _records_p;
  FOF::set_recs_p(_records_p);
  // And remember that FOF also needs to use the indices.
  FOF::set_indexes(std::tuple<VariableIndex*, FunctionIndex*, PredicateIndex*, TermIndex*>
    (new_vip, new_fip, new_pip, new_tip));
  clear();
};

Member Function Documentation

check_timeout()

void TPTPParser::check_timeout ( )

inlineprivate

Periodically, we need to check whether we've exceeded the global timeout.

Definition at line 725 of file TPTPParser.hpp.

                         {
      if (!params::timeout) {
        return;
      }
      if (std::chrono::steady_clock::now() > params::global_timeout) {
          cout << endl << "% SZS status Timeout for "
               << params::problem_name
               << " : terminated by global timeout." << endl;
          exit(EXIT_FAILURE);
      }
    }

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!!??

Definition at line 1912 of file TPTPParser.cpp.

                       {
  equals_added = false;
  conjecture_found = false;
  negated_conjecture_found = false;
  conjecture_true = false;
  conjecture_false = false;
  found_true_axiom = false;
  found_false_axiom = false; 
  negated_conjecture_exists = false;
  has_axioms = false;
  has_axioms_remaining = false;
  cnf_only = false;
  number_of_negated_conjecture_clauses = 0;
  number_of_simplified_negated_conjecture_clauses = 0;
  equals_p = nullptr;
  neg_lit = false;
  is_first_status = true;
  current_clause_name = "";
  current_clause_role = "";
  current_formula_role = "";
  current_formula_name = "";
  clause_roles.clear();
  clause_names.clear();
  fof_clause_names.clear();
  formula_roles.clear();
  formula_names.clear();
  file_contents.clear();
  comment_blocks.clear();
  status = "";
  all_defined.clear();
  all_system.clear();
  distinct_objects.clear();
  current_clause.clear();
  current_formula.clear();
  all_formulas.clear();
  all_clauses.clear();
  file_includes.clear();
  to_include.clear();
  include_this_item = true;
  include_file_path = fs::path();
  include_file_name = fs::path();
}

conjecture_present()

bool TPTPParser::conjecture_present

(

)

const

Did a conjecture turn up anywhere in the parse?

Definition at line 2126 of file TPTPParser.cpp.

                                          {
  return conjecture_found;
}

equality_used()

bool TPTPParser::equality_used

(

)

Did equality turn up anywhere in the parse?

Definition at line 1963 of file TPTPParser.cpp.

                               {
  return equals_added;
}

fof_conjecture_is_false()

bool TPTPParser::fof_conjecture_is_false

(

)

const

Self-explanatory.

Definition at line 2149 of file TPTPParser.cpp.

                                               {
  return conjecture_false;
}

fof_conjecture_is_missing()

bool TPTPParser::fof_conjecture_is_missing

(

)

const

Was there a conjecture clause in the problem file?

Definition at line 2153 of file TPTPParser.cpp.

                                                 {
  return !conjecture_found;
}

fof_conjecture_is_true()

bool TPTPParser::fof_conjecture_is_true

(

)

const

Self-explanatory.

Definition at line 2144 of file TPTPParser.cpp.

                                              {
  return conjecture_true;
}

fof_has_axioms()

bool TPTPParser::fof_has_axioms

(

)

const

Where there any axioms for an FOF problem before simplification?

Definition at line 2165 of file TPTPParser.cpp.

                                      {
  return has_axioms;
}

fof_negated_conjecture_removed()

bool TPTPParser::fof_negated_conjecture_removed

(

)

const

Was there a conjecture clause that got simplified away?

Definition at line 2157 of file TPTPParser.cpp.

                                                      {
  return conjecture_found && (number_of_simplified_negated_conjecture_clauses == 0);
}

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.

Definition at line 1955 of file TPTPParser.cpp.

                                             {
  return all_defined;
}

get_equals_predicate()

Predicate * TPTPParser::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.

Definition at line 1975 of file TPTPParser.cpp.

                                                  {
  if (equals_added)
    return equals_p;
  else
    return nullptr;
}

get_problem_status()

string TPTPParser::get_problem_status

(

)

The parse tries to identify the problem status.

Definition at line 1971 of file TPTPParser.cpp.

                                      {
  return status;
}

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.

Definition at line 1959 of file TPTPParser.cpp.

                                            {
  return all_system;
}

negated_conjecture_present()

bool TPTPParser::negated_conjecture_present

(

)

const

Did a negated conjecture turn up anywhere in the parse?

Definition at line 2130 of file TPTPParser.cpp.

                                                  {
  return negated_conjecture_found;
}

no_conjecture_clause()

bool TPTPParser::no_conjecture_clause

(

)

const

When you analysed the original problem, did you conclude that it has no conjecture clauses that can be used as a starting point?

Definition at line 2134 of file TPTPParser.cpp.

                                            {
  return ((all_formulas.size() > 0 && !conjecture_found) ||
          (all_formulas.size() > 0 && (conjecture_true || conjecture_false)) ||
          (all_formulas.size() == 0 && !negated_conjecture_found) ||
          (all_formulas.size() == 0 && !negated_conjecture_exists));
}

number_of_fof_formulas()

size_t TPTPParser::number_of_fof_formulas

(

)

const

How many first-order formulas turned up in the parse?

Definition at line 1967 of file TPTPParser.cpp.

                                                {
  return all_formulas.size();
}

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.

Definition at line 1497 of file TPTPParser.cpp.

                                                             {
    /*
    * Let the parser do the heavy-lifting: get stuff from the 
    * TPTP file and parse it.
    */
    read_tptp_from_file(file_name);
 
    Iter start = file_contents.begin();
    Iter end = file_contents.end();
 
    include_file_path = params::full_problem_path;
    fs::path f(file_name);
    include_file_name = f.filename().string();
    
    TPTP_file_grammar<Iter> g;
    bool result = qi::phrase_parse(start, end, g, ascii::space);
 
    if (start != end || !result) 
      throw (file_parse_exception(file_name));
    /*
    * If you get to here, then the parser has read everything and set 
    * up a whole bunch of stuff for you. In particular, all_clauses and 
    * all_formulas have the juicy stuff.
    *
    * However, what follows gets stupidly complicated because you 
    * have to deal with a lot of rare special cases. :-(
    */
    if (pip->true_false_added() && params::verbosity > 1) 
      cout << "Found true/false." << endl;
    /*
    * First, deal with cnf(...). entries. There's not much to 
    * do as simplification can happen later.
    */
    if (negated_conjecture_found && params::verbosity > 1) 
      cout << "Found negated conjecture." << endl;
    /* 
    * Now do clause conversion for the fof(...). entries.
    *
    * Remember: negate the conjecture if necessary.
    */
    if (conjecture_found && params::verbosity > 1 && params::first_parse) 
      cout << "Found conjecture." << endl;
    /*
    * Were there any first_order items, or is it just CNF?
    */
    cnf_only = (all_formulas.size() == 0);
    if (cnf_only && params::verbosity > 1) 
      cout << "The problem is CNF only." << endl;
    /*
    * First do a check for general oddness.
    */
    if (negated_conjecture_found && conjecture_found) {
        cout << "% SZS status Error for " 
             << params::problem_name 
             << " : conjecture and negated conjecture found in the same problem." << endl;
        exit(EXIT_FAILURE);
    }
    if (!negated_conjecture_found && !conjecture_found && params::verbosity > 1) {
      cout << "No conjecture or negated conjecture found." << endl;
    } 
    if (negated_conjecture_found && all_formulas.size() > 0 && params::verbosity > 1) {
      cout << "% SZS status Error for " 
           << params::problem_name 
           << " : negated conjecture found in FOF problem." << endl;
      exit(EXIT_FAILURE);
    } 
    /*
    * Now we can convert some formulas to clauses.
    *
    * Remember: different things need to happen here depending on the state 
    * of params::no_definitional and params::all_definitional.
    */
    if (params::no_definitional && params::all_definitional) {
        cout << "% SZS status Error for " 
             << params::problem_name 
             << " : --all-definitional and --no-definitional have both been set." << endl;
        exit(EXIT_FAILURE);
    }
    /*
    * Later on I'll need to know whether the original (FOF) problem 
    * actually had axioms.
    */
    has_axioms = (all_clauses.size() > 0); 
    if (!has_axioms) {
      for (const string& s : formula_roles) {
        if (s != "conjecture") {
          has_axioms = true;
          break;
        }
      }
    }
    /*
    * Do the conversion to clauses and store the results. 
    * Don't simplify yet.
    */   
    vector<vector<Clause>> all_fof_clauses;
    bool found_one_conjecture = false;
    vector<bool> definitional_conversion;
    size_t i = 0;
    size_t conjecture_index = 0;
    records_p->reset_indices();
    records_p->set_current_name("f");
    for (FOF f : all_formulas) {
       records_p->next_index_1();
       records_p->reset_index_2();
       records_p->set_current_source(records_p->find_fof_name(i + 1));
       records_p->reset_last_f();
       check_timeout();
       if (params::verbosity > 2) {
        cout << "Converting formula: " << std::to_string(i) << endl;
       }
       vector<Clause> vc;
       vector<string> cnf_names;
       if (formula_roles[i] == string("conjecture")) {
            conjecture_index = i;
            if (found_one_conjecture) {
              cout << "% SZS status Error for " 
              << params::problem_name 
              << " : more than one conjecture in the input file." << endl;
              exit(EXIT_FAILURE);
            }
            else {
              found_one_conjecture = true;
            }
            // This is rather important!
            f.negate(); 
            formula_roles[i] = "negated_conjecture";
            
            records_p->set_current_role("negated_conjecture");
            records_p->add_fof_inference_record("negate,[status(cth)]",
                                            f.to_tptp_string());
            if (!params::no_definitional) {
                f.definitional_convert_to_cnf_clauses(vc, cnf_names, formula_roles[i]);
                definitional_conversion.push_back(true);
            }
            else {
                f.convert_to_cnf_clauses(vc, cnf_names, formula_roles[i]);
                definitional_conversion.push_back(false);
            }
            number_of_negated_conjecture_clauses = vc.size();
       } 
       else {
            records_p->set_current_role("plain");
            if (params::all_definitional || !conjecture_found) {
                f.definitional_convert_to_cnf_clauses(vc, cnf_names, formula_roles[i]);
                definitional_conversion.push_back(true);
            }
            else {
                 f.convert_to_cnf_clauses(vc, cnf_names, formula_roles[i]);
                 definitional_conversion.push_back(false);
            }
       }
       all_fof_clauses.push_back(vc);
       fof_clause_names.push_back(cnf_names);
       i++;
    }
    /*
    * Now all_fof_clauses has unsimplified clauses, as
    * does all_clauses. We also know where any conjecture 
    * is.
    *
    * Before doing anything else, it might be that all we 
    * want is to see the clause conversion.
    */
    i = 0;
    if (params::show_clauses) {
      for (vector<Clause>& vc : all_fof_clauses) {
        cout << "---------------------" << endl;
        cout << "Formula: " << formula_names[i] << ", " 
             << formula_roles[i] << endl;
        cout << all_formulas[i] << endl;
        cout << "Clauses:";
        if (definitional_conversion[i]) {
          cout << " (definitional conversion)";
        } 
        cout << endl;
        FOF::simplify_cnf(vc);
        for (const Clause& c : vc) {
          cout << c << endl;
        } 
        i++;
      }
      exit(EXIT_SUCCESS);
    }
    /*
    * OK - so we've got more to do. Now simplify everything, 
    * but keep track of any strange cases.
    *
    * Start with the case when the problem is CNF only.
    */
    SimplificationResult cnf_result = FOF::simplify_cnf(all_clauses, clause_roles, clause_names);
    check_timeout();
    /* 
    * Did we somehow manage to delete all the negated conjectures?
    */
    for (const string& s : clause_roles) {
      if (s == string("negated_conjecture")) {
        negated_conjecture_exists = true;
        break;
      }
    }
    string output_string; 
    vector<Clause> simplified_fof_clauses;
    vector<string> simplified_fof_roles;
    vector<string> simplified_fof_names;
    /*
    * Note that we can draw the following conclusions regardless of whether 
    * or not any equality axioms have been added.
    */
    if (all_formulas.size() == 0) {
        if (cnf_result == SimplificationResult::Tautology) {
          output_string = "Satisfiable";
        }
        if (cnf_result == SimplificationResult::Contradiction) {
          output_string = "Unsatisfiable";
        }
        if (output_string != "") {
          cout << "% SZS status " << output_string << " for " 
               << params::problem_name 
               << " : established by clause simplification." << endl;
          if (params::generate_tptp_proof) {
            cout << "% SZS output start Proof for " << params::problem_name << endl;
            unordered_set<string> names;
            cout << records_p->to_tptp_string(names) << endl;
            cout << "% SZS output end Proof for " << params::problem_name << endl;
          }
          std::exit(EXIT_SUCCESS);
        }
    }
    // Here, we know it's a problem with FOF stuff in it.
    else {
      i = 0;
      for (vector<Clause> cs : all_fof_clauses) {
        check_timeout();
        vector<string> temporary_clause_roles(cs.size(), formula_roles[i]);
        vector<string> temporary_clause_names = fof_clause_names[i];
 
        SimplificationResult fof_result = FOF::simplify_cnf(cs, 
                            temporary_clause_roles, 
                            temporary_clause_names);
 
        if (i == conjecture_index && conjecture_found) {
          number_of_simplified_negated_conjecture_clauses = cs.size();
        }
 
        if (fof_result == SimplificationResult::Tautology) {
          if (i == conjecture_index && conjecture_found) {
            conjecture_false = true;
            if (params::verbosity > 1) {
              cout << "The conjecture is equivalent to $false." << endl;
            }
          }
          else {
            found_true_axiom = true; 
            if (params::verbosity > 1) {
              cout << "Axiom is equivalent to $true." << endl;
            }
          }
          i++;
          continue;
        }
        else if (fof_result == SimplificationResult::Contradiction) {
          if (i == conjecture_index && conjecture_found) {
            conjecture_true = true;
            if (params::verbosity > 1) {
              cout << "The conjecture is equivalent to $true." << endl;
            }
          }
          else {
            found_false_axiom = true;
            if (params::verbosity > 1) {
              cout << "Axiom is equivalent to $false." << endl;
            }
          }
          i++;
          continue;
        }
        else {
          size_t j = 0;
          for (const Clause& c : cs) {
            simplified_fof_clauses.push_back(c);
            simplified_fof_roles.push_back(temporary_clause_roles[j]);
            simplified_fof_names.push_back(temporary_clause_names[j]);
            j++;
          }
          i++;
        }
      } 
    }
    /*
    * Remember: this actually does some setup work, so don't do it 
    * until *everything* else is in place. In particular, definitional 
    * clause conversion can introduce new predicates, so this has to 
    * happen later.
    */
    matrix->set_num_preds(pip->get_num_preds());
 
    i = 0;
    for (Clause& c : all_clauses) {
      matrix->add_clause(c, clause_roles[i], clause_names[i]);
      i++;
    }
    /*
    * If it's a CNF only problem we're done! However, if there are FOF 
    * clauses then we have to deal with all the silly possibilities.
    */
    if (all_formulas.size() > 0) {
      /*
      * Now I know about all odd instances where a part of the problem  
      * gave rise to clauses that were equivalent to $true or $false.
      *
      * Does this allow me to stop?
      */
      string output_string;
      if (cnf_result == SimplificationResult::Contradiction || found_false_axiom) {
        if (conjecture_true) {
          output_string = "TautologousConclusionContradictoryAxioms";
        }
        else if (conjecture_false) {
          output_string = "UnsatisfiableConclusionContradictoryAxioms";
        }
        else if (!conjecture_found) {
          output_string = "Unsatisfiable";
        }
        else {
          output_string = "ContradictoryAxioms";
        }
      }
      else {
        /* 
        * The case of something in the axioms being $true just shrinks the 
        * set of axioms. So you need to handle the situation where there 
        * are no axioms remaining!
        */
        has_axioms_remaining = (all_clauses.size() > 0); 
        if (!has_axioms_remaining) {
          for (const string& s : simplified_fof_roles) {
            if (s != "conjecture") {
              has_axioms_remaining = true;
              break;
            }
          }
        }
        if (has_axioms_remaining) {
          /*
          * So: assuming you have some axioms, what happens if the conjecture 
          * was $true or $false?
          *
          * If the conjecture is $false then, as you have axioms, the outcome 
          * still needs to be determined in case the axioms are contradictory.
          */
          if (conjecture_true) {
            output_string = "Theorem";
          }       
          /*
          * We now have just axioms, or axioms with a false conjecture, so 
          * keep going and sort it out later -- 
          */
        }
        /*
        * We have no axioms.
        */
        else {
          if (conjecture_true) {
            output_string = "Theorem";
          }
          if (conjecture_false) {
            output_string = "CounterSatisfiable";
          }
          if (!conjecture_found) {
            output_string = "Theorem";
          }
         /*
         * We now have just a conjecture (or not), so keep going and sort it out 
         * later -- 
         */
        }
      }
      if (output_string != "") {
        cout << "% SZS status " << output_string << " for " 
             << params::problem_name 
             << " : established by clause simplification." << endl;
        if (params::generate_tptp_proof) {
            cout << "% SZS output start Proof for " << params::problem_name << endl;
            unordered_set<string> names;
            cout << records_p->to_tptp_string(names) << endl;
            cout << "% SZS output end Proof for " << params::problem_name << endl;
        }
        exit(EXIT_SUCCESS);
      }
      /*
      * If none of the special cases forced us to stop, then add the 
      * FOF material to the matrix.
      */
      i = 0;
      for (Clause& c : simplified_fof_clauses) {
        matrix->add_clause(c, simplified_fof_roles[i], simplified_fof_names[i]);
        i++;
      }
    }
    return true;
}

problem_is_cnf_only()

bool TPTPParser::problem_is_cnf_only

(

)

const

Self-explanatory.

Definition at line 2140 of file TPTPParser.cpp.

                                           {
  return cnf_only;
}

read_tptp_from_file()

void TPTPParser::read_tptp_from_file ( const string & file_name )

private

Read the file into a string, while stripping out and collecting comment blocks.

(Yes, better done with a custom skip parser, but writing those is a pain.)

Parameters

file_name

Reference to a string containing the file name

Definition at line 1453 of file TPTPParser.cpp.

                                                            {
    // Used to collect up comments as you see them.
    string comment;
    bool in_comment = false;
    
    char c;
 
    ifstream file;
    file.unsetf(std::ios_base::skipws);
    file.open(file_name);
    if (file.fail()) {
      throw (file_open_exception(file_name));
    }
    file.get(c);
    while (file.good()) {
        // Detect the start of a comment.
        if (!in_comment && c == '/') {
            if (file.peek() == '*') {
                file.get(c);
                in_comment = true;
                comment.clear();
            }
            else file_contents += c;
        }
        // Detect the end of a comment.
        else if (in_comment && c == '*') {
            if (file.peek() == '/') {
                file.get(c);
                in_comment = false;
                comment_blocks.push_back(comment);
            }
            else comment += c;
        }
        // Nothings to see. We're just adding to the
        // relevant output.
        else if (in_comment)
             comment += c;
        else
            file_contents += c;
        file.get(c);
    }
    file.close();
}

show_file_includes()

void TPTPParser::show_file_includes

(

)

Show any includes present in the TPTP file.

These are collected as part of the parse.

Definition at line 1900 of file TPTPParser.cpp.

                                    {
    for (FileIncludeItem i : file_includes) {
        cout << "From " << i.first << ": ";
        if (i.second.size() == 0)
            cout << "all";
        else
            for (string s : i.second)
                cout << s << " ";
        cout << endl;
    }
}

simplified_fof_has_axioms()

bool TPTPParser::simplified_fof_has_axioms

(

)

const

Where there any axioms for an FOF problem after simplification?

Definition at line 2161 of file TPTPParser.cpp.

                                                 {
  return has_axioms_remaining;
}

Member Data Documentation

comment_blocks

vector<string> TPTPParser::comment_blocks

private

Each comment is stored here.

Definition at line 672 of file TPTPParser.hpp.

file_contents

string TPTPParser::file_contents

private

Contents of the TPTP file, with comments removed.

Assuming of course that you used read_tptp_from_file.

Definition at line 668 of file TPTPParser.hpp.

fip

FunctionIndex* TPTPParser::fip

private

The class has pointers to all the relevant indices.

These are used directly to make the actual data structures used by the prover.

Definition at line 686 of file TPTPParser.hpp.

matrix

Matrix* TPTPParser::matrix

private

The class has a pointer to the matrix, and can therefore construct it as it parses.

Definition at line 705 of file TPTPParser.hpp.

pip

PredicateIndex* TPTPParser::pip

private

The class has pointers to all the relevant indices.

These are used directly to make the actual data structures used by the prover.

Definition at line 700 of file TPTPParser.hpp.

tip

TermIndex* TPTPParser::tip

private

The class has pointers to all the relevant indices.

These are used directly to make the actual data structures used by the prover.

Definition at line 693 of file TPTPParser.hpp.

tptp_proof_output_p

TPTPRecords* TPTPParser::tptp_proof_output_p

private

Used to build the complete TPTP description of the proof process that's completed by the parser.

Definition at line 710 of file TPTPParser.hpp.

vip

VariableIndex* TPTPParser::vip

private

The class has pointers to all the relevant indices.

These are used directly to make the actual data structures used by the prover.

Definition at line 679 of file TPTPParser.hpp.

---

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

• /Users/sbh11/Desktop/connection-prover/c++/connect++/source/TPTPParser.hpp
• /Users/sbh11/Desktop/connection-prover/c++/connect++/source/TPTPParser.cpp