From 5cee91676e0c0faf1f1fffcb8ffb71baaa6f8a60 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Mon, 6 Oct 2014 21:23:15 -0400
Subject: [PATCH] Fix a bug in tuple-record handling.  Thanks to Saumya Debray
 for the report.

---
 src/expr/node_manager.cpp                     | 38 +++++++++++++++++++
 src/smt/model_postprocessor.cpp               |  5 ++-
 test/regress/regress0/datatypes/Makefile.am   |  1 +
 .../regress0/datatypes/tuple-record-bug.cvc   | 20 ++++++++++
 4 files changed, 63 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress0/datatypes/tuple-record-bug.cvc

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index be3749021..d0a477b9a 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -397,6 +397,44 @@ TypeNode NodeManager::mkSubrangeType(const SubrangeBounds& bounds)
 TypeNode NodeManager::getDatatypeForTupleRecord(TypeNode t) {
   Assert(t.isTuple() || t.isRecord());
 
+  TypeNode tOrig = t;
+  if(t.isTuple()) {
+    vector<TypeNode> v;
+    bool changed = false;
+    for(size_t i = 0; i < t.getNumChildren(); ++i) {
+      TypeNode tn = t[i];
+      TypeNode base;
+      if(tn.isTuple() || tn.isRecord()) {
+        base = getDatatypeForTupleRecord(tn);
+      } else {
+        base = tn.getBaseType();
+      }
+      changed = changed || (tn != base);
+      v.push_back(base);
+    }
+    if(changed) {
+      t = mkTupleType(v);
+    }
+  } else {
+    const Record& r = t.getRecord();
+    std::vector< std::pair<std::string, Type> > v;
+    bool changed = false;
+    for(Record::iterator i = r.begin(); i != r.end(); ++i) {
+      Type tn = (*i).second;
+      Type base;
+      if(tn.isTuple() || tn.isRecord()) {
+        base = getDatatypeForTupleRecord(TypeNode::fromType(tn)).toType();
+      } else {
+        base = tn.getBaseType();
+      }
+      changed = changed || (tn != base);
+      v.push_back(std::make_pair((*i).first, base));
+    }
+    if(changed) {
+      t = mkRecordType(Record(v));
+    }
+  }
+
   // if the type doesn't have an associated datatype, then make one for it
   TypeNode& dtt = d_tupleAndRecordTypes[t];
   if(dtt.isNull()) {
diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index eea8d2282..dd9d0a78c 100644
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -163,7 +163,10 @@ void ModelPostprocessor::visit(TNode current, TNode parent) {
     Assert(t == expectType.end());
     d_nodes[current] = b;
     Debug("tuprec") << "returning " << d_nodes[current] << endl;
-    Assert(d_nodes[current].getType() == expectType);
+    // The assert below is too strong---we might be returning a model value but
+    // expect a type that still uses datatypes for tuples/records.  If it's
+    // really not the right type we should catch it in SmtEngine anyway.
+    // Assert(d_nodes[current].getType() == expectType);
   } else if(current.getType().hasAttribute(expr::DatatypeRecordAttr())) {
     Assert(current.getKind() == kind::APPLY_CONSTRUCTOR);
     TypeNode expectType = current.getType().getAttribute(expr::DatatypeRecordAttr());
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index e8a8f16f5..c02a70819 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -23,6 +23,7 @@ MAKEFLAGS = -k
 TESTS =	\
 	tuple.cvc \
 	tuple-model.cvc \
+	tuple-record-bug.cvc \
 	rec1.cvc \
 	rec2.cvc \
 	rec4.cvc \
diff --git a/test/regress/regress0/datatypes/tuple-record-bug.cvc b/test/regress/regress0/datatypes/tuple-record-bug.cvc
new file mode 100644
index 000000000..33c68dece
--- /dev/null
+++ b/test/regress/regress0/datatypes/tuple-record-bug.cvc
@@ -0,0 +1,20 @@
+% EXPECT: invalid
+
+Mem_0 : TYPE = ARRAY INT OF INT;
+
+MEMORY : TYPE = [# int : Mem_0, queries : Mem_0 #];
+
+x : INT;
+
+foo : MEMORY -> MEMORY
+    = LAMBDA (x : MEMORY) : LET y = x WITH .int := x.int IN y;
+
+m : MEMORY;
+
+w : [MEMORY,INT] =
+        IF x = 0
+        THEN (foo(m),0)
+        ELSE (m, 0)
+        ENDIF;
+
+QUERY w.1 = 1;
-- 
2.30.2