From: Morgan Deters Date: Fri, 17 May 2013 22:14:18 +0000 (-0400) Subject: Detect multiply-defined :named annotations and issue an error. X-Git-Tag: cvc5-1.0.0~7287^2~33^2~14 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0e6d0a7bced1083db25a286b5ddfd79fba344639;p=cvc5.git 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 c74996e47..c686e8f46 100644 --- 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 0ecc6b5c7..601c251d9 100644 --- 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 778b85fce..cf21ca6eb 100644 --- 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 198d1cc31..1c275add7 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -357,7 +357,7 @@ Parser::mkMutualDatatypeTypes(const std::vector& 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 0761b4cda..4f943a0b5 100644 --- 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 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 29b6e0fbb..133cedfbd 100644 --- 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::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 >::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 >::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 >::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 >::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 >::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& 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 );