Adding --no-checking option to disable semantic checks in parser

9 files changed, 89 insertions, 34 deletions

diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp
index ff9957c5c..8ace8e778 100644
--- a/src/main/getopt.cpp
+++ b/src/main/getopt.cpp
@@ -58,7 +58,8 @@ enum OptionValue {
   SMTCOMP,
   STATS,
   SEGV_NOSPIN,
-  PARSE_ONLY
+  PARSE_ONLY,
+  NO_CHECKING
 };/* enum OptionValue */
 
 // FIXME add a comment here describing the option array
@@ -74,7 +75,8 @@ static struct option cmdlineOptions[] = {
   { "smtcomp"    , no_argument      , NULL, SMTCOMP     },
   { "stats"      , no_argument      , NULL, STATS       },
   { "segv-nospin", no_argument      , NULL, SEGV_NOSPIN },
-  { "parse-only" , no_argument      , NULL, PARSE_ONLY  }
+  { "parse-only" , no_argument      , NULL, PARSE_ONLY  },
+  { "no-checking", no_argument      , NULL, NO_CHECKING }
 };/* if you add things to the above, please remember to update usage.h! */
 
 /** Full argv[0] */
@@ -176,6 +178,10 @@ throw(OptionException) {
       opts->parseOnly = true;
       break;
 
+    case NO_CHECKING:
+      opts->semanticChecks = false;
+      break;
+
     case '?':
       throw OptionException(string("can't understand option"));// + argv[optind - 1] + "'");
 
diff --git a/src/main/main.cpp b/src/main/main.cpp
index d0ad72fc4..e54bbb5f6 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -111,6 +111,10 @@ int main(int argc, char *argv[]) {
       parser = Parser::getNewParser(&exprMgr, options.lang, argv[firstArgIndex]);
     }
 
+    if(!options.semanticChecks) {
+      parser->disableChecks();
+    }
+
     // Parse and execute commands until we are done
     Command* cmd;
     while((cmd = parser->parseNextCommand())) {
diff --git a/src/parser/antlr_parser.cpp b/src/parser/antlr_parser.cpp
index af3ce9d1b..49a2f7362 100644
--- a/src/parser/antlr_parser.cpp
+++ b/src/parser/antlr_parser.cpp
@@ -37,19 +37,20 @@ namespace CVC4 {
 namespace parser {
 
 AntlrParser::AntlrParser(const antlr::ParserSharedInputState& state, int k) :
-  antlr::LLkParser(state, k) {
+  antlr::LLkParser(state, k), d_checksEnabled(true) {
 }
 
 AntlrParser::AntlrParser(antlr::TokenBuffer& tokenBuf, int k) :
-  antlr::LLkParser(tokenBuf, k) {
+  antlr::LLkParser(tokenBuf, k), d_checksEnabled(true) {
 }
 
 AntlrParser::AntlrParser(antlr::TokenStream& lexer, int k) :
-  antlr::LLkParser(lexer, k) {
+  antlr::LLkParser(lexer, k), d_checksEnabled(true) {
 }
 
 Expr AntlrParser::getSymbol(std::string name, SymbolType type) {
   Assert( isDeclared(name,type) );
+
   switch( type ) {
   case SYM_VARIABLE: // Functions share var namespace
   case SYM_FUNCTION:
@@ -295,41 +296,48 @@ void AntlrParser::parseError(string message)
                                  LT(1).get()->getColumn());
 }
 
-bool AntlrParser::checkDeclaration(string varName, 
+void AntlrParser::checkDeclaration(string varName,
                                    DeclarationCheck check,
                                    SymbolType type)
     throw (antlr::SemanticException) {
+  if(!d_checksEnabled) {
+    return;
+  }
+
   switch(check) {
   case CHECK_DECLARED:
     if( !isDeclared(varName, type) ) {
       parseError("Symbol " + varName + " not declared");
-    } else {
-      return true;
     }
+    break;
+
   case CHECK_UNDECLARED:
     if( isDeclared(varName, type) ) {
       parseError("Symbol " + varName + " previously declared");
-    } else {
-      return true;
     }
+    break;
+
   case CHECK_NONE:
-    return true;
+    break;
+
   default:
     Unhandled("Unknown check type!");
   }
 }
 
-bool AntlrParser::checkFunction(string name)   
+void AntlrParser::checkFunction(string name)
   throw (antlr::SemanticException) {
-  if( !isFunction(name) ) {
+  if( d_checksEnabled && !isFunction(name) ) {
     parseError("Expecting function symbol, found '" + name + "'");
   } 
-
-  return true;
 }
 
-bool AntlrParser::checkArity(Kind kind, unsigned int numArgs)
+void AntlrParser::checkArity(Kind kind, unsigned int numArgs)
   throw (antlr::SemanticException) {
+  if(!d_checksEnabled) {
+    return;
+  }
+
   unsigned int min = minArity(kind);
   unsigned int max = maxArity(kind);
 
@@ -345,8 +353,16 @@ bool AntlrParser::checkArity(Kind kind, unsigned int numArgs)
     ss << "found " << numArgs;
     parseError(ss.str());
   }
-  return true;
 }
 
+void AntlrParser::enableChecks() {
+  d_checksEnabled = true;
+}
+
+void AntlrParser::disableChecks() {
+  d_checksEnabled = false;
+}
+
+
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/antlr_parser.h b/src/parser/antlr_parser.h
index 52b4b4490..5c3f2f1f1 100644
--- a/src/parser/antlr_parser.h
+++ b/src/parser/antlr_parser.h
@@ -74,6 +74,12 @@ public:
    */
   virtual Expr parseExpr() = 0;
 
+  /** Enable semantic checks during parsing. */
+  void enableChecks();
+
+  /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */
+  void disableChecks();
+
 protected:
 
   /**
@@ -140,39 +146,38 @@ protected:
    * Checks if a symbol has been declared.
    * @param name the symbol name
    * @param type the symbol type
+   * @return true iff the symbol has been declared with the given type
    */
   bool isDeclared(std::string name, SymbolType type = SYM_VARIABLE);
 
   /**
-   * Return true if the the declaration policy we want to enforce holds
+   * Checks if the declaration policy we want to enforce holds
    * for the given symbol.
    * @param name the symbol to check
    * @param check the kind of check to perform
    * @param type the type of the symbol
-   * @return true if the check holds
-   * @throws SemanticException if the check fails
+   * @throws SemanticException if checks are enabled and the check fails
    */
-  bool checkDeclaration(std::string name, 
+  void checkDeclaration(std::string name,
                         DeclarationCheck check,
                         SymbolType type = SYM_VARIABLE)
     throw (antlr::SemanticException);
 
   /**
-   * Returns true if the given name is bound to a function.
+   * Checks whether the given name is bound to a function.
    * @param name the name to check
-   * @return true if name is bound to a function
-   * @throws SemanticException if name is not bound to a function
+   * @throws SemanticException if checks are enabled and name is not bound to a function
    */
-  bool checkFunction(std::string name) throw (antlr::SemanticException);
+  void checkFunction(std::string name) throw (antlr::SemanticException);
 
   /**
    * Check that <code>kind</code> can accept <code>numArgs</codes> arguments.
    * @param kind the built-in operator to check
    * @param numArgs the number of actual arguments
-   * @throws SemanticException if the operator <code>kind</code> cannot be
+   * @throws SemanticException if checks are enabled and the operator <code>kind</code> cannot be
    * applied to <code>numArgs</code> arguments.
    */
-  bool checkArity(Kind kind, unsigned int numArgs) throw (antlr::SemanticException);
+  void checkArity(Kind kind, unsigned int numArgs) throw (antlr::SemanticException);
 
   /** 
    * Returns the type for the variable with the given name. 
@@ -317,6 +322,8 @@ protected:
     }
   }
 
+//  bool checksEnabled();
+
 private:
 
   /** The expression manager */
@@ -332,6 +339,9 @@ private:
   /** The sort table */
   SymbolTable<const Type*> d_sortTable;
 
+  /** Are semantic checks enabled during parsing? */
+  bool d_checksEnabled;
+
   /** Lookup a symbol in the given namespace. */
   Expr getSymbol(std::string var_name, SymbolType type);
 };
diff --git a/src/parser/cvc/cvc_parser.g b/src/parser/cvc/cvc_parser.g
index e953244df..0cdf9f36b 100644
--- a/src/parser/cvc/cvc_parser.g
+++ b/src/parser/cvc/cvc_parser.g
@@ -154,7 +154,7 @@ identifier[DeclarationCheck check = CHECK_NONE,
 returns [std::string id]
   : x:IDENTIFIER
     { id = x->getText(); 
-      AlwaysAssert( checkDeclaration(id, check, type) ); }
+      checkDeclaration(id, check, type); }
   ;
 
 /**
@@ -381,6 +381,6 @@ functionSymbol[DeclarationCheck check = CHECK_NONE] returns [CVC4::Expr f]
   std::string name;
 }  
   : name = identifier[check,SYM_FUNCTION]
-    { AlwaysAssert( checkFunction(name) );  
+    { checkFunction(name);  
       f = getFunction(name); }
   ;
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index ef23d3883..b9e2d576e 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -132,5 +132,14 @@ Parser* Parser::getNewParser(ExprManager* em, InputLanguage lang,
   return getNewParser(em, lang, &input, "", false);
 }
 
+void Parser::disableChecks() {
+  d_antlrParser->disableChecks();
+}
+
+void Parser::enableChecks() {
+  d_antlrParser->enableChecks();
+}
+
+
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
diff --git a/src/parser/parser.h b/src/parser/parser.h
index bc4fd6018..170e1af31 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -84,6 +84,12 @@ public:
    */
   bool done() const;
 
+  /** Enable semantic checks during parsing. */
+  void enableChecks();
+
+  /** Disable semantic checks during parsing. Disabling checks may lead to crashes on bad inputs. */
+  void disableChecks();
+
 private:
 
   /**
diff --git a/src/parser/smt/smt_parser.g b/src/parser/smt/smt_parser.g
index a9f06d92c..39cadd47f 100644
--- a/src/parser/smt/smt_parser.g
+++ b/src/parser/smt/smt_parser.g
@@ -16,7 +16,6 @@
 header "post_include_hpp" {
 #include "parser/antlr_parser.h"
 #include "expr/command.h"
-#include "util/Assert.h"
 }
 
 header "post_include_cpp" {
@@ -123,7 +122,7 @@ annotatedFormula returns [CVC4::Expr formula]
 }
   : /* a built-in operator application */
     LPAREN kind = builtinOp annotatedFormulas[args] RPAREN 
-    { AlwaysAssert( checkArity(kind, args.size()) );
+    { checkArity(kind, args.size());
       formula = mkExpr(kind,args); }
 
   | /* A non-built-in function application */
@@ -213,7 +212,7 @@ functionSymbol returns [CVC4::Expr fun]
   string name;
 }
   : name = functionName[CHECK_DECLARED]
-    { AlwaysAssert( checkFunction(name) );
+    { checkFunction(name);
       fun = getFunction(name); }
   ;
   
@@ -316,6 +315,6 @@ returns [std::string id]
 }
   : x:IDENTIFIER
     { id = x->getText();
-      AlwaysAssert( checkDeclaration(id, check,type) ); }
+      checkDeclaration(id, check,type); }
   ;
 
diff --git a/src/util/options.h b/src/util/options.h
index 0a1766c09..cad00a61b 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -45,8 +45,12 @@ struct Options {
   /** The CNF conversion */
   CVC4::CnfConversion d_cnfConversion;
 
+  /** Should we exit after parsing? */
   bool parseOnly;
 
+  /** Should the parser do semantic checks? */
+  bool semanticChecks;
+
   Options() : binary_name(),
               smtcomp_mode(false),
               statistics(false),
@@ -55,7 +59,8 @@ struct Options {
               verbosity(0),
               lang(parser::Parser::LANG_AUTO),
               d_cnfConversion(CVC4::CNF_VAR_INTRODUCTION),
-              parseOnly(false)
+              parseOnly(false),
+              semanticChecks(true)
   {}
 };/* struct Options */