diff options
Diffstat (limited to 'src/parser/tptp')
-rw-r--r-- | src/parser/tptp/Tptp.g | 2 | ||||
-rw-r--r-- | src/parser/tptp/tptp.cpp | 4 | ||||
-rw-r--r-- | src/parser/tptp/tptp.h | 2 | ||||
-rw-r--r-- | src/parser/tptp/tptp_input.h | 2 |
4 files changed, 5 insertions, 5 deletions
diff --git a/src/parser/tptp/Tptp.g b/src/parser/tptp/Tptp.g index 2ae31e810..61e0999e9 100644 --- a/src/parser/tptp/Tptp.g +++ b/src/parser/tptp/Tptp.g @@ -189,7 +189,7 @@ parseCommand returns [CVC4::Command* cmd = NULL] } */ PARSER_STATE->includeFile(name /* , inclArgs */ ); - // The command of the included file will be produced at the new parseCommand call + // The command of the included file will be produced at the next parseCommand() call cmd = new EmptyCommand("include::" + name); } | EOF diff --git a/src/parser/tptp/tptp.cpp b/src/parser/tptp/tptp.cpp index 3e6aa82b7..edffaa01f 100644 --- a/src/parser/tptp/tptp.cpp +++ b/src/parser/tptp/tptp.cpp @@ -107,7 +107,7 @@ bool newInputStream(std::string fileName, pANTLR3_LEXER lexer) { Debug("parser") << "Can't open " << fileName << std::endl; return false; } - // Samething than the predefined PUSHSTREAM(in); + // Same thing as the predefined PUSHSTREAM(in); lexer->pushCharStream(lexer,in); // restart it //lexer->rec->state->tokenStartCharIndex = -10; @@ -163,7 +163,7 @@ void Tptp::includeFile(std::string fileName) { // Test in the directory of the actual parsed file std::string currentDirFileName; if(inputName != "<stdin>") { - // TODO: Use dirname ot Boost::filesystem? + // TODO: Use dirname or Boost::filesystem? size_t pos = inputName.rfind('/'); if(pos != std::string::npos) { currentDirFileName = std::string(inputName, 0, pos + 1); diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index eb49d7dcc..e180d1524 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -203,7 +203,7 @@ inline void Tptp::makeApplication(Expr& expr, std::string& name, inline Command* Tptp::makeCommand(FormulaRole fr, Expr& expr, bool cnf) { // For SZS ontology compliance. - // If we're in cnf() though, conjectures don't result in "Theorem" or + // if we're in cnf() though, conjectures don't result in "Theorem" or // "CounterSatisfiable". if(!cnf && (fr == FR_NEGATED_CONJECTURE || fr == FR_CONJECTURE)) { d_hasConjecture = true; diff --git a/src/parser/tptp/tptp_input.h b/src/parser/tptp/tptp_input.h index 19e928e7e..cb2bcd3a3 100644 --- a/src/parser/tptp/tptp_input.h +++ b/src/parser/tptp/tptp_input.h @@ -64,7 +64,7 @@ public: /** Get the language that this Input is reading. */ InputLanguage getLanguage() const throw() { - return language::input::LANG_SMTLIB_V2; + return language::input::LANG_TPTP; } protected: |