Bug fixes and refactoring of parametric datatypes, add some regressions.

1 files changed, 40 insertions, 40 deletions

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 51ae0fd11..ba7902d32 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -137,13 +137,17 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode,
   TypeNode in_t = in.getType();
   if( processing.find( in_t )==processing.end() ){
     processing[in_t] = true;
-    if(in.getType().isDatatype()) {
-      if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) {
-        processing.erase( in_t );
-        return NodeManager::currentNM()->mkNode(kind::EQUAL, d_ttDt, in);
+    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]);
       }
-      Assert(as.isDatatype());
-      const Datatype* dt2 = &as.getDatatype();
       const Datatype* dt1;
       if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) {
         dt1 = d_datatypeCache[dt2];
@@ -151,14 +155,16 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode,
         dt1 = d_datatypeReverseCache[dt2];
       }
       Assert(dt1 != NULL, "expected datatype in cache");
-      Assert(*dt1 == in.getType().getDatatype(), "improper rewriteAs() between datatypes");
+      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) {
-          appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()), processing);
+          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_TOTAL, ctor[j].getSelector(), in), asType, processing);
         }
         Node appctor = appctorb;
         if(i == 0) {
@@ -171,35 +177,13 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode,
       processing.erase( in_t );
       return out;
     }
-    if(in.getType().isArray()) {
-      // convert in to in'
-      // e.g. in : (Array Int Bool)
-      // for in' : (Array Int (_ BitVec 1))
-      // then subs  in  |=>  \array_lambda ( \lambda (x:Int) . [convert (read a' x) x]
-      Assert(as.isArray());
-      Assert(as.getArrayIndexType() == in.getType().getArrayIndexType());
-      Assert(as.getArrayConstituentType() != in.getType().getArrayConstituentType());
-      Node x = NodeManager::currentNM()->mkBoundVar(as.getArrayIndexType());
-      Node boundvars = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, x);
-      Node sel = NodeManager::currentNM()->mkNode(kind::SELECT, in, x);
-      Node selprime = rewriteAs(sel, as.getArrayConstituentType(), processing);
-      Node lam = NodeManager::currentNM()->mkNode(kind::LAMBDA, boundvars, selprime);
-      Node out = NodeManager::currentNM()->mkNode(kind::ARRAY_LAMBDA, lam);
-      Assert(out.getType() == as);
-      processing.erase( in_t );
-      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]);
+    if(in.getType().isDatatype()) {
+      if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) {
+        processing.erase( in_t );
+        return NodeManager::currentNM()->mkNode(kind::EQUAL, d_ttDt, in);
       }
+      Assert(as.isDatatype());
+      const Datatype* dt2 = &as.getDatatype();
       const Datatype* dt1;
       if(d_datatypeCache.find(dt2) != d_datatypeCache.end()) {
         dt1 = d_datatypeCache[dt2];
@@ -207,16 +191,14 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode,
         dt1 = d_datatypeReverseCache[dt2];
       }
       Assert(dt1 != NULL, "expected datatype in cache");
-      Assert(*dt1 == in.getType()[0].getDatatype(), "improper rewriteAs() between datatypes");
+      Assert(*dt1 == in.getType().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_TOTAL, ctor[j].getSelector(), in), asType, processing);
+          appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()), processing);
         }
         Node appctor = appctorb;
         if(i == 0) {
@@ -229,6 +211,24 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode,
       processing.erase( in_t );
       return out;
     }
+    if(in.getType().isArray()) {
+      // convert in to in'
+      // e.g. in : (Array Int Bool)
+      // for in' : (Array Int (_ BitVec 1))
+      // then subs  in  |=>  \array_lambda ( \lambda (x:Int) . [convert (read a' x) x]
+      Assert(as.isArray());
+      Assert(as.getArrayIndexType() == in.getType().getArrayIndexType());
+      Assert(as.getArrayConstituentType() != in.getType().getArrayConstituentType());
+      Node x = NodeManager::currentNM()->mkBoundVar(as.getArrayIndexType());
+      Node boundvars = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, x);
+      Node sel = NodeManager::currentNM()->mkNode(kind::SELECT, in, x);
+      Node selprime = rewriteAs(sel, as.getArrayConstituentType(), processing);
+      Node lam = NodeManager::currentNM()->mkNode(kind::LAMBDA, boundvars, selprime);
+      Node out = NodeManager::currentNM()->mkNode(kind::ARRAY_LAMBDA, lam);
+      Assert(out.getType() == as);
+      processing.erase( in_t );
+      return out;
+    }
     Unhandled(in);
   }else{
     Message() << "Type " << in_t << " involving Boolean sort is not supported." << std::endl;