Detect multiply-defined :named annotations and issue an error.

Thanks to David Cok for pointing out this issue.

Conflicts:
	library_versions

diff --git a/library_versions b/library_versions
index c74996e473aa9815a122a15839aecc66c88a8813..c686e8f46c79755aac5ac9152f82f3cdd900c2b8 100644 (file)
--- a/library_versions
+++ b/library_versions
@@ -52,3 +52,5 @@
 1\.2-prerelease libcvc4:1:0:0 libcvc4parser:1:0:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0
 1\.2 libcvc4:1:1:1 libcvc4parser:1:1:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0
 1\.2\.1-prerelease libcvc4:1:1:1 libcvc4parser:1:1:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0
+# note: SmtEngine::setLogicString() exceptions have changed, bump library version on next release?
+# note: removed Parser::getDeclarationLevel(), added other interfaces

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 0ecc6b5c719eb9c082f05ca808aed73907516251..601c251d9d2dd765adf99c3e8a7ada44c375825e 100644 (file)
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -2273,7 +2273,7 @@ void ValidityChecker::popto(int stackLevel) {
 }
 
 int ValidityChecker::scopeLevel() {
-  return d_parserContext->getDeclarationLevel();
+  return d_parserContext->scopeLevel();
 }
 
 void ValidityChecker::pushScope() {
@@ -2287,12 +2287,12 @@ void ValidityChecker::popScope() {
 void ValidityChecker::poptoScope(int scopeLevel) {
   CVC4::CheckArgument(scopeLevel >= 0, scopeLevel,
                       "Cannot pop to a negative scope level %d", scopeLevel);
-  CVC4::CheckArgument(unsigned(scopeLevel) <= d_parserContext->getDeclarationLevel(),
+  CVC4::CheckArgument(unsigned(scopeLevel) <= d_parserContext->scopeLevel(),
                       scopeLevel,
                       "Cannot pop to a scope level higher than the current one!  "
                       "At scope level %u, user requested scope level %d",
-                      d_parserContext->getDeclarationLevel(), scopeLevel);
-  while(unsigned(scopeLevel) < d_parserContext->getDeclarationLevel()) {
+                      d_parserContext->scopeLevel(), scopeLevel);
+  while(unsigned(scopeLevel) < d_parserContext->scopeLevel()) {
     popScope();
   }
 }

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 778b85fce44e07676c10702092824e524604a1c1..cf21ca6eb1b76a61b4a38f7a9d42c1489a3be969 100644 (file)
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -1372,7 +1372,7 @@ letDecl
   : identifier[name,CHECK_NONE,SYM_VARIABLE] EQUAL_TOK formula[e]
     { Debug("parser") << Expr::setlanguage(language::output::LANG_CVC4) << e.getType() << std::endl;
       PARSER_STATE->defineVar(name, e);
-      Debug("parser") << "LET[" << PARSER_STATE->getDeclarationLevel() << "]: "
+      Debug("parser") << "LET[" << PARSER_STATE->scopeLevel() << "]: "
                       << name << std::endl
                       << " ==>" << " " << e << std::endl;
     }

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 198d1cc31233f9c2daf88731eb1ec6a44bffa12f..1c275add7c68b6a05ae931dfaeac390cf8c6c789 100644 (file)
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -357,7 +357,7 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
 bool Parser::isDeclared(const std::string& name, SymbolType type) {
   switch(type) {
   case SYM_VARIABLE:
-    return d_symtab->isBound(name);
+    return d_reservedSymbols.find(name) != d_reservedSymbols.end() || d_symtab->isBound(name);
   case SYM_SORT:
     return d_symtab->isBoundType(name);
   }
@@ -365,6 +365,11 @@ bool Parser::isDeclared(const std::string& name, SymbolType type) {
   return false;
 }
 
+void Parser::reserveSymbolAtAssertionLevel(const std::string& varName) {
+  checkDeclaration(varName, CHECK_UNDECLARED, SYM_VARIABLE);
+  d_reservedSymbols.insert(varName);
+}
+
 void Parser::checkDeclaration(const std::string& varName,
                               DeclarationCheck check,
                               SymbolType type)

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 0761b4cda30fe8bb5b1830a448c3baf7ba1448db..4f943a0b5e1aa434a894ba1b781e4dc3f7a429e5 100644 (file)
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -126,6 +126,23 @@ class CVC4_PUBLIC Parser {
    */
   SymbolTable* d_symtab;
 
+  /**
+   * The level of the assertions in the declaration scope.  Things declared
+   * after this level are bindings from e.g. a let, a quantifier, or a
+   * lambda.
+   */
+  size_t d_assertionLevel;
+
+  /**
+   * Maintains a list of reserved symbols at the assertion level that might
+   * not occur in our symbol table.  This is necessary to e.g. support the
+   * proper behavior of the :named annotation in SMT-LIBv2 when used under
+   * a let or a quantifier, since inside a let/quant body the declaration
+   * scope is that of the let/quant body, but the defined name should be
+   * reserved at the assertion level.
+   */
+  std::set<std::string> d_reservedSymbols;
+
   /** How many anonymous functions we've created. */
   size_t d_anonymousFunctionCount;
 
@@ -287,6 +304,11 @@ public:
   void checkDeclaration(const std::string& name, DeclarationCheck check,
                         SymbolType type = SYM_VARIABLE) throw(ParserException);
 
+  /**
+   * Reserve a symbol at the assertion level.
+   */
+  void reserveSymbolAtAssertionLevel(const std::string& name);
+
   /**
    * Checks whether the given name is bound to a function.
    * @param name the name to check
@@ -487,9 +509,25 @@ public:
     }
   }
 
+  /**
+   * Gets the current declaration level.
+   */
   inline size_t scopeLevel() const { return d_symtab->getLevel(); }
-  inline void pushScope() { d_symtab->pushScope(); }
-  inline void popScope() { d_symtab->popScope(); }
+
+  inline void pushScope(bool bindingLevel = false) {
+    d_symtab->pushScope();
+    if(!bindingLevel) {
+      d_assertionLevel = scopeLevel();
+    }
+  }
+
+  inline void popScope() {
+    d_symtab->popScope();
+    if(scopeLevel() < d_assertionLevel) {
+      d_assertionLevel = scopeLevel();
+      d_reservedSymbols.clear();
+    }
+  }
 
   /**
    * Set the current symbol table used by this parser.
@@ -532,13 +570,6 @@ public:
     return d_symtab;
   }
 
-  /**
-   * Gets the current declaration level.
-   */
-  inline size_t getDeclarationLevel() const throw() {
-    return d_symtab->getLevel();
-  }
-
   /**
    * An expression stream interface for a parser.  This stream simply
    * pulls expressions from the given Parser object.

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 29b6e0fbb7d68f62d5e1e5430575a25e8fb4f45a..133cedfbd84d7957c901d3e648f73415e53de192 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -251,7 +251,7 @@ command returns [CVC4::Command* cmd = NULL]
     symbol[name,CHECK_UNDECLARED,SYM_SORT]
     { PARSER_STATE->checkUserSymbol(name); }
     LPAREN_TOK symbolList[names,CHECK_NONE,SYM_SORT] RPAREN_TOK
-    { PARSER_STATE->pushScope();
+    { PARSER_STATE->pushScope(true);
       for(std::vector<std::string>::const_iterator i = names.begin(),
             iend = names.end();
           i != iend;
@@ -297,7 +297,7 @@ command returns [CVC4::Command* cmd = NULL]
         }
         t = EXPR_MANAGER->mkFunctionType(sorts, t);
       }
-      PARSER_STATE->pushScope();
+      PARSER_STATE->pushScope(true);
       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
             sortedVarNames.begin(), iend = sortedVarNames.end();
           i != iend;
@@ -427,7 +427,7 @@ extendedCommand[CVC4::Command*& cmd]
      * --smtlib2 compliance mode. */
   : DECLARE_DATATYPES_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     { /* open a scope to keep the UnresolvedTypes contained */
-      PARSER_STATE->pushScope(); }
+      PARSER_STATE->pushScope(true); }
     LPAREN_TOK         /* parametric sorts */
       ( symbol[name,CHECK_UNDECLARED,SYM_SORT] {
         sorts.push_back( PARSER_STATE->mkSort(name) ); }
@@ -516,7 +516,7 @@ extendedCommand[CVC4::Command*& cmd]
       sortedVarList[sortedVarNames] RPAREN_TOK
       { /* add variables to parser state before parsing term */
         Debug("parser") << "define fun: '" << name << "'" << std::endl;
-        PARSER_STATE->pushScope();
+        PARSER_STATE->pushScope(true);
         for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
               sortedVarNames.begin(), iend = sortedVarNames.end();
             i != iend;
@@ -563,7 +563,7 @@ rewriterulesCommand[CVC4::Command*& cmd]
     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
     {
       kind = CVC4::kind::RR_REWRITE;
-      PARSER_STATE->pushScope();
+      PARSER_STATE->pushScope(true);
       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
             sortedVarNames.begin(), iend = sortedVarNames.end();
           i != iend;
@@ -604,7 +604,7 @@ rewriterulesCommand[CVC4::Command*& cmd]
   | rewritePropaKind[kind]
     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
     {
-      PARSER_STATE->pushScope();
+      PARSER_STATE->pushScope(true);
       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
             sortedVarNames.begin(), iend = sortedVarNames.end();
           i != iend;
@@ -792,7 +792,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
   | LPAREN_TOK quantOp[kind]
     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
     {
-      PARSER_STATE->pushScope();
+      PARSER_STATE->pushScope(true);
       for(std::vector<std::pair<std::string, CVC4::Type> >::const_iterator i =
             sortedVarNames.begin(), iend = sortedVarNames.end();
           i != iend;
@@ -861,7 +861,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
 
   | /* a let binding */
     LPAREN_TOK LET_TOK LPAREN_TOK
-    { PARSER_STATE->pushScope(); }
+    { PARSER_STATE->pushScope(true); }
     ( LPAREN_TOK symbol[name,CHECK_NONE,SYM_VARIABLE] term[expr, f2] RPAREN_TOK
       // this is a parallel let, so we have to save up all the contributions
       // of the let and define them only later on
@@ -1043,10 +1043,8 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
         }
         PARSER_STATE->parseError(ss.str());
       }
-      // check that sexpr is a fresh function symbol
-      // FIXME: this doesn't work if we're in a forall/exists/let, because then the function
-      // we make is in the subscope, and disappears, and can be re-bound with another :named.  :-(
-      PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE);
+      // check that sexpr is a fresh function symbol, and reserve it
+      PARSER_STATE->reserveSymbolAtAssertionLevel(name);
       // define it
       Expr func = PARSER_STATE->mkFunction(name, expr.getType());
       // bind name to expr with define-fun
@@ -1371,7 +1369,7 @@ datatypeDef[std::vector<CVC4::Datatype>& datatypes, std::vector< CVC4::Type >& p
      * datatypes won't work, because this type will already be
      * "defined" as an unresolved type; don't worry, we check
      * below. */
-  : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(); }
+  : symbol[id,CHECK_NONE,SYM_SORT] { PARSER_STATE->pushScope(true); }
    /* ( '[' symbol[id2,CHECK_UNDECLARED,SYM_SORT] {
         t = PARSER_STATE->mkSort(id2);
         params.push_back( t );