Support for Boolean term conversion in datatypes.

1 files changed, 13 insertions, 2 deletions

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 2cfeaafc1..524344612 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -817,7 +817,7 @@ void CvcPrinter::toStream(std::ostream& out, Model& m, const Command* c) const t
     TypeNode tn = TypeNode::fromType( ((const DeclareTypeCommand*)c)->getType() );
     if( options::modelUninterpDtEnum() && tn.isSort() &&
         tm.d_rep_set.d_type_reps.find( tn )!=tm.d_rep_set.d_type_reps.end() ){
-      out << "DATATYPE " << std::endl;
+      out << "DATATYPE" << std::endl;
       out << "  " << dynamic_cast<const DeclareTypeCommand*>(c)->getSymbol() << " = ";
       for( size_t i=0; i<(*tm.d_rep_set.d_type_reps.find(tn)).second.size(); i++ ){
         if (i>0) {
@@ -1068,7 +1068,18 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) thr
       out << ',' << endl;
     }
     const Datatype& dt = (*i).getDatatype();
-    out << "  " << dt.getName() << " = ";
+    out << "  " << dt.getName();
+    if(dt.isParametric()) {
+      out << '[';
+      for(size_t j = 0; j < dt.getNumParameters(); ++j) {
+        if(j > 0) {
+          out << ',';
+        }
+        out << dt.getParameter(j);
+      }
+      out << ']';
+    }
+    out << " = ";
     bool firstConstructor = true;
     for(Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) {
       if(! firstConstructor) {