diff options
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) |