Clean smt2 parsing of named attributes (#3172)

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)