Fix model postprocessor for tuples, add regression.

3 files changed, 80 insertions, 55 deletions

diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index f9e449be3..0ba668b33 100644
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -156,70 +156,80 @@ Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) {
 void ModelPostprocessor::visit(TNode current, TNode parent) {
   Debug("tuprec") << "visiting " << current << endl;
   Assert(!alreadyVisited(current, TNode::null()));
+  bool rewriteChildren = false;
   if(current.getType().hasAttribute(expr::DatatypeTupleAttr())) {
-    Assert(current.getKind() == kind::APPLY_CONSTRUCTOR);
-    TypeNode expectType = current.getType().getAttribute(expr::DatatypeTupleAttr());
-    NodeBuilder<> b(kind::TUPLE);
-    TypeNode::iterator t = expectType.begin();
-    for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++t) {
-      Assert(alreadyVisited(*i, TNode::null()));
-      Assert(t != expectType.end());
-      TNode n = d_nodes[*i];
-      n = n.isNull() ? *i : n;
-      if(!n.getType().isSubtypeOf(*t)) {
-        Assert(n.getType().isBitVector(1u) ||
-               (n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())));
-        Assert(n.isConst());
-        Assert((*t).isBoolean());
-        if(n.getType().isBitVector(1u)) {
-          b << NodeManager::currentNM()->mkConst(bool(n.getConst<BitVector>().getValue() == 1));
+    if(current.getKind() == kind::APPLY_CONSTRUCTOR){
+      TypeNode expectType = current.getType().getAttribute(expr::DatatypeTupleAttr());
+      NodeBuilder<> b(kind::TUPLE);
+      TypeNode::iterator t = expectType.begin();
+      for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++t) {
+        Assert(alreadyVisited(*i, TNode::null()));
+        Assert(t != expectType.end());
+        TNode n = d_nodes[*i];
+        n = n.isNull() ? *i : n;
+        if(!n.getType().isSubtypeOf(*t)) {
+          Assert(n.getType().isBitVector(1u) ||
+                 (n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())));
+          Assert(n.isConst());
+          Assert((*t).isBoolean());
+          if(n.getType().isBitVector(1u)) {
+            b << NodeManager::currentNM()->mkConst(bool(n.getConst<BitVector>().getValue() == 1));
+          } else {
+            // we assume (by construction) false is first; see boolean_terms.cpp
+            b << NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n.getOperator().toExpr()) == 1));
+          }
         } else {
-          // we assume (by construction) false is first; see boolean_terms.cpp
-          b << NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n.getOperator().toExpr()) == 1));
+          b << n;
         }
-      } else {
-        b << n;
       }
+      Assert(t == expectType.end());
+      d_nodes[current] = b;
+      Debug("tuprec") << "returning " << d_nodes[current] << ", operator = " << d_nodes[current].getOperator() << endl;
+      // 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);
+      return;
+    }else{
+      rewriteChildren = true;
     }
-    Assert(t == expectType.end());
-    d_nodes[current] = b;
-    Debug("tuprec") << "returning " << d_nodes[current] << ", operator = " << d_nodes[current].getOperator() << endl;
-    // 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());
-    const Record& expectRec = expectType.getConst<Record>();
-    NodeBuilder<> b(kind::RECORD);
-    b << current.getType().getAttribute(expr::DatatypeRecordAttr());
-    const Record::FieldVector& fields = expectRec.getFields();
-    Record::FieldVector::const_iterator t = fields.begin();
-    for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++t) {
-      Assert(alreadyVisited(*i, TNode::null()));
-      Assert(t != fields.end());
-      TNode n = d_nodes[*i];
-      n = n.isNull() ? *i : n;
-      if(!n.getType().isSubtypeOf(TypeNode::fromType((*t).second))) {
-        Assert(n.getType().isBitVector(1u) ||
-               (n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())));
-        Assert(n.isConst());
-        Assert((*t).second.isBoolean());
-        if(n.getType().isBitVector(1u)) {
-          b << NodeManager::currentNM()->mkConst(bool(n.getConst<BitVector>().getValue() == 1));
+    if(current.getKind() == kind::APPLY_CONSTRUCTOR){
+      //Assert(current.getKind() == kind::APPLY_CONSTRUCTOR);
+      TypeNode expectType = current.getType().getAttribute(expr::DatatypeRecordAttr());
+      const Record& expectRec = expectType.getConst<Record>();
+      NodeBuilder<> b(kind::RECORD);
+      b << current.getType().getAttribute(expr::DatatypeRecordAttr());
+      const Record::FieldVector& fields = expectRec.getFields();
+      Record::FieldVector::const_iterator t = fields.begin();
+      for(TNode::iterator i = current.begin(); i != current.end(); ++i, ++t) {
+        Assert(alreadyVisited(*i, TNode::null()));
+        Assert(t != fields.end());
+        TNode n = d_nodes[*i];
+        n = n.isNull() ? *i : n;
+        if(!n.getType().isSubtypeOf(TypeNode::fromType((*t).second))) {
+          Assert(n.getType().isBitVector(1u) ||
+                 (n.getType().isDatatype() && n.getType().hasAttribute(BooleanTermAttr())));
+          Assert(n.isConst());
+          Assert((*t).second.isBoolean());
+          if(n.getType().isBitVector(1u)) {
+            b << NodeManager::currentNM()->mkConst(bool(n.getConst<BitVector>().getValue() == 1));
+          } else {
+            // we assume (by construction) false is first; see boolean_terms.cpp
+            b << NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n.getOperator().toExpr()) == 1));
+          }
         } else {
-          // we assume (by construction) false is first; see boolean_terms.cpp
-          b << NodeManager::currentNM()->mkConst(bool(Datatype::indexOf(n.getOperator().toExpr()) == 1));
+          b << n;
         }
-      } else {
-        b << n;
       }
+      Assert(t == fields.end());
+      d_nodes[current] = b;
+      Debug("tuprec") << "returning " << d_nodes[current] << ", operator = " << d_nodes[current].getOperator() << endl;
+      Assert(d_nodes[current].getType() == expectType);
+      return;
+    }else{
+      rewriteChildren = true;
     }
-    Assert(t == fields.end());
-    d_nodes[current] = b;
-    Debug("tuprec") << "returning " << d_nodes[current] << ", operator = " << d_nodes[current].getOperator() << endl;
-    Assert(d_nodes[current].getType() == expectType);
   } else if(current.getKind() == kind::APPLY_CONSTRUCTOR &&
             ( current.getOperator().hasAttribute(BooleanTermAttr()) ||
               ( current.getOperator().getKind() == kind::APPLY_TYPE_ASCRIPTION &&
@@ -257,9 +267,13 @@ void ModelPostprocessor::visit(TNode current, TNode parent) {
     Debug("boolean-terms") << "model-post: " << current << endl
                            << "- returning " << n << endl;
     d_nodes[current] = n;
+    return;
   //all kinds with children that can occur in nodes in a model go here
   } else if(current.getKind() == kind::LAMBDA || current.getKind() == kind::SINGLETON || current.getKind() == kind::UNION || 
             current.getKind()==kind::STORE || current.getKind()==kind::STORE_ALL || current.getKind()==kind::APPLY_CONSTRUCTOR ) {
+    rewriteChildren = true;
+  }
+  if( rewriteChildren ){
     // rewrite based on children
     bool self = true;
     for(size_t i = 0; i < current.getNumChildren(); ++i) {
diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am
index 1759d2924..350a948aa 100644
--- a/test/regress/regress0/datatypes/Makefile.am
+++ b/test/regress/regress0/datatypes/Makefile.am
@@ -69,7 +69,8 @@ TESTS =	\
 	cdt-model-cade15.smt2 \
 	sc-cdt1.smt2  \
 	conqueue-dt-enum-iloop.smt2 \
-	coda_simp_model.smt2
+	coda_simp_model.smt2 \
+	Test1-tup-mp.cvc
 
 FAILING_TESTS = \
 	datatype-dump.cvc
diff --git a/test/regress/regress0/datatypes/Test1-tup-mp.cvc b/test/regress/regress0/datatypes/Test1-tup-mp.cvc
new file mode 100644
index 000000000..6f49496f3
--- /dev/null
+++ b/test/regress/regress0/datatypes/Test1-tup-mp.cvc
@@ -0,0 +1,10 @@
+% EXPECT: sat
+TEST : TYPE = INT -> [INT, INT];
+
+test: TEST;
+
+ASSERT test(5) = (2, 3);
+ASSERT test(7) = (3, 4);
+
+CHECKSAT;
+