Make tuple and record names unique. Do not print internal datatype declaration in...

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 34f2960be59ed43daabdd92c56d159c6147f6bab..b07af0c14271b408d3cb3d164557153f2befaf7a 100644 (file)
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -488,12 +488,19 @@ TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds)
 TypeNode NodeManager::TupleTypeCache::getTupleType( NodeManager * nm, std::vector< TypeNode >& types, unsigned index ) {
   if( index==types.size() ){
     if( d_data.isNull() ){
-      Datatype dt("__cvc4_tuple");
+      std::stringstream sst;
+      sst << "__cvc4_tuple";
+      for (unsigned i = 0; i < types.size(); ++ i) {
+        sst << "_" << types[i];
+      }
+      Datatype dt(sst.str());
       dt.setTuple();
-      DatatypeConstructor c("__cvc4_tuple_ctor");
+      std::stringstream ssc;
+      ssc << sst.str() << "_ctor";
+      DatatypeConstructor c(ssc.str());
       for (unsigned i = 0; i < types.size(); ++ i) {
         std::stringstream ss;
-        ss << "__cvc4_tuple_stor_" << i;
+        ss << sst.str() << "_stor_" << i;
         c.addArg(ss.str().c_str(), types[i].toType());
       }
       dt.addConstructor(c);
@@ -510,9 +517,16 @@ TypeNode NodeManager::RecTypeCache::getRecordType( NodeManager * nm, const Recor
   if( index==rec.getNumFields() ){
     if( d_data.isNull() ){
       const Record::FieldVector& fields = rec.getFields();
-      Datatype dt("__cvc4_record");
+      std::stringstream sst;
+      sst << "__cvc4_record";
+      for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
+        sst << "_" << (*i).first << "_" << (*i).second;
+      }
+      Datatype dt(sst.str());
       dt.setRecord();
-      DatatypeConstructor c("__cvc4_record_ctor");
+      std::stringstream ssc;
+      ssc << sst.str() << "_ctor";
+      DatatypeConstructor c(ssc.str());
       for(Record::FieldVector::const_iterator i = fields.begin(); i != fields.end(); ++i) {
         c.addArg((*i).first, (*i).second);
       }

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 11cf7dd11575d21c9c38eb090dc00e9a05f564ab..b7e1520b78b96063d8ad0da5af89e227750dbbad 100644 (file)
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -1248,58 +1248,61 @@ static void toStream(std::ostream& out, const GetOptionCommand* c, bool cvc3Mode
 
 static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c, bool cvc3Mode) throw() {
   const vector<DatatypeType>& datatypes = c->getDatatypes();
-  out << "DATATYPE" << endl;
-  bool firstDatatype = true;
-  for(vector<DatatypeType>::const_iterator i = datatypes.begin(),
-        i_end = datatypes.end();
-      i != i_end;
-      ++i) {
-    if(! firstDatatype) {
-      out << ',' << endl;
-    }
-    const Datatype& dt = (*i).getDatatype();
-    out << "  " << dt.getName();
-    if(dt.isParametric()) {
-      out << '[';
-      for(size_t j = 0; j < dt.getNumParameters(); ++j) {
-        if(j > 0) {
-          out << ',';
-        }
-        out << dt.getParameter(j);
+  //do not print tuple/datatype internal declarations
+  if( datatypes.size()!=1 || ( !datatypes[0].getDatatype().isTuple() && !datatypes[0].getDatatype().isRecord() ) ){
+    out << "DATATYPE" << endl;
+    bool firstDatatype = true;
+    for(vector<DatatypeType>::const_iterator i = datatypes.begin(),
+          i_end = datatypes.end();
+        i != i_end;
+        ++i) {
+      if(! firstDatatype) {
+        out << ',' << endl;
       }
-      out << ']';
-    }
-    out << " = ";
-    bool firstConstructor = true;
-    for(Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) {
-      if(! firstConstructor) {
-        out << " | ";
-      }
-      firstConstructor = false;
-      const DatatypeConstructor& c = *j;
-      out << c.getName();
-      if(c.getNumArgs() > 0) {
-        out << '(';
-        bool firstSelector = true;
-        for(DatatypeConstructor::const_iterator k = c.begin(); k != c.end(); ++k) {
-          if(! firstSelector) {
-            out << ", ";
+      const Datatype& dt = (*i).getDatatype();
+      out << "  " << dt.getName();
+      if(dt.isParametric()) {
+        out << '[';
+        for(size_t j = 0; j < dt.getNumParameters(); ++j) {
+          if(j > 0) {
+            out << ',';
           }
-          firstSelector = false;
-          const DatatypeConstructorArg& selector = *k;
-          Type t = SelectorType(selector.getType()).getRangeType();
-          if( t.isDatatype() ){
-            const Datatype & sdt = ((DatatypeType)t).getDatatype();
-            out << selector.getName() << ": " << sdt.getName();
-          }else{
-            out << selector.getName() << ": " << t;
+          out << dt.getParameter(j);
+        }
+        out << ']';
+      }
+      out << " = ";
+      bool firstConstructor = true;
+      for(Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) {
+        if(! firstConstructor) {
+          out << " | ";
+        }
+        firstConstructor = false;
+        const DatatypeConstructor& c = *j;
+        out << c.getName();
+        if(c.getNumArgs() > 0) {
+          out << '(';
+          bool firstSelector = true;
+          for(DatatypeConstructor::const_iterator k = c.begin(); k != c.end(); ++k) {
+            if(! firstSelector) {
+              out << ", ";
+            }
+            firstSelector = false;
+            const DatatypeConstructorArg& selector = *k;
+            Type t = SelectorType(selector.getType()).getRangeType();
+            if( t.isDatatype() ){
+              const Datatype & sdt = ((DatatypeType)t).getDatatype();
+              out << selector.getName() << ": " << sdt.getName();
+            }else{
+              out << selector.getName() << ": " << t;
+            }
           }
+          out << ')';
         }
-        out << ')';
       }
     }
+    out << endl << "END;";
   }
-  out << endl << "END;";
 }
 
 static void toStream(std::ostream& out, const CommentCommand* c, bool cvc3Mode) throw() {