Fix a bug in tuple-record handling. Thanks to Saumya Debray for the report.

diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index be37490215be25204d54d4458c0b939be3a0bc4f..d0a477b9acd9b2ff8ab719887804ea9198e81d80 100644 (file)
--- 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 eea8d2282441fa9c4e3d788f2bd85cefc7faf2b0..dd9d0a78caa4ac81ef1c3881ac00089fb5c73bd9 100644 (file)
--- 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 e8a8f16f593e4723663d768944aaf420d60043e8..c02a708198b2a1412766112ca6dca0b0e00e38af 100644 (file)
--- 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 (file)
index 0000000..33c68de
--- /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;