Minor refactoring in preparation for datatypes node cycle breaking.

6 files changed, 63 insertions, 5 deletions

diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 001f38a79..a7039110f 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -1105,4 +1105,9 @@ std::ostream& operator<<(std::ostream& os, const DatatypeConstructorArg& arg) {
   return os;
 }
 
+DatatypeIndexConstant::DatatypeIndexConstant(unsigned index) throw(IllegalArgumentException) : d_index(index){
+
+}
+
+
 }/* CVC4 namespace */
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index dfd893fe8..06735262d 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -757,6 +757,49 @@ struct CVC4_PUBLIC DatatypeHashFunction {
   }
 };/* struct DatatypeHashFunction */
 
+
+
+/* stores an index to Datatype residing in NodeManager */
+class CVC4_PUBLIC DatatypeIndexConstant {
+public:
+
+  DatatypeIndexConstant(unsigned index) throw(IllegalArgumentException);
+
+  ~DatatypeIndexConstant() throw() { }
+
+  const unsigned getIndex() const throw() {
+    return d_index;
+  }
+  bool operator==(const DatatypeIndexConstant& uc) const throw() {
+    return d_index == uc.d_index;
+  }
+  bool operator!=(const DatatypeIndexConstant& uc) const throw() {
+    return !(*this == uc);
+  }
+  bool operator<(const DatatypeIndexConstant& uc) const throw() {
+    return d_index < uc.d_index;
+  }
+  bool operator<=(const DatatypeIndexConstant& uc) const throw() {
+    return d_index <= uc.d_index;
+  }
+  bool operator>(const DatatypeIndexConstant& uc) const throw() {
+    return !(*this <= uc);
+  }
+  bool operator>=(const DatatypeIndexConstant& uc) const throw() {
+    return !(*this < uc);
+  }
+private:
+  const unsigned d_index;
+};/* class DatatypeIndexConstant */
+
+struct CVC4_PUBLIC DatatypeIndexConstantHashFunction {
+  inline size_t operator()(const DatatypeIndexConstant& uc) const {
+    return IntegerHashFunction()(uc.getIndex());
+  }
+};/* struct DatatypeIndexConstantHashFunction */
+
+
+
 // FUNCTION DECLARATIONS FOR OUTPUT STREAMS
 
 std::ostream& operator<<(std::ostream& os, const Datatype& dt) CVC4_PUBLIC;
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index f7e76c06b..af4f89da1 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -176,6 +176,13 @@ NodeManager::~NodeManager() {
   d_tt_cache.d_children.clear();
   d_rt_cache.d_children.clear();
 
+  for( std::vector<Datatype*>::iterator datatype_iter = d_ownedDatatypes.begin(),	datatype_end = d_ownedDatatypes.end(); 
+       datatype_iter != datatype_end; ++datatype_iter) {
+    Datatype* datatype = *datatype_iter;
+    delete datatype;
+  }
+  d_ownedDatatypes.clear();
+
   Assert(!d_attrManager->inGarbageCollection() );
   while(!d_zombies.empty()) {
     reclaimZombies();
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 3c3636d5f..aa78c9627 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -165,6 +165,9 @@ class NodeManager {
    * A list of subscribers for NodeManager events.
    */
   std::vector<NodeManagerListener*> d_listeners;
+  
+  /** A list of datatypes owned by this node manager. */
+  std::vector<Datatype*> d_ownedDatatypes;
 
   /**
    * A map of tuple and record types to their corresponding datatype.
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 0c4d554ef..18157016f 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -566,7 +566,7 @@ const Datatype& DatatypeType::getDatatype() const {
   NodeManagerScope nms(d_nodeManager);
   if( d_typeNode->isParametricDatatype() ) {
     PrettyCheckArgument( (*d_typeNode)[0].getKind() == kind::DATATYPE_TYPE, this);
-    const Datatype& dt = (*d_typeNode)[0].getConst<Datatype>();
+    const Datatype& dt = (*d_typeNode)[0].getDatatype();
     return dt;
   } else {
     return d_typeNode->getDatatype();
diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index dc2370bea..ede710dad 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -275,14 +275,14 @@ bool TypeNode::isRecord() const {
 
 size_t TypeNode::getTupleLength() const {
   Assert(isTuple());
-  const Datatype& dt = getConst<Datatype>();
+  const Datatype& dt = getDatatype();
   Assert(dt.getNumConstructors()==1);
   return dt[0].getNumArgs();
 }
 
 vector<TypeNode> TypeNode::getTupleTypes() const {
   Assert(isTuple());
-  const Datatype& dt = getConst<Datatype>();
+  const Datatype& dt = getDatatype();
   Assert(dt.getNumConstructors()==1);
   vector<TypeNode> types;
   for(unsigned i = 0; i < dt[0].getNumArgs(); ++i) {
@@ -315,7 +315,7 @@ bool TypeNode::isInstantiatedDatatype() const {
   if(getKind() != kind::PARAMETRIC_DATATYPE) {
     return false;
   }
-  const Datatype& dt = (*this)[0].getConst<Datatype>();
+  const Datatype& dt = (*this)[0].getDatatype();
   unsigned n = dt.getNumParameters();
   Assert(n < getNumChildren());
   for(unsigned i = 0; i < n; ++i) {
@@ -329,7 +329,7 @@ bool TypeNode::isInstantiatedDatatype() const {
 /** Is this an instantiated datatype parameter */
 bool TypeNode::isParameterInstantiatedDatatype(unsigned n) const {
   AssertArgument(getKind() == kind::PARAMETRIC_DATATYPE, *this);
-  const Datatype& dt = (*this)[0].getConst<Datatype>();
+  const Datatype& dt = (*this)[0].getDatatype();
   AssertArgument(n < dt.getNumParameters(), *this);
   return TypeNode::fromType(dt.getParameter(n)) != (*this)[n + 1];
 }