true and false are only defined if the core theory is loaded in SMT v2 strict mode

diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index 11e3ed60449226d7253687c5fd17121cde8767b4..fc03a2903bc8a9e09d893b81cc53c5d01d780c4f 100644 (file)
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -204,14 +204,13 @@ void AntlrInput::setAntlr3Lexer(pANTLR3_LEXER pLexer) {
   d_lexer->rec->state->tokSource->nextToken = &nextTokenStr;
 }
 
-void AntlrInput::setParser(Parser *parser) {
+void AntlrInput::setParser(Parser& parser) {
   // ANTLR isn't using super in the lexer or the parser, AFAICT.
   // We could also use @lexer/parser::context to add a field to the generated
   // objects, but then it would have to be declared separately in every
   // language's grammar and we'd have to in the address of the field anyway.
-  d_lexer->super = parser;
-  d_parser->super = parser;
-
+  d_lexer->super = &parser;
+  d_parser->super = &parser;
 }
 
 void AntlrInput::setAntlr3Parser(pANTLR3_PARSER pParser) {

diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 4e075e5ddecdbb6e2c8499a56565ccad93da96dd..27337c35f0399fdad09405bc33036c33aeb92531 100644 (file)
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -90,7 +90,7 @@ class Parser;
  * for the given input language and attach it to an input source of the
  * appropriate type.
  */
-class AntlrInput : public Input{
+class AntlrInput : public Input {
   /** The token lookahead used to lex and parse the input. This should usually be equal to
    * <code>K</code> for an LL(k) grammar. */
   unsigned int d_lookahead;
@@ -192,7 +192,7 @@ protected:
   void setAntlr3Parser(pANTLR3_PARSER pParser);
 
   /** Set the Parser object for this input. */
-  void setParser(Parser *parser);
+  virtual void setParser(Parser& parser);
 };
 
 inline std::string AntlrInput::tokenText(pANTLR3_COMMON_TOKEN token) {

diff --git a/src/parser/input.h b/src/parser/input.h
index b277f6428a10affc0dbce9d272e1c102e75e3ce6..114880bb00867df3ddc3990f2877fb3979301ce7 100644 (file)
--- a/src/parser/input.h
+++ b/src/parser/input.h
@@ -150,7 +150,7 @@ protected:
   virtual Expr parseExpr() throw(ParserException) = 0;
 
   /** Set the Parser object for this input. */
-  virtual void setParser(Parser *parser) = 0;
+  virtual void setParser(Parser& parser) = 0;
 };
 
 }/* CVC4::parser namespace */

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index a1d6398f0aca513d2d4755b5b5193819900e5b5e..286867e84ca220e977ec67a52f7bad8611f87dd5 100644 (file)
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -35,13 +35,13 @@ using namespace CVC4::kind;
 namespace CVC4 {
 namespace parser {
 
-Parser::Parser(ExprManager* exprManager, Input* input) :
+Parser::Parser(ExprManager* exprManager, Input* input, bool strictMode) :
   d_exprManager(exprManager),
   d_input(input),
   d_done(false),
   d_checksEnabled(true),
-  d_strictMode(false) {
-  d_input->setParser(this);
+  d_strictMode(strictMode) {
+  d_input->setParser(*this);
 }
 
 Expr Parser::getSymbol(const std::string& name, SymbolType type) {
@@ -111,14 +111,12 @@ Parser::mkVars(const std::vector<std::string> names,
 
 void
 Parser::defineVar(const std::string& name, const Expr& val) {
-  Assert(!isDeclared(name));
   d_declScope.bind(name,val);
   Assert(isDeclared(name));
 }
 
 void
 Parser::defineType(const std::string& name, const Type& type) {
-  Assert( !isDeclared(name, SYM_SORT) );
   d_declScope.bindType(name,type);
   Assert( isDeclared(name, SYM_SORT) ) ;
 }

diff --git a/src/parser/parser.h b/src/parser/parser.h
index d87a97ec46f391cd3198728ed9245677dc8d62d4..c191d9f39a88222bbb9448bd856704126992d7fe 100644 (file)
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -129,7 +129,7 @@ public:
    * @param exprManager the expression manager to use when creating expressions
    * @param input the parser input
    */
-  Parser(ExprManager* exprManager, Input* input);
+  Parser(ExprManager* exprManager, Input* input, bool strictMode = false);
 
   virtual ~Parser() { }
 

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 94a9aa30beb6e5a58eaa916b3fca1e494adf9337..dec0528596cc0ceb0d00a1b744362d6d653acb68 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -246,8 +246,8 @@ term[CVC4::Expr& expr]
     { expr = PARSER_STATE->getVariable(name); }
 
     /* constants */
-  | TRUE_TOK          { expr = MK_CONST(true); }
-  | FALSE_TOK         { expr = MK_CONST(false); }
+//  | TRUE_TOK          { expr = MK_CONST(true); }
+//  | FALSE_TOK         { expr = MK_CONST(false); }
   | INTEGER_LITERAL
     { expr = MK_CONST( AntlrInput::tokenToInteger($INTEGER_LITERAL) ); }
   | DECIMAL_LITERAL
@@ -376,7 +376,7 @@ CHECKSAT_TOK : 'check-sat';
 DECLARE_FUN_TOK : 'declare-fun';
 DECLARE_SORT_TOK : 'declare-sort';
 EXIT_TOK : 'exit';
-FALSE_TOK : 'false';
+//FALSE_TOK : 'false';
 ITE_TOK : 'ite';
 LET_TOK : 'let';
 LPAREN_TOK : '(';
@@ -388,7 +388,7 @@ SET_INFO_TOK : 'set-info';
 //SMT_VERSION_TOK : ':smt-lib-version';
 //SOURCE_TOK : ':source';
 //STATUS_TOK : ':status';
-TRUE_TOK : 'true';
+//TRUE_TOK : 'true';
 //UNKNOWN_TOK : 'unknown';
 //UNSAT_TOK : 'unsat';
 

diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 4d3062d8119b7a41d24ddfc4c5e419346171ca20..9fd6588bb22268a357322e109dabbcc77a531158 100644 (file)
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -60,6 +60,8 @@ void Smt2::addTheory(Parser& parser, Theory theory) {
   switch(theory) {
   case THEORY_CORE:
     parser.defineType("Bool", parser.getExprManager()->booleanType());
+    parser.defineVar("true", parser.getExprManager()->mkConst(true));
+    parser.defineVar("false", parser.getExprManager()->mkConst(false));
     parser.addOperator(kind::AND);
     parser.addOperator(kind::EQUAL);
     parser.addOperator(kind::IFF);

diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index bcefe166baec0a7d58e01c024a4524a0dc9f005b..6d7a04800ccc8e661a29b5377e0df4c3da2649e3 100644 (file)
--- a/src/parser/smt2/smt2_input.cpp
+++ b/src/parser/smt2/smt2_input.cpp
@@ -20,6 +20,7 @@
 #include "parser/input.h"
 #include "parser/parser.h"
 #include "parser/parser_exception.h"
+#include "parser/smt2/smt2.h"
 #include "parser/smt2/generated/Smt2Lexer.h"
 #include "parser/smt2/generated/Smt2Parser.h"
 
@@ -64,5 +65,12 @@ Expr Smt2Input::parseExpr() throw (ParserException) {
   return d_pSmt2Parser->parseExpr(d_pSmt2Parser);
 }
 
+void Smt2Input::setParser(Parser& parser) {
+  super::setParser(parser);
+  if( !parser.strictModeEnabled() ) {
+    Smt2::addTheory(parser,Smt2::THEORY_CORE);
+  }
+}
+
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */

diff --git a/src/parser/smt2/smt2_input.h b/src/parser/smt2/smt2_input.h
index ad32edcbc101865268a9cd6345fca15ada741959..c003a76ec356bfa85e64d954b7b1eb2320b7fd99 100644 (file)
--- a/src/parser/smt2/smt2_input.h
+++ b/src/parser/smt2/smt2_input.h
@@ -33,6 +33,7 @@ class ExprManager;
 namespace parser {
 
 class Smt2Input : public AntlrInput {
+  typedef AntlrInput super;
 
   /** The ANTLR3 SMT2 lexer for the input. */
   pSmt2Lexer d_pSmt2Lexer;
@@ -85,6 +86,11 @@ protected:
    */
   Expr parseExpr() throw(ParserException);
 
+  /** Set the Parser object for this input. This implementation overrides the super-class
+   * implementation to add the core theory symbols to the parser state when strict
+   * mode is disabled. */
+  virtual void setParser(Parser& parser);
+
 };/* class Smt2Input */
 
 }/* CVC4::parser namespace */

diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h
index e7df2708312ef0da6840489ba57ff11c286ac62f..49ff248635d63dbc5a703bdb03675e58cd185174 100644 (file)
--- a/test/unit/parser/parser_black.h
+++ b/test/unit/parser/parser_black.h
@@ -82,11 +82,11 @@ protected:
       }
   }
 
-  void tryBadInput(const string badInput) {
+  void tryBadInput(const string badInput, bool strictMode = false) {
 //      cerr << "Testing bad input: '" << badInput << "'\n";
 //      Debug.on("parser");
       Input* input = Input::newStringInput(d_lang, badInput, "test");
-      Parser parser(d_exprManager, input);
+      Parser parser(d_exprManager, input, strictMode);
       TS_ASSERT_THROWS
         ( while(parser.nextCommand());
           cout << "\nBad input succeeded:\n" << badInput << endl;,
@@ -134,10 +134,7 @@ protected:
 //    Debug.on("parser-extra");
 //      cout << "Testing bad expr: '" << badExpr << "'\n";
       Input* input = Input::newStringInput(d_lang, badExpr, "test");
-      Parser parser(d_exprManager, input);
-      if( strictMode ) {
-        parser.enableStrictMode();
-      }
+      Parser parser(d_exprManager, input, strictMode);
       setupContext(parser);
       TS_ASSERT( !parser.done() );
       TS_ASSERT_THROWS
@@ -278,10 +275,10 @@ public:
     tryGoodInput(""); // empty string is OK
     tryGoodInput("(set-logic QF_UF)");
     tryGoodInput("(set-info :notes |This is a note, take note!|)");
-    tryGoodInput("(set-logic QF_UF)(assert true)");
+    tryGoodInput("(set-logic QF_UF) (assert true)");
     tryGoodInput("(check-sat)");
     tryGoodInput("(exit)");
-    tryGoodInput("(assert false) (check-sat)");
+    tryGoodInput("(set-logic QF_UF) (assert false) (check-sat)");
     tryGoodInput("(set-logic QF_UF) (declare-fun a () Bool) "
                  "(declare-fun b () Bool)");
     tryGoodInput("(set-logic QF_UF) (declare-fun a () Bool) "
@@ -299,10 +296,13 @@ public:
   void testBadSmt2Inputs() {
     tryBadInput("(assert)"); // no args
     tryBadInput("(set-info :notes |Symbols can't contain the | character|)");
-    tryBadInput("(check-sat true)"); // shouldn't have an arg
+    tryBadInput("(set-logic QF_UF) (check-sat true)"); // shouldn't have an arg
     tryBadInput("(declare-sort a)"); // no arg
     tryBadInput("(declare-sort a 0) (declare-sort a 0)"); // double decl
-    tryBadInput("(declare-fun p Bool)"); // should be "p () Bool"
+    tryBadInput("(set-logic QF_UF) (declare-fun p Bool)"); // should be "p () Bool"
+    // strict mode
+    tryBadInput("(assert true)", true); // no set-logic, core theory symbol "true" undefined
+    tryBadInput("(declare-fun p Bool)", true); // core theory symbol "Bool" undefined
   }
 
   void testGoodSmt2Exprs() {