diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-12 15:40:26 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-12 15:40:26 -0500 |
commit | eba03c5af0112aea04d83977333ae37e8a13137d (patch) | |
tree | eefef30537be62f6116a9e99a614049a93fa14b8 /src/parser/smt2/Smt2.g | |
parent | 75d70649e2d72d6d6bb46f47cf96ee523b718cb9 (diff) |
Clean smt2 parsing of named attributes (#3172)
Diffstat (limited to 'src/parser/smt2/Smt2.g')
-rw-r--r-- | src/parser/smt2/Smt2.g | 59 |
1 files changed, 1 insertions, 58 deletions
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index c672d8ff5..a5109361b 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -150,41 +150,6 @@ using namespace CVC4::parser; #define SOLVER PARSER_STATE->getSolver() #define UNSUPPORTED PARSER_STATE->unimplementedFeature -static bool isClosed(const Expr& e, std::set<Expr>& free, std::unordered_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); - } - } 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(const Expr& e, std::set<Expr>& free) { - std::unordered_set<Expr, ExprHashFunction> cache; - return isClosed(e, free, cache); -} - }/* parser::postinclude */ /** @@ -2842,30 +2807,8 @@ 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"); - } + Expr func = PARSER_STATE->setNamedAttribute(expr, sexpr); std::string name = sexpr.getValue(); - 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->mkVar(name, expr.getType()); - // remember the last term to have been given a :named attribute - PARSER_STATE->setLastNamedTerm(expr, name); // bind name to expr with define-fun Command* c = new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr); |