Eliminate most of the internal representation infrastructure for tuples and records, replace with datatypes throughout, update cvc printer for tuples/records. Minor changes to API for records and tuples.

1 files changed, 5 insertions, 4 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 0b9557cc8..ce7a92b48 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -20,6 +20,7 @@
 
 #include "expr/node_manager.h"
 #include "expr/variable_type_map.h"
+#include "expr/node_manager_attributes.h"
 #include "options/options.h"
 #include "util/statistics_registry.h"
 
@@ -596,18 +597,18 @@ FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) {
   return FunctionType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes))));
 }
 
-TupleType ExprManager::mkTupleType(const std::vector<Type>& types) {
+DatatypeType ExprManager::mkTupleType(const std::vector<Type>& types) {
   NodeManagerScope nms(d_nodeManager);
   std::vector<TypeNode> typeNodes;
   for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) {
      typeNodes.push_back(*types[i].d_typeNode);
   }
-  return TupleType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes))));
+  return DatatypeType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes))));
 }
 
-RecordType ExprManager::mkRecordType(const Record& rec) {
+DatatypeType ExprManager::mkRecordType(const Record& rec) {
   NodeManagerScope nms(d_nodeManager);
-  return RecordType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkRecordType(rec))));
+  return DatatypeType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkRecordType(rec))));
 }
 
 SExprType ExprManager::mkSExprType(const std::vector<Type>& types) {