From 7a9a63e183a9034b654a75cabc55964e78040435 Mon Sep 17 00:00:00 2001
From: Wen Zhang <zhangwen@cs.berkeley.edu>
Date: Tue, 28 Sep 2021 12:17:42 -0700
Subject: [PATCH] SMTLIB2 parser: record formula label on ParserResult

---
 Parse/SMTLIB2.cpp | 21 +++++++++++++--------
 Parse/SMTLIB2.hpp | 14 ++++++++++++++
 2 files changed, 27 insertions(+), 8 deletions(-)

diff --git a/Parse/SMTLIB2.cpp b/Parse/SMTLIB2.cpp
index 689e8a0bf8..d6089802ee 100644
--- a/Parse/SMTLIB2.cpp
+++ b/Parse/SMTLIB2.cpp
@@ -1208,7 +1208,7 @@ bool SMTLIB2::ParseResult::asFormula(Formula*& resFrm)
 
   if (formula) {
     ASS_EQ(sort, Term::boolSort());
-    resFrm = frm;
+    resFrm = attachLabelToFormula(frm);
 
     LOG2("asFormula formula ",resFrm->toString());
     return true;
@@ -1219,7 +1219,7 @@ bool SMTLIB2::ParseResult::asFormula(Formula*& resFrm)
     if (trm.isTerm()) {
       Term* t = trm.term();
       if (t->isFormula()) {
-        resFrm = t->getSpecialData()->getFormula();
+        resFrm = attachLabelToFormula(t->getSpecialData()->getFormula());
 
         // t->destroy(); -- we cannot -- it can be accessed more than once
 
@@ -1231,7 +1231,7 @@ bool SMTLIB2::ParseResult::asFormula(Formula*& resFrm)
 
     LOG2("asFormula wrap ",trm.toString());
 
-    resFrm = new BoolTermFormula(trm);
+    resFrm = attachLabelToFormula(new BoolTermFormula(trm));
     return true;
   }
 
@@ -1274,6 +1274,14 @@ vstring SMTLIB2::ParseResult::toString()
   return "term of sort "+sort.toString()+": "+trm.toString();
 }
 
+Formula* SMTLIB2::ParseResult::attachLabelToFormula(Formula* frm)
+{
+  if (!label.empty()) {
+    frm->label(label);
+  }
+  return frm;
+}
+
 Interpretation SMTLIB2::getFormulaSymbolInterpretation(FormulaSymbol fs, TermList firstArgSort)
 {
   CALL("SMTLIB2::getFormulaSymbolInterpretation");
@@ -2653,12 +2661,9 @@ SMTLIB2::ParseResult SMTLIB2::parseTermOrFormula(LExpr* body)
       case PO_LABEL: {
         ASS_GE(_results.size(),1);
         ParseResult res =  _results.pop();
-        ASS(res.formula);
-        Formula* f;
-        res.asFormula(f);
         vstring label = exp->toString();
-        f->label(label);
-        _results.push(res); 
+        res.setLabel(label);
+        _results.push(res);
         continue;
       }
       case PO_LET_PREPARE_LOOKUP:
diff --git a/Parse/SMTLIB2.hpp b/Parse/SMTLIB2.hpp
index 56a1fbd660..73ba79ae60 100644
--- a/Parse/SMTLIB2.hpp
+++ b/Parse/SMTLIB2.hpp
@@ -292,6 +292,9 @@ class SMTLIB2 {
 
     TermList sort;
     bool formula;
+    /** The label assigned to this formula using the ":named" annotation of SMT-LIB2;
+     * empty string means no label. */
+    vstring label;
     union {
       Formula* frm;
       TermList trm;
@@ -309,6 +312,17 @@ class SMTLIB2 {
      * and return its vampire sort (which may be Sorts::SRT_BOOL).
      */
     TermList asTerm(TermList& resTrm);
+    /**
+     * Records a label for the formula represented by this `ParserResult`,
+     * resulting from a ":named" SMT-LIB2 annotation.
+     */
+    void setLabel(vstring l){ label = l; }
+    /**
+     * Helper that attaches a label to a `Formula`
+     * if a label is recorded for this `ParserResult`.
+     * Returns the formula.
+     */
+    Formula* attachLabelToFormula(Formula* frm);
 
     vstring toString();
   };