diff options
Diffstat (limited to 'src/parser/smt2/smt2.cpp')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index be0306a9e..d1fb3fe32 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -1566,5 +1566,29 @@ InputLanguage Smt2::getLanguage() const return em->getOptions().getInputLanguage(); } +Expr Smt2::setNamedAttribute(Expr& expr, const SExpr& sexpr) +{ + if (!sexpr.isKeyword()) + { + parseError("improperly formed :named annotation"); + } + std::string name = sexpr.getValue(); + checkUserSymbol(name); + // ensure expr is a closed subterm + if (expr.hasFreeVariable()) + { + std::stringstream ss; + ss << ":named annotations can only name terms that are closed"; + parseError(ss.str()); + } + // check that sexpr is a fresh function symbol, and reserve it + reserveSymbolAtAssertionLevel(name); + // define it + Expr func = mkVar(name, expr.getType()); + // remember the last term to have been given a :named attribute + setLastNamedTerm(expr, name); + return func; +} + } // namespace parser }/* CVC4 namespace */ |