Partial fix for bug 435; still needs some effort.

(this commit was certified error- and warning-free by the test-and-commit script.)

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index a61d2d4c0bbd836853faf10aec1ffb4763e220f1..a9d439a0fb151f3aee4bae25b0aa46f13a184591 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -290,6 +290,17 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       break;
 
     // DATATYPES
+    case kind::PARAMETRIC_DATATYPE:
+      out << n[0].getConst<Datatype>().getName() << '[';
+      for(unsigned i = 1; i < n.getNumChildren(); ++i) {
+        if(i > 1) {
+          out << ',';
+        }
+        out << n[i];
+      }
+      out << ']';
+      return;
+      break;
     case kind::APPLY_TYPE_ASCRIPTION: {
         toStream(out, n[0], depth, types, false);
         out << "::";
@@ -462,9 +473,6 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       op << ">=";
       opType = INFIX;
       break;
-    case kind::PARAMETRIC_DATATYPE:
-      out << n[0].getConst<Datatype>().getName();
-      break;
 
     // BITVECTORS
     case kind::BITVECTOR_XOR:

diff --git a/src/theory/datatypes/kinds b/src/theory/datatypes/kinds
index d1fbf82bc641259eaaabe876a126a9916213dc0f..3968af4dd7a83a671a92541165f0c06833c2d521 100644 (file)
--- a/src/theory/datatypes/kinds
+++ b/src/theory/datatypes/kinds
@@ -63,11 +63,15 @@ operator PARAMETRIC_DATATYPE 1: "parametric datatype"
 cardinality PARAMETRIC_DATATYPE \
     "DatatypeType(%TYPE%.toType()).getDatatype().getCardinality()" \
     "util/datatype.h"
-well-founded PARAMETRIC_DATATYPE\
+well-founded PARAMETRIC_DATATYPE \
     "DatatypeType(%TYPE%.toType()).getDatatype().isWellFounded()" \
     "DatatypeType(%TYPE%.toType()).getDatatype().mkGroundTerm(%TYPE%.toType())" \
     "util/datatype.h"
 
+enumerator PARAMETRIC_DATATYPE \
+    "::CVC4::theory::datatypes::DatatypesEnumerator" \
+    "theory/datatypes/type_enumerator.h"
+
 parameterized APPLY_TYPE_ASCRIPTION ASCRIPTION_TYPE 1 \
     "type ascription, for datatype constructor applications"
 constant ASCRIPTION_TYPE \

diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index ea68e8957910c56a3cf6a27bcdf9353671973b10..d8557fcaf83e23c98e2b80409b06cae83decf34f 100644 (file)
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -66,6 +66,11 @@ public:
     d_zeroCtor(0),
     d_argEnumerators(NULL) {
 
+    //Assert(type.isDatatype());
+    Debug("te") << "datatype is datatype? " << type.isDatatype() << std::endl;
+    Debug("te") << "datatype is kind " << type.getKind() << std::endl;
+    Debug("te") << "datatype is " << type << std::endl;
+
     /* find the "zero" constructor (the first non-recursive one) */
     /* FIXME: this isn't sufficient for mutually-recursive datatypes! */
     while(d_zeroCtor < d_datatype.getNumConstructors()) {