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: 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 ++++-
 2 files changed, 42 insertions(+), 1 deletion(-)

(limited to 'src')

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());
-- 
cgit v1.2.3