More complete fix for bug 484 (includes fixes for records and tuples).

3 files changed, 171 insertions, 24 deletions

diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h
index 8ee275f70..2a74f6d15 100644
--- a/src/theory/datatypes/type_enumerator.h
+++ b/src/theory/datatypes/type_enumerator.h
@@ -92,23 +92,21 @@ 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),
+  DatatypesEnumerator(const DatatypesEnumerator& de) throw() :
+    TypeEnumeratorBase<DatatypesEnumerator>(de.getType()),
+    d_datatype(de.d_datatype),
+    d_ctor(de.d_ctor),
+    d_zeroCtor(de.d_zeroCtor),
     d_argEnumerators(NULL) {
-    
-    if (other.d_argEnumerators != NULL) {
-      d_argEnumerators = new TypeEnumerator*[d_datatype[d_ctor].getNumArgs()];
+
+    if(de.d_argEnumerators != NULL) {
+      newEnumerators();
       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;
+        if(de.d_argEnumerators[a] != NULL) {
+          d_argEnumerators[a] = new TypeEnumerator(*de.d_argEnumerators[a]);
         }
-       }
-    }             
+      }
+    }
   }
 
   ~DatatypesEnumerator() throw() {
@@ -174,6 +172,14 @@ public:
 class TupleEnumerator : public TypeEnumeratorBase<TupleEnumerator> {
   TypeEnumerator** d_enumerators;
 
+  /** Allocate and initialize the delegate enumerators */
+  void newEnumerators() {
+    d_enumerators = new TypeEnumerator*[getType().getNumChildren()];
+    for(size_t i = 0; i < getType().getNumChildren(); ++i) {
+      d_enumerators[i] = NULL;
+    }
+  }
+
   void deleteEnumerators() throw() {
     if(d_enumerators != NULL) {
       for(size_t i = 0; i < getType().getNumChildren(); ++i) {
@@ -189,9 +195,20 @@ public:
   TupleEnumerator(TypeNode type) throw() :
     TypeEnumeratorBase<TupleEnumerator>(type) {
     Assert(type.isTuple());
-    d_enumerators = new TypeEnumerator*[type.getNumChildren()];
-    for(size_t i = 0; i < type.getNumChildren(); ++i) {
-      d_enumerators[i] = new TypeEnumerator(type[i]);
+    newEnumerators();
+  }
+
+  TupleEnumerator(const TupleEnumerator& te) throw() :
+    TypeEnumeratorBase<TupleEnumerator>(te.getType()),
+    d_enumerators(NULL) {
+
+    if(te.d_enumerators != NULL) {
+      newEnumerators();
+      for(size_t i = 0; i < getType().getNumChildren(); ++i) {
+        if(te.d_enumerators[i] != NULL) {
+          d_enumerators[i] = new TypeEnumerator(*te.d_enumerators[i]);
+        }
+      }
     }
   }
 
@@ -240,9 +257,19 @@ public:
 class RecordEnumerator : public TypeEnumeratorBase<RecordEnumerator> {
   TypeEnumerator** d_enumerators;
 
+  /** Allocate and initialize the delegate enumerators */
+  void newEnumerators() {
+    const Record& rec = getType().getConst<Record>();
+    d_enumerators = new TypeEnumerator*[rec.getNumFields()];
+    for(size_t i = 0; i < rec.getNumFields(); ++i) {
+      d_enumerators[i] = new TypeEnumerator(TypeNode::fromType(rec[i].second));
+    }
+  }
+
   void deleteEnumerators() throw() {
     if(d_enumerators != NULL) {
-      for(size_t i = 0; i < getType().getNumChildren(); ++i) {
+      const Record& rec = getType().getConst<Record>();
+      for(size_t i = 0; i < rec.getNumFields(); ++i) {
         delete d_enumerators[i];
       }
       delete [] d_enumerators;
@@ -255,12 +282,20 @@ public:
   RecordEnumerator(TypeNode type) throw() :
     TypeEnumeratorBase<RecordEnumerator>(type) {
     Assert(type.isRecord());
-    const Record& rec = getType().getConst<Record>();
-    Debug("te") << "creating record enumerator for " << type << std::endl;
-    d_enumerators = new TypeEnumerator*[rec.getNumFields()];
-    for(size_t i = 0; i < rec.getNumFields(); ++i) {
-      Debug("te") << " - sub-enumerator for " << rec[i].second << std::endl;
-      d_enumerators[i] = new TypeEnumerator(TypeNode::fromType(rec[i].second));
+    newEnumerators();
+  }
+
+  RecordEnumerator(const RecordEnumerator& re) throw() :
+    TypeEnumeratorBase<RecordEnumerator>(re.getType()),
+    d_enumerators(NULL) {
+
+    if(re.d_enumerators != NULL) {
+      newEnumerators();
+      for(size_t i = 0; i < getType().getNumChildren(); ++i) {
+        if(re.d_enumerators[i] != NULL) {
+          d_enumerators[i] = new TypeEnumerator(*re.d_enumerators[i]);
+        }
+      }
     }
   }
 
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 99cd6dbe6..4f473212c 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -144,6 +144,7 @@ BUG_TESTS = \
 	bug421b.smt2 \
 	bug425.cvc \
 	bug480.smt2 \
+	bug484.smt2 \
 	bug486.cvc
 
 TESTS =	$(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
diff --git a/test/regress/regress0/bug484.smt2 b/test/regress/regress0/bug484.smt2
new file mode 100644
index 000000000..afbd72420
--- /dev/null
+++ b/test/regress/regress0/bug484.smt2
@@ -0,0 +1,111 @@
+; Preamble  --------------
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-datatypes () ((UNIT (Unit))))
+(declare-datatypes () ((BOOL (Truth) (Falsity))))
+
+; Decls     --------------
+(declare-sort A 0)
+(declare-sort B 0)
+(declare-sort C 0)
+(declare-sort D 0)
+(declare-datatypes () ((E (one) (two) (three))))
+(declare-datatypes () ((F (four) (five) (six))))
+(declare-datatypes () ((G (c_G (seven BOOL)))))
+
+(declare-datatypes () 
+  ((H
+    (c_H 
+      (foo1 BOOL) 
+      (foo2 A) 
+      (foo3 B) 
+      (foo4 B) 
+      (foo5 Int)
+    )
+  ))
+)
+
+(declare-datatypes () 
+  ((I 
+    (c_I 
+      (bar1 E) 
+      (bar2 Int) 
+      (bar3 Int) 
+      (bar4 A)
+    )
+  ))
+)
+
+(declare-datatypes () 
+  ((J 
+    (c_J 
+      (f1 BOOL) 
+      (f2 Int) 
+      (f3 Int) 
+      (f4 Int) 
+      (f5 I) 
+      (f6 B) 
+      (f7 C)
+    )
+  ))
+)
+
+(declare-datatypes () 
+  ((K 
+    (c_K 
+      (g1 BOOL) 
+      (g2 F) 
+      (g3 A) 
+      (g4 BOOL)
+    )
+  ))
+)
+
+; Var Decls --------------
+(declare-fun s1 () (Array A J))
+(declare-fun s2 () (Array A J))
+(declare-fun e1 () (Array A K))
+(declare-fun e2 () (Array A K))
+(declare-fun x  () A)
+(declare-fun y  () A)
+(declare-fun foo (A) A)
+(declare-fun bar (A) C)
+
+
+; Asserts   --------------
+(assert 
+  (not 
+    (= 
+      (ite 
+        (=> 
+          (= y (g3 (select e1 x)))
+          (=> 
+            (= s2 
+               (store 
+                 s1 
+                 y 
+                 (let ((z (select s1 y)))
+                   (c_J 
+                     (f1 z) 
+                     (f2 z) 
+                     (- (f3 (select s1 y)) 1) 
+                     (f4 z)
+                     (f5 z) 
+                     (f6 z) 
+                     (f7 z)
+                   )
+                 )
+               )
+            ) 
+            (forall ((s A)) (= (g3 (select e2 s)) s))
+          )
+        )
+       Truth 
+       Falsity
+      ) 
+      Truth
+    )
+  )
+)
+                           
+(check-sat)