Addressed many of the concerns raised in the public interface review of CVC4 Datatypes (bug #283) by Chris Conway. Thanks, Chris!

4 files changed, 8 insertions, 8 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 12a60021e..576d0324d 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -638,7 +638,7 @@ void ExprManager::checkResolvedDatatype(DatatypeType dtt) const {
   for(Datatype::const_iterator i = dt.begin(), i_end = dt.end();
       i != i_end;
       ++i) {
-    const Datatype::Constructor& c = *i;
+    const DatatypeConstructor& c = *i;
     Type testerType CVC4_UNUSED = c.getTester().getType();
     Assert(c.isResolved() &&
            testerType.isTester() &&
@@ -651,10 +651,10 @@ void ExprManager::checkResolvedDatatype(DatatypeType dtt) const {
            ConstructorType(ctorType).getRangeType() == dtt,
            "malformed constructor in datatype post-resolution");
     // for all selectors...
-    for(Datatype::Constructor::const_iterator j = c.begin(), j_end = c.end();
+    for(DatatypeConstructor::const_iterator j = c.begin(), j_end = c.end();
         j != j_end;
         ++j) {
-      const Datatype::Constructor::Arg& a = *j;
+      const DatatypeConstructorArg& a = *j;
       Type selectorType = a.getSelector().getType();
       Assert(a.isResolved() &&
              selectorType.isSelector() &&
@@ -669,7 +669,7 @@ void ExprManager::checkResolvedDatatype(DatatypeType dtt) const {
   }
 }
 
-ConstructorType ExprManager::mkConstructorType(const Datatype::Constructor& constructor, Type range) const {
+ConstructorType ExprManager::mkConstructorType(const DatatypeConstructor& constructor, Type range) const {
   NodeManagerScope nms(d_nodeManager);
   return Type(d_nodeManager, new TypeNode(d_nodeManager->mkConstructorType(constructor, *range.d_typeNode)));
 }
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index ade9a334d..81d30fd1e 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -381,7 +381,7 @@ public:
   /**
    * Make a type representing a constructor with the given parameterization.
    */
-  ConstructorType mkConstructorType(const Datatype::Constructor& constructor, Type range) const;
+  ConstructorType mkConstructorType(const DatatypeConstructor& constructor, Type range) const;
 
   /** Make a type representing a selector with the given parameterization. */
   SelectorType mkSelectorType(Type domain, Type range) const;
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 3b4d8ac66..2bf0a864a 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -298,11 +298,11 @@ TypeNode NodeManager::getType(TNode n, bool check)
   return typeNode;
 }
 
-TypeNode NodeManager::mkConstructorType(const Datatype::Constructor& constructor,
+TypeNode NodeManager::mkConstructorType(const DatatypeConstructor& constructor,
                                         TypeNode range) {
   std::vector<TypeNode> sorts;
   Debug("datatypes") << "ctor name: " << constructor.getName() << std::endl;
-  for(Datatype::Constructor::const_iterator i = constructor.begin();
+  for(DatatypeConstructor::const_iterator i = constructor.begin();
       i != constructor.end();
       ++i) {
     TypeNode selectorType = *(*i).getSelector().getType().d_typeNode;
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index adba8087c..3646e91c5 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -580,7 +580,7 @@ public:
   inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType);
 
   /** Make a type representing a constructor with the given parameterization */
-  TypeNode mkConstructorType(const Datatype::Constructor& constructor, TypeNode range);
+  TypeNode mkConstructorType(const DatatypeConstructor& constructor, TypeNode range);
 
   /** Make a type representing a selector with the given parameterization */
   inline TypeNode mkSelectorType(TypeNode domain, TypeNode range);