Adding --strict-parsing option

diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index b24e91803b00cd235c764c5e110dff3df9ca0702..fda0bf766095d808a32d6cd69ad7467fd1b57172 100644 (file)
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -62,7 +62,8 @@ enum OptionValue {
   PARSE_ONLY,
   NO_CHECKING,
   USE_MMAP,
-  SHOW_CONFIG
+  SHOW_CONFIG,
+  STRICT_PARSING
 };/* enum OptionValue */
 
 /**
@@ -104,7 +105,8 @@ static struct option cmdlineOptions[] = {
   { "about"      , no_argument      , NULL, 'V'         },
   { "lang"       , required_argument, NULL, 'L'         },
   { "parse-only" , no_argument      , NULL, PARSE_ONLY  },
-  { "mmap",        no_argument      , NULL, USE_MMAP    }
+  { "mmap",        no_argument      , NULL, USE_MMAP    },
+  { "strict-parsing", no_argument   , NULL, STRICT_PARSING },
 };/* if you add things to the above, please remember to update usage.h! */
 
 /** Full argv[0] */
@@ -210,6 +212,10 @@ throw(OptionException) {
       opts->memoryMap = true;
       break;
 
+    case STRICT_PARSING:
+      opts->strictParsing = true;
+      break;
+
     case SHOW_CONFIG:
       fputs(Configuration::about().c_str(), stdout);
       printf("\n");

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 037dde559af2e2f79c1c13197d6043642cf46d41..19e1d0cffa764af7b20de3e5b4b338f4ad0573b4 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -165,6 +165,10 @@ int runCvc4(int argc, char* argv[]) {
     parser.disableChecks();
   }
 
+  if( options.strictParsing ) {
+    parser.enableStrictMode();
+  }
+
   // Parse and execute commands until we are done
   Command* cmd;
   while((cmd = parser.nextCommand())) {

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index d788a2c3ffe62e917afa0ac44510de7101d9651f..a393bc85fe49ceb795c3ab98515acf51033adf2f 100644 (file)
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -209,14 +209,6 @@ void Parser::checkArity(Kind kind, unsigned int numArgs)
   }
 }
 
-void Parser::enableChecks() {
-  d_checksEnabled = true;
-}
-
-void Parser::disableChecks() {
-  d_checksEnabled = false;
-}
-
 Command* Parser::nextCommand() throw(ParserException) {
   Debug("parser") << "nextCommand()" << std::endl;
   Command* cmd = NULL;

diff --git a/src/parser/parser.h b/src/parser/parser.h
index f56ec03acc577810cc2edaa9f49c4b6fccc0365a..25d7f2cd184fd2f8979241ae5e92f521298f185d 100644 (file)
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -113,6 +113,8 @@ class CVC4_PUBLIC Parser {
   /** Are semantic checks enabled during parsing? */
   bool d_checksEnabled;
 
+  /** Are we parsing in strict mode? */
+  bool d_strictMode;
 
   /** Lookup a symbol in the given namespace. */
   Expr getSymbol(const std::string& var_name, SymbolType type);
@@ -158,10 +160,18 @@ public:
   }
 
   /** Enable semantic checks during parsing. */
-  void enableChecks();
+  void enableChecks() { d_checksEnabled = true; }
 
   /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */
-  void disableChecks();
+  void disableChecks() { d_checksEnabled = false; }
+
+  /** Enable strict parsing, according to the language standards. */
+  void enableStrictMode() { d_strictMode = true; }
+
+  /** Disable strict parsing. Allows certain syntactic infelicities to pass without comment. */
+  void disableStrictMode() { d_strictMode = false; }
+
+  bool strictModeEnabled() { return d_strictMode; }
 
   /** Get the name of the input file. */
 /*

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index fd5e334ed8005da9fd628f8186038ad3567b80e9..bcab391835299b32d7108f24c7c6bad5d7b80577 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -208,7 +208,9 @@ term[CVC4::Expr& expr]
 } 
   : /* a built-in operator application */
     LPAREN_TOK builtinOp[kind] termList[args,expr] RPAREN_TOK 
-    { if((kind == CVC4::kind::AND || kind == CVC4::kind::OR) && args.size() == 1) {
+    { if( !PARSER_STATE->strictModeEnabled() && 
+          (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. */
         Assert( expr == args[0] );

diff --git a/src/util/options.h b/src/util/options.h
index d095d98d33aadd9ad0aefa5950fd4daaa30499f5..c7a730b1441cb4a57ba0971baa017cfc03bf1742 100644 (file)
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -53,6 +53,9 @@ struct CVC4_PUBLIC Options {
   /** Should the parser memory-map file input? */
   bool memoryMap;
 
+  /** Should we strictly enforce the language standard while parsing? */
+  bool strictParsing;
+
   Options() : binary_name(),
               statistics(false),
               out(0),
@@ -61,7 +64,8 @@ struct CVC4_PUBLIC Options {
               lang(parser::LANG_AUTO),
               parseOnly(false),
               semanticChecks(true),
-              memoryMap(false)
+              memoryMap(false),
+              strictParsing(false)
   {}
 };/* struct Options */