Fix datatype declaration printing in LFSC printer (#8222)

diff --git a/src/proof/lfsc/lfsc_printer.cpp b/src/proof/lfsc/lfsc_printer.cpp
index 3018d3b6bf317bbeea1c9825e94d9bf155727560..329b9106fce8faaebf81a6da15e98171d41660b5 100644 (file)
--- a/src/proof/lfsc/lfsc_printer.cpp
+++ b/src/proof/lfsc/lfsc_printer.cpp
@@ -80,91 +80,43 @@ void LfscPrinter::print(std::ostream& out,
   {
     // note that we must get all "component types" of a type, so that
     // e.g. U is printed as a sort declaration when we have type (Array U Int).
-    std::unordered_set<TypeNode> ctypes;
-    expr::getComponentTypes(st, ctypes);
-    for (const TypeNode& stc : ctypes)
+    ensureTypeDefinitionPrinted(preamble, st, sts, tupleArity);
+  }
+  // print datatype definitions for the above sorts
+  for (const TypeNode& stc : sts)
+  {
+    if (!stc.isDatatype() || stc.getKind() == PARAMETRIC_DATATYPE)
     {
-      if (sts.find(stc) != sts.end())
-      {
-        continue;
-      }
-      sts.insert(stc);
-      if (stc.isSort())
+      // skip the instance of a parametric datatype
+      continue;
+    }
+    const DType& dt = stc.getDType();
+    preamble << "; DATATYPE " << dt.getName() << std::endl;
+    NodeManager* nm = NodeManager::currentNM();
+    for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
+    {
+      const DTypeConstructor& cons = dt[i];
+      std::string cname = d_tproc.getNameForUserNameOf(cons.getConstructor());
+      // for now, must print as node to ensure same policy for printing
+      // variable names. For instance, this means that cvc.X is printed as
+      // LFSC identifier |cvc.X| if X contains symbols legal in LFSC but not
+      // SMT-LIB. (cvc5-projects/issues/466) We should disable printing quote
+      // escapes in the smt2 printing of LFSC converted terms.
+      Node cc = nm->mkBoundVar(cname, stc);
+      // print constructor/tester
+      preamble << "(declare " << cc << " term)" << std::endl;
+      for (size_t j = 0, nargs = cons.getNumArgs(); j < nargs; j++)
       {
-        preamble << "(declare ";
-        printType(preamble, stc);
-        preamble << " sort)" << std::endl;
+        const DTypeSelector& arg = cons[j];
+        // print selector
+        std::string sname = d_tproc.getNameForUserNameOf(arg.getSelector());
+        Node sc = nm->mkBoundVar(sname, stc);
+        preamble << "(declare " << sc << " term)" << std::endl;
       }
-      else if (stc.isDatatype())
-      {
-        const DType& dt = stc.getDType();
-        if (stc.getKind() == PARAMETRIC_DATATYPE)
-        {
-          // skip the instance of a parametric datatype
-          continue;
-        }
-        preamble << "; DATATYPE " << dt.getName() << std::endl;
-        if (dt.isTuple())
-        {
-          const DTypeConstructor& cons = dt[0];
-          size_t arity = cons.getNumArgs();
-          if (tupleArity.find(arity) == tupleArity.end())
-          {
-            tupleArity.insert(arity);
-            preamble << "(declare Tuple_" << arity << " ";
-            std::stringstream tcparen;
-            for (size_t j = 0, nargs = cons.getNumArgs(); j < nargs; j++)
-            {
-              preamble << "(! s" << j << " sort ";
-              tcparen << ")";
-            }
-            preamble << "sort" << tcparen.str() << ")";
-          }
-          preamble << std::endl;
-        }
-        else
-        {
-          preamble << "(declare ";
-          printType(preamble, stc);
-          std::stringstream cdttparens;
-          if (dt.isParametric())
-          {
-            std::vector<TypeNode> params = dt.getParameters();
-            for (const TypeNode& tn : params)
-            {
-              preamble << " (! " << tn << " sort";
-              cdttparens << ")";
-            }
-          }
-          preamble << " sort)" << cdttparens.str() << std::endl;
-        }
-        for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
-        {
-          const DTypeConstructor& cons = dt[i];
-          std::stringstream sscons;
-          sscons << d_tproc.convert(cons.getConstructor());
-          std::string cname =
-              LfscNodeConverter::getNameForUserName(sscons.str());
-          // print construct/tester
-          preamble << "(declare " << cname << " term)" << std::endl;
-          for (size_t j = 0, nargs = cons.getNumArgs(); j < nargs; j++)
-          {
-            const DTypeSelector& arg = cons[j];
-            // print selector
-            Node si = d_tproc.convert(arg.getSelector());
-            std::stringstream sns;
-            sns << si;
-            std::string sname =
-                LfscNodeConverter::getNameForUserName(sns.str());
-            preamble << "(declare " << sname << " term)" << std::endl;
-          }
-        }
-        // testers and updaters are instances of parametric symbols
-        // shared selectors are instance of parametric symbol "sel"
-        preamble << "; END DATATYPE " << std::endl;
-      }
-      // all other sorts are builtin into the LFSC signature
     }
+    // testers and updaters are instances of parametric symbols
+    // shared selectors are instance of parametric symbol "sel"
+    preamble << "; END DATATYPE " << std::endl;
   }
   Trace("lfsc-print-debug") << "; print user symbols" << std::endl;
   // [1b] user declare function symbols
@@ -262,6 +214,92 @@ void LfscPrinter::print(std::ostream& out,
   out << cparen.str() << std::endl;
 }
 
+void LfscPrinter::ensureTypeDefinitionPrinted(
+    std::ostream& os,
+    TypeNode tn,
+    std::unordered_set<TypeNode>& processed,
+    std::unordered_set<size_t>& tupleArityProcessed)
+{
+  // note that we must get all "component types" of a type, so that
+  // e.g. U is printed as a sort declaration when we have type (Array U Int).
+  std::unordered_set<TypeNode> ctypes;
+  expr::getComponentTypes(tn, ctypes);
+
+  for (const TypeNode& stc : ctypes)
+  {
+    printTypeDefinition(os, stc, processed, tupleArityProcessed);
+  }
+}
+
+void LfscPrinter::printTypeDefinition(
+    std::ostream& os,
+    TypeNode tn,
+    std::unordered_set<TypeNode>& processed,
+    std::unordered_set<size_t>& tupleArityProcessed)
+{
+  if (processed.find(tn) != processed.end())
+  {
+    return;
+  }
+  processed.insert(tn);
+  if (tn.isSort())
+  {
+    os << "(declare ";
+    printType(os, tn);
+    os << " sort)" << std::endl;
+  }
+  else if (tn.isDatatype())
+  {
+    const DType& dt = tn.getDType();
+    if (tn.getKind() == PARAMETRIC_DATATYPE)
+    {
+      // skip the instance of a parametric datatype
+      return;
+    }
+    if (dt.isTuple())
+    {
+      const DTypeConstructor& cons = dt[0];
+      size_t arity = cons.getNumArgs();
+      if (tupleArityProcessed.find(arity) == tupleArityProcessed.end())
+      {
+        tupleArityProcessed.insert(arity);
+        os << "(declare Tuple_" << arity << " ";
+        std::stringstream tcparen;
+        for (size_t j = 0, nargs = cons.getNumArgs(); j < nargs; j++)
+        {
+          os << "(! s" << j << " sort ";
+          tcparen << ")";
+        }
+        os << "sort" << tcparen.str() << ")";
+      }
+      os << std::endl;
+    }
+    else
+    {
+      os << "(declare ";
+      printType(os, tn);
+      std::stringstream cdttparens;
+      if (dt.isParametric())
+      {
+        std::vector<TypeNode> params = dt.getParameters();
+        for (const TypeNode& p : params)
+        {
+          os << " (! " << p << " sort";
+          cdttparens << ")";
+        }
+      }
+      os << " sort)" << cdttparens.str() << std::endl;
+    }
+    // must also ensure the subfield types of the datatype are printed
+    std::unordered_set<TypeNode> sftypes = dt.getSubfieldTypes();
+    for (const TypeNode& sft : sftypes)
+    {
+      ensureTypeDefinitionPrinted(os, sft, processed, tupleArityProcessed);
+    }
+  }
+  // all other sorts are builtin into the LFSC signature
+}
+
 void LfscPrinter::printProofLetify(
     LfscPrintChannel* out,
     const ProofNode* pn,
@@ -426,10 +464,7 @@ void LfscPrinter::printProofInternal(
             Node res = d_tproc.convert(cur->getResult());
             res = lbind.convert(res, "__t", true);
             out->printTrust(res, r);
-            if (d_trustWarned.find(r) == d_trustWarned.end())
-            {
-              d_trustWarned.insert(r);
-            }
+            d_trustWarned.insert(r);
           }
         }
       }
@@ -576,8 +611,9 @@ bool LfscPrinter::computeProofArgs(const ProofNode* pn,
       Assert(res[1].getKind() == CONST_RATIONAL);
       pf << h << h << d_tproc.convert(res[1]) << cs[0];
     }
+    break;
     // strings
-    break;case PfRule::STRING_LENGTH_POS:
+    case PfRule::STRING_LENGTH_POS:
       pf << as[0] << d_tproc.convertType(as[0].getType()) << h;
       break;
     case PfRule::STRING_LENGTH_NON_EMPTY: pf << h << h << cs[0]; break;

diff --git a/src/proof/lfsc/lfsc_printer.h b/src/proof/lfsc/lfsc_printer.h
index fb58903940ed723331754797d6920bd56fa1656d..3a6e367643800756167034200a0c09829c232e51 100644 (file)
--- a/src/proof/lfsc/lfsc_printer.h
+++ b/src/proof/lfsc/lfsc_printer.h
@@ -64,6 +64,35 @@ class LfscPrinter
   void printType(std::ostream& out, TypeNode n);
 
  private:
+  /**
+   * This ensures that the type definition of type tn has been
+   * printed, which ensures that all of its component types, and the
+   * user-defined subfields of datatype types among those are declared. This
+   * furthermore includes running to a fixed point in the case that tn contains
+   * subfield types that are themselves datatypes.
+   * Notice that type definitions do not include printing the symbols of the
+   * datatype.
+   *
+   * @param os The stream to print to
+   * @param tn The type to ensure the definition(s) are printed for
+   * @param processed The types whose definitions we have already printed
+   * @param tupleArityProcessed The arity of tuples that we have declared.
+   * Note this is only required until we have a more robust treatment of
+   * tuples in the LFSC signature
+   */
+  void ensureTypeDefinitionPrinted(
+      std::ostream& os,
+      TypeNode tn,
+      std::unordered_set<TypeNode>& processed,
+      std::unordered_set<size_t>& tupleArityProcessed);
+  /**
+   * print type definition, which is the same as above, but does not process
+   * component types.
+   */
+  void printTypeDefinition(std::ostream& os,
+                           TypeNode tn,
+                           std::unordered_set<TypeNode>& processed,
+                           std::unordered_set<size_t>& tupleArityProcessed);
   /**
    * Print node to stream in the expected format of LFSC.
    */