Merge pull request #277 from zhangwen0411/smtlib-parse-named

SMTLIB2 parser: record formula label on ParserResult
vprover · Oct 18, 2021 · b6b253a · b6b253a
2 parents bc65d54 + 0e1d96b
commit b6b253a
Show file tree

Hide file tree

Showing 2 changed files with 28 additions and 9 deletions.
diff --git a/Parse/SMTLIB2.cpp b/Parse/SMTLIB2.cpp
@@ -1197,7 +1197,8 @@ bool SMTLIB2::ParseResult::asFormula(Formula*& resFrm)
 
   if (formula) {
     ASS_EQ(sort, AtomicSort::boolSort());
-    resFrm = frm;
+    resFrm = attachLabelToFormula(frm);
+
 
     LOG2("asFormula formula ",resFrm->toString());
     return true;
@@ -1208,7 +1209,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
 
@@ -1220,7 +1221,7 @@ bool SMTLIB2::ParseResult::asFormula(Formula*& resFrm)
 
     LOG2("asFormula wrap ",trm.toString());
 
-    resFrm = new BoolTermFormula(trm);
+    resFrm = attachLabelToFormula(new BoolTermFormula(trm));
     return true;
   }
 
@@ -1263,6 +1264,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");
@@ -2643,13 +2652,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);
-        //cout << "Label " << label << " : " << f << endl;
-        _results.push(ParseResult(f)); 
+        res.setLabel(label);
+        _results.push(res);
         continue;
       }
       case PO_LET_PREPARE_LOOKUP:

diff --git 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();
   };