summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--library_versions2
-rw-r--r--src/compat/cvc3_compat.cpp8
-rw-r--r--src/parser/cvc/Cvc.g2
-rw-r--r--src/parser/parser.cpp7
-rw-r--r--src/parser/parser.h49
-rw-r--r--src/parser/smt2/Smt2.g24
6 files changed, 64 insertions, 28 deletions
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<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 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<std::string> d_reservedSymbols;
+
/** How many anonymous functions we've created. */
size_t d_anonymousFunctionCount;
@@ -288,6 +305,11 @@ public:
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
* @throws ParserException if checks are enabled and name is not
@@ -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.
@@ -533,13 +571,6 @@ public:
}
/**
- * 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<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 );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback