diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-08-16 15:15:03 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-13 18:32:39 -0400 |
commit | 14776d0aeb833a7e728a27af6ef545f20b495f7f (patch) | |
tree | eccc91e0be00cfb9af7d757aae3dd07479c256fb /src/parser | |
parent | 09fc93244e10b4450592b4ede151873142d54b34 (diff) |
Documentation fixes, some code typo fixes, file perms, other minor things.
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/smt2/Smt2.g | 4 | ||||
-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 |
5 files changed, 7 insertions, 7 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 74434f499..5aa1e53e4 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -342,7 +342,7 @@ command returns [CVC4::Command* cmd = NULL] ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); } term[expr, expr2] { cmd = new AssertCommand(expr); } - | /* checksat */ + | /* check-sat */ CHECKSAT_TOK { PARSER_STATE->checkThatLogicIsSet(); } ( term[expr, expr2] { if(PARSER_STATE->strictModeEnabled()) { @@ -781,7 +781,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] (kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) { /* Unary AND/OR can be replaced with the argument. - It just so happens expr should already by the only argument. */ + * It just so happens expr should already be the only argument. */ assert( expr == args[0] ); } else if( CVC4::kind::isAssociative(kind) && args.size() > EXPR_MANAGER->maxArity(kind) ) { 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: |