Fix constructor type printing (#3246)

3 files changed, 118 insertions, 87 deletions

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index bd2d053e5..e9e8f2ea0 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -270,7 +270,7 @@ void Smt2Printer::toStream(std::ostream& out,
       }
       break;
     }
-
+    
     case kind::UNINTERPRETED_CONSTANT: {
       const UninterpretedConstant& uc = n.getConst<UninterpretedConstant>();
       std::stringstream ss;
@@ -473,12 +473,14 @@ void Smt2Printer::toStream(std::ostream& out,
   bool parametricTypeChildren = false;   // parametric operators that are (op t1 ... tn) where t1...tn must have same type
   bool typeChildren = false;  // operators (op t1...tn) where at least one of t1...tn may require a type cast e.g. Int -> Real
   // operator
+  Kind k = n.getKind();
   if(n.getNumChildren() != 0 &&
-     n.getKind() != kind::INST_PATTERN_LIST &&
-     n.getKind() != kind::APPLY_TYPE_ASCRIPTION) {
+     k != kind::INST_PATTERN_LIST &&
+     k != kind::APPLY_TYPE_ASCRIPTION &&
+     k != kind::CONSTRUCTOR_TYPE) {
     out << '(';
   }
-  switch(Kind k = n.getKind()) {
+  switch(k) {
     // builtin theory
   case kind::EQUAL:
   case kind::DISTINCT:
@@ -781,102 +783,110 @@ void Smt2Printer::toStream(std::ostream& out,
     stillNeedToPrintParams = false;
     break;
 
-    case kind::APPLY_CONSTRUCTOR:
+  case kind::APPLY_CONSTRUCTOR:
+  {
+    typeChildren = true;
+    const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
+    if (dt.isTuple())
     {
-      typeChildren = true;
-      const Datatype& dt = Datatype::datatypeOf(n.getOperator().toExpr());
-      if (dt.isTuple())
-      {
-        stillNeedToPrintParams = false;
-        out << "mkTuple" << ( dt[0].getNumArgs()==0 ? "" : " ");
-      }
+      stillNeedToPrintParams = false;
+      out << "mkTuple" << ( dt[0].getNumArgs()==0 ? "" : " ");
     }
+    break;
+  }
+  case kind::CONSTRUCTOR_TYPE:
+  {
+    out << n[n.getNumChildren()-1];
+    return;
+    break;
+  }
+  case kind::APPLY_TESTER:
+  case kind::APPLY_SELECTOR:
+  case kind::APPLY_SELECTOR_TOTAL:
+  case kind::PARAMETRIC_DATATYPE: break;
+
+  // separation logic
+  case kind::SEP_EMP:
+  case kind::SEP_PTO:
+  case kind::SEP_STAR:
+  case kind::SEP_WAND: out << smtKindString(k, d_variant) << " "; break;
+
+  case kind::SEP_NIL:
+    out << "(as sep.nil " << n.getType() << ")";
+    break;
 
-    case kind::APPLY_TESTER:
-    case kind::APPLY_SELECTOR:
-    case kind::APPLY_SELECTOR_TOTAL:
-    case kind::PARAMETRIC_DATATYPE: break;
-
-    // separation logic
-    case kind::SEP_EMP:
-    case kind::SEP_PTO:
-    case kind::SEP_STAR:
-    case kind::SEP_WAND: out << smtKindString(k, d_variant) << " "; break;
-
-    case kind::SEP_NIL:
-      out << "(as sep.nil " << n.getType() << ")";
-      break;
-
-      // quantifiers
-    case kind::FORALL:
-    case kind::EXISTS:
-      if (k == kind::FORALL)
-      {
-        out << "forall ";
-      }
-      else
-      {
-        out << "exists ";
-      }
-      for (unsigned i = 0; i < 2; i++)
-      {
-        out << n[i] << " ";
-        if (i == 0 && n.getNumChildren() == 3)
-        {
-          out << "(! ";
-        }
-      }
-      if (n.getNumChildren() == 3)
+    // quantifiers
+  case kind::FORALL:
+  case kind::EXISTS:
+  {
+    if (k == kind::FORALL)
+    {
+      out << "forall ";
+    }
+    else
+    {
+      out << "exists ";
+    }
+    for (unsigned i = 0; i < 2; i++)
+    {
+      out << n[i] << " ";
+      if (i == 0 && n.getNumChildren() == 3)
       {
-        out << n[2];
-        out << ")";
+        out << "(! ";
       }
+    }
+    if (n.getNumChildren() == 3)
+    {
+      out << n[2];
       out << ")";
-      return;
-      break;
-    case kind::BOUND_VAR_LIST:
-      // the left parenthesis is already printed (before the switch)
-      for (TNode::iterator i = n.begin(), iend = n.end(); i != iend;)
+    }
+    out << ")";
+    return;
+    break;
+  }
+  case kind::BOUND_VAR_LIST:
+  {
+    // the left parenthesis is already printed (before the switch)
+    for (TNode::iterator i = n.begin(), iend = n.end(); i != iend;)
+    {
+      out << '(';
+      toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, types, 0);
+      out << ' ';
+      out << (*i).getType();
+      out << ')';
+      if (++i != iend)
       {
-        out << '(';
-        toStream(out, *i, toDepth < 0 ? toDepth : toDepth - 1, types, 0);
         out << ' ';
-        out << (*i).getType();
-        // The following code do stange things
-        // (*i).getType().toStream(out, toDepth < 0 ? toDepth : toDepth - 1,
-        //                         false, language::output::LANG_SMTLIB_V2_5);
-        out << ')';
-        if (++i != iend)
-        {
-          out << ' ';
-        }
       }
-      out << ')';
-      return;
-    case kind::INST_PATTERN: break;
-    case kind::INST_PATTERN_LIST:
-      for (unsigned i = 0; i < n.getNumChildren(); i++)
+    }
+    out << ')';
+    return;
+  }
+  case kind::INST_PATTERN: break;
+  case kind::INST_PATTERN_LIST:
+  {
+    for (const Node& nc : n)
+    {
+      if (nc.getKind() == kind::INST_ATTRIBUTE)
       {
-        if (n[i].getKind() == kind::INST_ATTRIBUTE)
-        {
-          if (n[i][0].getAttribute(theory::FunDefAttribute()))
-          {
-            out << ":fun-def";
-          }
-        }
-        else
+        if (nc[0].getAttribute(theory::FunDefAttribute()))
         {
-          out << ":pattern " << n[i];
+          out << ":fun-def";
         }
       }
-      return;
-      break;
-
-    default:
-      // fall back on however the kind prints itself; this probably
-      // won't be SMT-LIB v2 compliant, but it will be clear from the
-      // output that support for the kind needs to be added here.
-      out << n.getKind() << ' ';
+      else
+      {
+        out << ":pattern " << nc;
+      }
+    }
+    return;
+    break;
+  }
+  default:
+    // fall back on however the kind prints itself; this probably
+    // won't be SMT-LIB v2 compliant, but it will be clear from the
+    // output that support for the kind needs to be added here.
+    out << n.getKind() << ' ';
   }
   if( n.getMetaKind() == kind::metakind::PARAMETERIZED &&
       stillNeedToPrintParams ) {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 5b44128fc..56010858d 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -360,6 +360,7 @@ set(regress_0_tests
   regress0/datatypes/dt-2.6.smt2
   regress0/datatypes/dt-match-pat-param-2.6.smt2
   regress0/datatypes/dt-param-2.6.smt2
+  regress0/datatypes/dt-param-2.6-print.smt2
   regress0/datatypes/dt-param-card4-bool-sat.smt2
   regress0/datatypes/dt-sel-2.6.smt2
   regress0/datatypes/empty_tuprec.cvc
diff --git a/test/regress/regress0/datatypes/dt-param-2.6-print.smt2 b/test/regress/regress0/datatypes/dt-param-2.6-print.smt2
new file mode 100644
index 000000000..165de0dba
--- /dev/null
+++ b/test/regress/regress0/datatypes/dt-param-2.6-print.smt2
@@ -0,0 +1,20 @@
+; EXPECT: sat
+; EXPECT: (model
+; EXPECT: (declare-datatypes ((Pair 2)) ((par (X Y)((mkPair (first X) (second Y))))))
+; EXPECT: (define-fun x () (Pair Int Real) ((as mkPair (Pair Int Real)) 2 (/ 3 2)))
+; EXPECT: )
+
+(set-logic ALL)
+(set-option :produce-models true)
+(set-info :status sat)
+(declare-datatypes ( (Pair 2) ) (
+(par ( X Y ) ( (mkPair (first X) (second Y))))
+))
+
+
+(declare-fun x () (Pair Int Real))
+
+(assert (= x (mkPair 2 1.5)))
+
+(check-sat)
+(get-model)