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

3 files changed, 7 insertions, 7 deletions

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 7a45c98aa..23768545d 100644
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -67,7 +67,7 @@ public:
       size_t selectorIndex = Datatype::indexOf(selectorExpr);
       size_t constructorIndex = Datatype::indexOf(constructorExpr);
       const Datatype& dt = Datatype::datatypeOf(constructorExpr);
-      const Datatype::Constructor& c = dt[constructorIndex];
+      const DatatypeConstructor& c = dt[constructorIndex];
       if(c.getNumArgs() > selectorIndex &&
          c[selectorIndex].getSelector() == selectorExpr) {
         Debug("datatypes-rewrite") << "DatatypesRewriter::postRewrite: "
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 6b067c681..75980993b 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -32,7 +32,7 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::datatypes;
 
-const Datatype::Constructor& TheoryDatatypes::getConstructor( Node cons )
+const DatatypeConstructor& TheoryDatatypes::getConstructor( Node cons )
 {
   Expr consExpr = cons.toExpr();
   return Datatype::datatypeOf(consExpr)[ Datatype::indexOf(consExpr) ];
@@ -272,7 +272,7 @@ void TheoryDatatypes::check(Effort e) {
             }
           }
           if( !cons.isNull() ) {
-            const Datatype::Constructor& cn = getConstructor( cons );
+            const DatatypeConstructor& cn = getConstructor( cons );
             Debug("datatypes-split") << "*************Split for possible constructor " << cons << endl;
             Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( cn.getTester() ), (*i).first );
             NodeBuilder<> nb(kind::OR);
@@ -464,7 +464,7 @@ bool TheoryDatatypes::checkInstantiate( Node te, Node cons )
     vector< Node > selectorVals;
     selectorVals.push_back( cons );
     bool foundSel = false;
-    const Datatype::Constructor& cn = getConstructor( cons );
+    const DatatypeConstructor& cn = getConstructor( cons );
     for( unsigned int i=0; i<cn.getNumArgs(); i++ ) {
       Node s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( cn[i].getSelector() ), te );
       if( d_selectors.find( s ) != d_selectors.end() ) {
@@ -480,7 +480,7 @@ bool TheoryDatatypes::checkInstantiate( Node te, Node cons )
       if( val.getType()!=te.getType() ){ //IDT-param
         Assert( Datatype::datatypeOf( cons.toExpr() ).isParametric() );
         Debug("datatypes-gt") << "Inst: ambiguous type for " << cons << ", ascribe to " << te.getType() << std::endl;
-        const Datatype::Constructor& dtc = Datatype::datatypeOf(cons.toExpr())[Datatype::indexOf(cons.toExpr())];
+        const DatatypeConstructor& dtc = Datatype::datatypeOf(cons.toExpr())[Datatype::indexOf(cons.toExpr())];
         Debug("datatypes-gt") << "constructor is " << dtc << std::endl;
         Type tspec = dtc.getSpecializedConstructorType(te.getType().toType());
         Debug("datatypes-gt") << "tpec is " << tspec << std::endl;
@@ -537,7 +537,7 @@ bool TheoryDatatypes::collapseSelector( Node t ) {
     Node sel = t.getOperator();
     TypeNode selType = sel.getType();
     Node cons = getConstructorForSelector( sel );
-    const Datatype::Constructor& cn = getConstructor( cons );
+    const DatatypeConstructor& cn = getConstructor( cons );
     Node tmp = find( t[0] );
     Node retNode = t;
     if( tmp.getKind() == APPLY_CONSTRUCTOR ) {
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 433af38c3..4d429bc54 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -65,7 +65,7 @@ private:
   /** has seen cycle */
   context::CDO< bool > d_hasSeenCycle;
   /** get the constructor for the node */
-  const Datatype::Constructor& getConstructor( Node cons );
+  const DatatypeConstructor& getConstructor( Node cons );
   /** get the constructor for the selector */
   Node getConstructorForSelector( Node sel );