Fixes related to printing tuples, define-fun commands in smt2 (#6679)

This PR fixes some initial issues with printing datatypes in smt2.

It does not yet address further issues on printing define-fun as a result of dump=raw-benchmark, which requires deeper refactoring of the implementation of the API / SmtEngine.

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 04a57e0e9330be88bb56acc5ee7ab2d3b9dd239d..1f64bd23db9de9534c443e0fca0007c79db87e59 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -951,10 +951,43 @@ void Smt2Printer::toStream(std::ostream& out,
     return;
     break;
   }
-  case kind::APPLY_TESTER:
   case kind::APPLY_SELECTOR:
-  case kind::APPLY_SELECTOR_TOTAL:
+  {
+    Node op = n.getOperator();
+    const DType& dt = DType::datatypeOf(op);
+    if (dt.isTuple())
+    {
+      stillNeedToPrintParams = false;
+      out << "(_ tupSel " << DType::indexOf(op) << ") ";
+    }
+  }
+  break;
+  case kind::APPLY_TESTER:
+  {
+    stillNeedToPrintParams = false;
+    Node op = n.getOperator();
+    size_t cindex = DType::indexOf(op);
+    const DType& dt = DType::datatypeOf(op);
+    out << "(_ is ";
+    toStream(
+        out, dt[cindex].getConstructor(), toDepth < 0 ? toDepth : toDepth - 1);
+    out << ") ";
+  }
+  break;
   case kind::APPLY_UPDATER:
+  {
+    Node op = n.getOperator();
+    size_t index = DType::indexOf(op);
+    const DType& dt = DType::datatypeOf(op);
+    size_t cindex = DType::cindexOf(op);
+    out << "(_ update ";
+    toStream(out,
+             dt[cindex][index].getSelector(),
+             toDepth < 0 ? toDepth : toDepth - 1);
+    out << ") ";
+  }
+  break;
+  case kind::APPLY_SELECTOR_TOTAL:
   case kind::PARAMETRIC_DATATYPE: break;
 
   // separation logic
@@ -1037,19 +1070,8 @@ void Smt2Printer::toStream(std::ostream& out,
   if( n.getMetaKind() == kind::metakind::PARAMETERIZED &&
       stillNeedToPrintParams ) {
     if(toDepth != 0) {
-      if (n.getKind() == kind::APPLY_TESTER)
-      {
-        unsigned cindex = DType::indexOf(n.getOperator());
-        const DType& dt = DType::datatypeOf(n.getOperator());
-        out << "(_ is ";
-        toStream(out,
-                 dt[cindex].getConstructor(),
-                 toDepth < 0 ? toDepth : toDepth - 1);
-        out << ")";
-      }else{
-        toStream(
-            out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, lbind);
-      }
+      toStream(
+          out, n.getOperator(), toDepth < 0 ? toDepth : toDepth - 1, lbind);
     } else {
       out << "(...)";
     }

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 0aebee7b3f8d9dd97d07ef884a0e3ad939a1c990..d672b79a6a0bc544a73d3c997e194d2c4fe9ca13 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1404,11 +1404,16 @@ void DefineFunctionCommand::toStream(std::ostream& out,
                                      size_t dag,
                                      OutputLanguage language) const
 {
+  TypeNode rangeType = termToNode(d_func).getType();
+  if (rangeType.isFunction())
+  {
+    rangeType = rangeType.getRangeType();
+  }
   Printer::getPrinter(language)->toStreamCmdDefineFunction(
       out,
       d_func.toString(),
       termVectorToNodes(d_formals),
-      termToNode(d_func).getType().getRangeType(),
+      rangeType,
       termToNode(d_formula));
 }