From: Christopher L. Conway <christopherleeconway@gmail.com>
Date: Wed, 12 May 2010 20:29:17 +0000 (+0000)
Subject: true and false are only defined if the core theory is loaded in SMT v2 strict mode
X-Git-Tag: cvc5-1.0.0~9064
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8d691eac8e478576ebceb6406a8e372db5e3f7f1;p=cvc5.git

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 11e3ed604..fc03a2903 100644
--- 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 4e075e5dd..27337c35f 100644
--- 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 b277f6428..114880bb0 100644
--- 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 a1d6398f0..286867e84 100644
--- 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 d87a97ec4..c191d9f39 100644
--- 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 94a9aa30b..dec052859 100644
--- 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 4d3062d81..9fd6588bb 100644
--- 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 bcefe166b..6d7a04800 100644
--- 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 ad32edcbc..c003a76ec 100644
--- 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 e7df27083..49ff24863 100644
--- 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() {