From 0d8c1936b8b8159af5f6688e63d74a806f48ac75 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 7 Jun 2013 11:30:00 -0400
Subject: [PATCH] Fix for bug 517.

---
 src/expr/type_node.cpp                     |  9 +++++++++
 src/smt/boolean_terms.cpp                  | 22 +++++++++++++++++++++-
 src/theory/arrays/theory_arrays_rewriter.h | 14 +++++++++-----
 3 files changed, 39 insertions(+), 6 deletions(-)

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index e654b5d71..1d4c330fa 100644
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -123,6 +123,15 @@ bool TypeNode::isSubtypeOf(TypeNode t) const {
     }
     return true;
   }
+  if(isFunction()) {
+    // A function is a subtype of another if the args are the same type, and 
+    // the return type is a subtype of the other's.  This is enough for now
+    // (and it's necessary for model generation, since a Real-valued function
+    // might return a constant Int and thus the model value is typed differently).
+    return t.isFunction() &&
+           getArgTypes() == t.getArgTypes() &&
+           getRangeType().isSubtypeOf(t.getRangeType());
+  }
   if(isPredicateSubtype()) {
     return getSubtypeParentType().isSubtypeOf(t);
   }
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 166a695a4..ffd17dc07 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -487,7 +487,27 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
         } else if(t.isArray()) {
           TypeNode indexType = convertType(t.getArrayIndexType(), false);
           TypeNode constituentType = convertType(t.getArrayConstituentType(), false);
-          if(indexType != t.getArrayIndexType() || constituentType != t.getArrayConstituentType()) {
+          if(indexType != t.getArrayIndexType() && constituentType == t.getArrayConstituentType()) {
+            TypeNode newType = nm->mkArrayType(indexType, constituentType);
+            Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
+                                  newType, "an array variable introduced by Boolean-term conversion",
+                                  NodeManager::SKOLEM_EXACT_NAME);
+            top.setAttribute(BooleanTermAttr(), n);
+            Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
+            Node n_ff = nm->mkNode(kind::SELECT, n, d_ff);
+            Node n_tt = nm->mkNode(kind::SELECT, n, d_tt);
+            Node base = nm->mkConst(ArrayStoreAll(ArrayType(top.getType().toType()), (*TypeEnumerator(n_ff.getType())).toExpr()));
+            Node repl = nm->mkNode(kind::STORE,
+                                   nm->mkNode(kind::STORE, base, nm->mkConst(true),
+                                              n_tt),
+                                   nm->mkConst(false), n_ff);
+            Debug("boolean-terms") << "array replacement: " << top << " => " << repl << endl;
+            d_smt.d_theoryEngine->getModel()->addSubstitution(top, repl);
+            d_termCache[make_pair(top, parentTheory)] = n;
+            result.top() << n;
+            worklist.pop();
+            goto next_worklist;
+          } else if(indexType != t.getArrayIndexType() || constituentType != t.getArrayConstituentType()) {
             TypeNode newType = nm->mkArrayType(indexType, constituentType);
             Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "'",
                                   newType, "an array variable introduced by Boolean-term conversion",
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index 18bbef8cf..5df06bda8 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -36,6 +36,10 @@ namespace attr {
 typedef expr::Attribute<attr::ArrayConstantMostFrequentValueCountTag, uint64_t> ArrayConstantMostFrequentValueCountAttr;
 typedef expr::Attribute<attr::ArrayConstantMostFrequentValueTag, Node> ArrayConstantMostFrequentValueAttr;
 
+static inline Node mkEqNode(Node a, Node b) {
+  return a.getType().isBoolean() ? a.iffNode(b) : a.eqNode(b);
+}
+
 class TheoryArraysRewriter {
   static Node normalizeConstant(TNode node) {
     return normalizeConstant(node, node[1].getType().getCardinality());
@@ -244,7 +248,7 @@ public:
             val = false;
           }
           else {
-            n = Rewriter::rewrite(store[1].eqNode(index));
+            n = Rewriter::rewrite(mkEqNode(store[1], index));
             if (n.getKind() != kind::CONST_BOOLEAN) {
               break;
             }
@@ -301,7 +305,7 @@ public:
             val = false;
           }
           else {
-            Node eqRewritten = Rewriter::rewrite(store[1].eqNode(index));
+            Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index));
             if (eqRewritten.getKind() != kind::CONST_BOOLEAN) {
               Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << node << std::endl;
               return RewriteResponse(REWRITE_DONE, node);
@@ -340,7 +344,7 @@ public:
                 val = false;
               }
               else {
-                n = Rewriter::rewrite(store[1].eqNode(index));
+                n = Rewriter::rewrite(mkEqNode(store[1], index));
                 if (n.getKind() != kind::CONST_BOOLEAN) {
                   break;
                 }
@@ -416,7 +420,7 @@ public:
             val = false;
           }
           else {
-            n = Rewriter::rewrite(store[1].eqNode(index));
+            n = Rewriter::rewrite(mkEqNode(store[1], index));
             if (n.getKind() != kind::CONST_BOOLEAN) {
               break;
             }
@@ -466,7 +470,7 @@ public:
             val = false;
           }
           else {
-            Node eqRewritten = Rewriter::rewrite(store[1].eqNode(index));
+            Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index));
             if (eqRewritten.getKind() != kind::CONST_BOOLEAN) {
               break;
             }
-- 
2.30.2