Fix Boolean terms w.r.t. parametric datatypes (e.g., (Pair Bool Bool) now works).

2 files changed, 59 insertions, 0 deletions

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 108c88829..30aa79aca 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -152,6 +152,40 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() {
     }
     return out;
   }
+  if(in.getType().isParametricDatatype() &&
+     in.getType().isInstantiatedDatatype()) {
+    // We have something here like (Pair Bool Bool)---need to dig inside
+    // and make it (Pair BV1 BV1)
+    Assert(as.isParametricDatatype() && as.isInstantiatedDatatype());
+    const Datatype* dt2 = &as[0].getDatatype();
+    std::vector<TypeNode> fromParams, toParams;
+    for(unsigned i = 0; i < dt2->getNumParameters(); ++i) {
+      fromParams.push_back(TypeNode::fromType(dt2->getParameter(i)));
+      toParams.push_back(as[i + 1]);
+    }
+    const Datatype* dt1 = d_datatypeCache[dt2];
+    Assert(dt1 != NULL, "expected datatype in cache");
+    Assert(*dt1 == in.getType()[0].getDatatype(), "improper rewriteAs() between datatypes");
+    Node out;
+    for(size_t i = 0; i < dt1->getNumConstructors(); ++i) {
+      DatatypeConstructor ctor = (*dt1)[i];
+      NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR);
+      appctorb << (*dt2)[i].getConstructor();
+      for(size_t j = 0; j < ctor.getNumArgs(); ++j) {
+        TypeNode asType = TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType());
+        asType = asType.substitute(fromParams.begin(), fromParams.end(), toParams.begin(), toParams.end());
+        appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, ctor[j].getSelector(), in), asType);
+      }
+      Node appctor = appctorb;
+      if(i == 0) {
+        out = appctor;
+      } else {
+        Node newOut = NodeManager::currentNM()->mkNode(kind::ITE, ctor.getTester(), appctor, out);
+        out = newOut;
+      }
+    }
+    return out;
+  }
 
   Unhandled(in);
 }
diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp
index 686ecbbe6..a66e02778 100644
--- a/src/smt/model_postprocessor.cpp
+++ b/src/smt/model_postprocessor.cpp
@@ -88,6 +88,31 @@ Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) {
     Node val = rewriteAs(asa.getExpr(), asType[1]);
     return NodeManager::currentNM()->mkConst(ArrayStoreAll(asType.toType(), val.toExpr()));
   }
+  if(n.getType().isParametricDatatype() &&
+     n.getType().isInstantiatedDatatype() &&
+     asType.isParametricDatatype() &&
+     asType.isInstantiatedDatatype() &&
+     n.getType()[0] == asType[0]) {
+    // Here, we're doing something like rewriting a (Pair BV1 BV1) as a
+    // (Pair Bool Bool).
+    const Datatype* dt2 = &asType[0].getDatatype();
+    std::vector<TypeNode> fromParams, toParams;
+    for(unsigned i = 0; i < dt2->getNumParameters(); ++i) {
+      fromParams.push_back(TypeNode::fromType(dt2->getParameter(i)));
+      toParams.push_back(asType[i + 1]);
+    }
+    Assert(dt2 == &Datatype::datatypeOf(n.getOperator().toExpr()));
+    size_t ctor_ix = Datatype::indexOf(n.getOperator().toExpr());
+    NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR);
+    appctorb << (*dt2)[ctor_ix].getConstructor();
+    for(size_t j = 0; j < n.getNumChildren(); ++j) {
+      TypeNode asType = TypeNode::fromType(SelectorType((*dt2)[ctor_ix][j].getSelector().getType()).getRangeType());
+      asType = asType.substitute(fromParams.begin(), fromParams.end(), toParams.begin(), toParams.end());
+      appctorb << rewriteAs(n[j], asType);
+    }
+    Node out = appctorb;
+    return out;
+  }
   if(asType.getNumChildren() != n.getNumChildren() ||
      n.getMetaKind() == kind::metakind::CONSTANT) {
     return n;