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.h | |
parent | 75d70649e2d72d6d6bb46f47cf96ee523b718cb9 (diff) |
Clean smt2 parsing of named attributes (#3172)
Diffstat (limited to 'src/parser/smt2/smt2.h')
-rw-r--r-- | src/parser/smt2/smt2.h | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 3afbcd61a..669104954 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -425,6 +425,17 @@ class Smt2 : public Parser } } } + /** Set named attribute + * + * This is called when expression expr is annotated with a name, i.e. + * (! expr :named sexpr). It sets up the necessary information to process + * this naming, including marking that expr is the last named term. + * + * We construct an expression symbol whose name is the name of s-expression + * which is used later for tracking assertions in unsat cores. This + * symbol is returned by this method. + */ + Expr setNamedAttribute(Expr& expr, const SExpr& sexpr); // Throw a ParserException with msg appended with the current logic. inline void parseErrorLogic(const std::string& msg) |