adding copy constructor for the datatype enumerator

fixes bug 484

diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index d8557fcaf83e23c98e2b80409b06cae83decf34f..2a14d7fbab13f351f4bebb684092863748652995 100644 (file)
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -57,6 +57,7 @@ class DatatypesEnumerator : public TypeEnumeratorBase<DatatypesEnumerator> {
     }
   }
 
+
 public:
 
   DatatypesEnumerator(TypeNode type) throw() :
@@ -91,6 +92,25 @@ public:
     newEnumerators();
   }
 
+  DatatypesEnumerator(const DatatypesEnumerator& other) :
+    TypeEnumeratorBase<DatatypesEnumerator>(other.getType()),
+    d_datatype(other.d_datatype),
+    d_ctor(other.d_ctor),
+    d_zeroCtor(other.d_zeroCtor),
+    d_argEnumerators(NULL) {
+    
+    if (other.d_argEnumerators != NULL) {
+      d_argEnumerators = new TypeEnumerator*[d_datatype[d_ctor].getNumArgs()];
+      for(size_t a = 0; a < d_datatype[d_ctor].getNumArgs(); ++a) {
+        if (other.d_argEnumerators[a] != NULL) {
+          d_argEnumerators[a] = new TypeEnumerator(*other.d_argEnumerators[a]);
+        } else {
+          d_argEnumerators[a] = NULL;
+        }
+       }
+    }             
+  }
+
   ~DatatypesEnumerator() throw() {
     deleteEnumerators();
   }