diff options
| -rw-r--r-- | NEWS | 5 | ||||
| -rw-r--r-- | THANKS | 3 | ||||
| -rw-r--r-- | library_versions | 1 | ||||
| -rw-r--r-- | src/compat/cvc3_compat.cpp | 8 | ||||
| -rw-r--r-- | src/parser/cvc/Cvc.g | 2 | ||||
| -rw-r--r-- | src/parser/parser.cpp | 7 | ||||
| -rw-r--r-- | src/parser/parser.h | 54 | ||||
| -rw-r--r-- | src/parser/smt2/Smt2.g | 78 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 54 | ||||
| -rw-r--r-- | src/smt/smt_engine.h | 6 |
10 files changed, 166 insertions, 52 deletions
@@ -3,7 +3,10 @@ This file contains a summary of important user-visible changes. Changes since 1.2 ================= -* nothing yet +* We no longer permit model or proof generation if there's been an + intervening push/pop. +* Increased compliance to SMT-LIBv2, numerous bugs and usability issues + resolved Changes since 1.1 ================= @@ -1,3 +1,6 @@ Thanks to Peter Collingbourne and his group (the Multicore Programming Group at Imperial College London) for developing and submitting some patches in September 2012 related to SMT-LIBv2 compliance. + +Thanks to David Cok of GrammaTech, Inc., for suggesting numerous improvements +in CVC4's SMT-LIBv2 compliance in May 2013. diff --git a/library_versions b/library_versions index 7174f7b0b..ad37ce67a 100644 --- a/library_versions +++ b/library_versions @@ -54,3 +54,4 @@ 1\.2\.1-prerelease libcvc4:1:1:1 libcvc4parser:1:1:0 libcvc4compat:1:0:0 libcvc4bindings:1:0:0 1\.3-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 d13fbf2d6..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 @@ -462,6 +484,11 @@ public: d_input->parseError(msg); } + /** Unexpectedly encountered an EOF */ + inline void unexpectedEOF(const std::string& msg) throw(ParserException) { + d_input->parseError(msg, true); + } + /** * If we are parsing only, don't raise an exception; if we are not, * raise a parse error with the given message. There is no actual @@ -482,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. @@ -528,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 7c0c1aad3..133cedfbd 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -133,6 +133,41 @@ using namespace CVC4::parser; #define MK_CONST EXPR_MANAGER->mkConst #define UNSUPPORTED PARSER_STATE->unimplementedFeature +static bool isClosed(Expr e, std::set<Expr>& free, std::hash_set<Expr, ExprHashFunction>& closedCache) { + if(closedCache.find(e) != closedCache.end()) { + return true; + } + + if(e.getKind() == kind::FORALL || e.getKind() == kind::EXISTS || e.getKind() == kind::LAMBDA) { + isClosed(e[1], free, closedCache); + for(Expr::const_iterator i = e[0].begin(); i != e[0].end(); ++i) { + free.erase((*i)[0]); + } + } else if(e.getKind() == kind::BOUND_VARIABLE) { + free.insert(e); + return false; + } else { + if(e.hasOperator()) { + isClosed(e.getOperator(), free, closedCache); + } + for(Expr::const_iterator i = e.begin(); i != e.end(); ++i) { + isClosed(*i, free, closedCache); + } + } + + if(free.empty()) { + closedCache.insert(e); + return true; + } else { + return false; + } +} + +static inline bool isClosed(Expr e, std::set<Expr>& free) { + std::hash_set<Expr, ExprHashFunction> cache; + return isClosed(e, free, cache); +} + }/* parser::postinclude */ /** @@ -216,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; @@ -262,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; @@ -392,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) ); } @@ -481,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; @@ -528,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; @@ -569,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; @@ -757,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; @@ -826,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 @@ -992,10 +1027,24 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] | ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr] { attr = std::string(":named"); + if(!sexpr.isKeyword()) { + PARSER_STATE->parseError("improperly formed :named annotation"); + } std::string name = sexpr.getValue(); - // FIXME ensure expr is a closed subterm - // check that sexpr is a fresh function symbol - PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_VARIABLE); + PARSER_STATE->checkUserSymbol(name); + // ensure expr is a closed subterm + std::set<Expr> freeVars; + if(!isClosed(expr, freeVars)) { + assert(!freeVars.empty()); + std::stringstream ss; + ss << ":named annotations can only name terms that are closed; this one contains free variables:"; + for(std::set<Expr>::const_iterator i = freeVars.begin(); i != freeVars.end(); ++i) { + ss << " " << *i; + } + PARSER_STATE->parseError(ss.str()); + } + // 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 @@ -1295,6 +1344,8 @@ symbol[std::string& id, PARSER_STATE->checkDeclaration(id, check, type); } } + | UNTERMINATED_QUOTED_SYMBOL EOF + { PARSER_STATE->unexpectedEOF("unterminated |quoted| symbol"); } ; /** @@ -1318,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 ); @@ -1488,6 +1539,9 @@ BVSGE_TOK : 'bvsge'; QUOTED_SYMBOL : '|' ~('|' | '\\')* '|' ; +UNTERMINATED_QUOTED_SYMBOL + : '|' ~('|' | '\\')* + ; /** * Matches a keyword from the input. A keyword is a simple symbol prefixed diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index ab4b13d4c..ca89ce36d 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -823,15 +823,6 @@ void SmtEngine::setLogicInternal() throw() { d_logic.lock(); - // may need to force uninterpreted functions to be on for non-linear - if(((d_logic.isTheoryEnabled(THEORY_ARITH) && !d_logic.isLinear()) || - d_logic.isTheoryEnabled(THEORY_BV)) && - !d_logic.isTheoryEnabled(THEORY_UF)){ - d_logic = d_logic.getUnlockedCopy(); - d_logic.enableTheory(THEORY_UF); - d_logic.lock(); - } - // Set the options for the theoryOf if(!options::theoryOfMode.wasSetByUser()) { if(d_logic.isSharingEnabled() && !d_logic.isTheoryEnabled(THEORY_BV)) { @@ -1322,6 +1313,11 @@ Node SmtEnginePrivate::expandBVDivByZero(TNode n) { Node divTotalNumDen = nm->mkNode(n.getKind() == kind::BITVECTOR_UDIV ? kind::BITVECTOR_UDIV_TOTAL : kind::BITVECTOR_UREM_TOTAL, num, den); Node node = nm->mkNode(kind::ITE, den_eq_0, divByZeroNum, divTotalNumDen); + if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) { + d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); + d_smt.d_logic.enableTheory(THEORY_UF); + d_smt.d_logic.lock(); + } return node; } @@ -1372,13 +1368,14 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF } case kind::DIVISION: { // partial function: division - if(d_smt.d_logic.isLinear()) { - node = n; - break; - } if(d_divByZero.isNull()) { d_divByZero = nm->mkSkolem("divByZero", nm->mkFunctionType(nm->realType(), nm->realType()), "partial real division", NodeManager::SKOLEM_EXACT_NAME); + if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) { + d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); + d_smt.d_logic.enableTheory(THEORY_UF); + d_smt.d_logic.lock(); + } } TNode num = n[0], den = n[1]; Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); @@ -1390,13 +1387,14 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF case kind::INTS_DIVISION: { // partial function: integer div - if(d_smt.d_logic.isLinear()) { - node = n; - break; - } if(d_intDivByZero.isNull()) { d_intDivByZero = nm->mkSkolem("intDivByZero", nm->mkFunctionType(nm->integerType(), nm->integerType()), "partial integer division", NodeManager::SKOLEM_EXACT_NAME); + if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) { + d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); + d_smt.d_logic.enableTheory(THEORY_UF); + d_smt.d_logic.lock(); + } } TNode num = n[0], den = n[1]; Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); @@ -1408,13 +1406,14 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF case kind::INTS_MODULUS: { // partial function: mod - if(d_smt.d_logic.isLinear()) { - node = n; - break; - } if(d_modZero.isNull()) { d_modZero = nm->mkSkolem("modZero", nm->mkFunctionType(nm->integerType(), nm->integerType()), "partial modulus", NodeManager::SKOLEM_EXACT_NAME); + if(!d_smt.d_logic.isTheoryEnabled(THEORY_UF)) { + d_smt.d_logic = d_smt.d_logic.getUnlockedCopy(); + d_smt.d_logic.enableTheory(THEORY_UF); + d_smt.d_logic.lock(); + } } TNode num = n[0], den = n[1]; Node den_eq_0 = nm->mkNode(kind::EQUAL, den, nm->mkConst(Rational(0))); @@ -3639,6 +3638,11 @@ void SmtEngine::push() throw(ModalException, LogicException) { d_needPostsolve = false; } + // The problem isn't really "extended" yet, but this disallows + // get-model after a push, simplifying our lives somewhat and + // staying symmtric with pop. + d_problemExtended = true; + d_userLevels.push_back(d_userContext->getLevel()); internalPush(); Trace("userpushpop") << "SmtEngine: pushed to level " @@ -3665,6 +3669,14 @@ void SmtEngine::pop() throw(ModalException) { d_needPostsolve = false; } + // The problem isn't really "extended" yet, but this disallows + // get-model after a pop, simplifying our lives somewhat. It might + // not be strictly necessary to do so, since the pops occur lazily, + // but also it would be weird to have a legally-executed (get-model) + // that only returns a subset of the assignment (because the rest + // is no longer in scope!). + d_problemExtended = true; + AlwaysAssert(d_userContext->getLevel() > 0); AlwaysAssert(d_userLevels.back() < d_userContext->getLevel()); while (d_userLevels.back() < d_userContext->getLevel()) { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 8266bb1ed..1b5af415f 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -189,9 +189,9 @@ class CVC4_PUBLIC SmtEngine { bool d_fullyInited; /** - * Whether or not we have added any assertions/declarations/definitions - * since the last checkSat/query (and therefore we're not responsible - * for an assignment). + * Whether or not we have added any assertions/declarations/definitions, + * or done push/pop, since the last checkSat/query, and therefore we're + * not responsible for models or proofs. */ bool d_problemExtended; |