From: Dejan Jovanović <dejan@cs.nyu.edu>
Date: Sat, 22 Dec 2012 00:08:26 +0000 (-0500)
Subject: adding copy constructor for the datatype enumerator
X-Git-Tag: cvc5-1.0.0~7391^2~33
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d1cd7732b17b280ad17d12a84399ff05cd1d77c4;p=cvc5.git

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 d8557fcaf..2a14d7fba 100644
--- 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();
   }