diff options
author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-06 21:11:43 +0000 |
---|---|---|
committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-05-06 21:11:43 +0000 |
commit | d292e8c233305c402da65a1cf97668881f7b099c (patch) | |
tree | 995ba2c65c61c0e3a7038d1eeae95c8b9efea599 /src/parser | |
parent | f4643b0e2f5ca233dcfeb91fbb424b8caec836e6 (diff) |
Adding --strict-parsing option
Diffstat (limited to 'src/parser')
-rw-r--r-- | src/parser/parser.cpp | 8 | ||||
-rw-r--r-- | src/parser/parser.h | 14 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 4 |
3 files changed, 15 insertions, 11 deletions
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] ); |