From d292e8c233305c402da65a1cf97668881f7b099c Mon Sep 17 00:00:00 2001
From: "Christopher L. Conway" <christopherleeconway@gmail.com>
Date: Thu, 6 May 2010 21:11:43 +0000
Subject: Adding --strict-parsing option

---
 src/main/getopt.cpp    | 10 ++++++++--
 src/main/main.cpp      |  4 ++++
 src/parser/parser.cpp  |  8 --------
 src/parser/parser.h    | 14 ++++++++++++--
 src/parser/smt2/Smt2.g |  4 +++-
 src/util/options.h     |  6 +++++-
 6 files changed, 32 insertions(+), 14 deletions(-)

diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index b24e91803..fda0bf766 100644
--- 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 037dde559..19e1d0cff 100644
--- 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 d788a2c3f..a393bc85f 100644
--- 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 f56ec03ac..25d7f2cd1 100644
--- 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 fd5e334ed..bcab39183 100644
--- 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 d095d98d3..c7a730b14 100644
--- 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 */
 
-- 
cgit v1.2.3