From 227ae68748524ec205a93ec959d770bccebcf4fe Mon Sep 17 00:00:00 2001
From: Andres Notzli <andres.noetzli@gmail.com>
Date: Tue, 9 May 2017 12:31:22 -0700
Subject: update

---
 src/theory/arrays/arrays_post.h | 60 ++++++++++++++++-------------------------
 1 file changed, 23 insertions(+), 37 deletions(-)

diff --git a/src/theory/arrays/arrays_post.h b/src/theory/arrays/arrays_post.h
index 3e29d77f4..2d3bdaffe 100644
--- a/src/theory/arrays/arrays_post.h
+++ b/src/theory/arrays/arrays_post.h
@@ -134,38 +134,6 @@ inline RewriteResponse arrays_post_rewrite7(TNode node, RewriteProof *proof) {
 
 template <bool Proof>
 inline RewriteResponse arrays_post_rewrite8(TNode node, RewriteProof *proof) {
-  NodeManager *nm = NodeManager::currentNM();
-  if ((node).getKind() == kind::SELECT) {
-    if (((node[0]).getKind() == kind::STORE) &&
-        (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) ==
-         nm->mkConst(false))) {
-      if (Proof) {
-        proof->registerRewrite(arrays_post_SELECT_STORE_DIFF_I_J);
-      };
-      Node rewritten_node = nm->mkNode(kind::SELECT, node[0][0], node[1]);
-      return arrays_post_rewrite7<Proof>(rewritten_node, proof);
-    };
-    if (((node[0]).getKind() == kind::STORE) &&
-        ((((node[0][1]).isConst()) && ((node[1]).isConst())) &&
-         ((node[0][1] != node[1])))) {
-      if (Proof) {
-        proof->registerRewrite(arrays_post_SELECT_STORE_DIFF_CONSTS);
-      };
-      Node rewritten_node = nm->mkNode(kind::SELECT, node[0][0], node[1]);
-      return arrays_post_rewrite7<Proof>(rewritten_node, proof);
-    }
-  };
-  return arrays_post_rewrite6<Proof>(node, proof);
-}
-
-template <bool Proof>
-inline RewriteResponse arrays_post_rewrite9(TNode node, RewriteProof *proof) {
-  NodeManager *nm = NodeManager::currentNM();
-  return RewriteResponse(REWRITE_DONE, node);
-}
-
-template <bool Proof>
-inline RewriteResponse arrays_post_rewrite10(TNode node, RewriteProof *proof) {
   NodeManager *nm = NodeManager::currentNM();
   if ((node).getKind() == kind::SELECT) {
     if (((node[0]).getKind() == kind::STORE) && (true) &&
@@ -174,7 +142,7 @@ inline RewriteResponse arrays_post_rewrite10(TNode node, RewriteProof *proof) {
         proof->registerRewrite(arrays_post_SELECT_STORE_I_I);
       };
       Node rewritten_node = node[0][2];
-      return arrays_post_rewrite9<Proof>(rewritten_node, proof);
+      return arrays_post_rewrite7<Proof>(rewritten_node, proof);
     };
     if (((node[0]).getKind() == kind::STORE) &&
         (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) ==
@@ -183,7 +151,7 @@ inline RewriteResponse arrays_post_rewrite10(TNode node, RewriteProof *proof) {
         proof->registerRewrite(arrays_post_SELECT_STORE_I_J);
       };
       Node rewritten_node = node[0][2];
-      return arrays_post_rewrite9<Proof>(rewritten_node, proof);
+      return arrays_post_rewrite7<Proof>(rewritten_node, proof);
     };
     if (((node[0]).getKind() == kind::STORE_ALL) && (true)) {
       if (Proof) {
@@ -191,16 +159,34 @@ inline RewriteResponse arrays_post_rewrite10(TNode node, RewriteProof *proof) {
       };
       Node rewritten_node =
           Node::fromExpr(node[0].getConst<ArrayStoreAll>().getExpr());
-      return arrays_post_rewrite9<Proof>(rewritten_node, proof);
+      return arrays_post_rewrite7<Proof>(rewritten_node, proof);
+    };
+    if (((node[0]).getKind() == kind::STORE) &&
+        (Rewriter::rewrite(nm->mkNode(kind::EQUAL, node[0][1], node[1])) ==
+         nm->mkConst(false))) {
+      if (Proof) {
+        proof->registerRewrite(arrays_post_SELECT_STORE_DIFF_I_J);
+      };
+      Node rewritten_node = nm->mkNode(kind::SELECT, node[0][0], node[1]);
+      return arrays_post_rewrite7<Proof>(rewritten_node, proof);
+    };
+    if (((node[0]).getKind() == kind::STORE) &&
+        ((((node[0][1]).isConst()) && ((node[1]).isConst())) &&
+         ((node[0][1] != node[1])))) {
+      if (Proof) {
+        proof->registerRewrite(arrays_post_SELECT_STORE_DIFF_CONSTS);
+      };
+      Node rewritten_node = nm->mkNode(kind::SELECT, node[0][0], node[1]);
+      return arrays_post_rewrite7<Proof>(rewritten_node, proof);
     }
   };
-  return arrays_post_rewrite8<Proof>(node, proof);
+  return arrays_post_rewrite6<Proof>(node, proof);
 }
 
 template <bool Proof>
 inline RewriteResponse arrays_post_applyRules(TNode node, RewriteProof *proof) {
 
-  return arrays_post_rewrite10<Proof>(node, proof);
+  return arrays_post_rewrite8<Proof>(node, proof);
 }
 
 inline void arrays_post_printProof(bool use_cache, TheoryProofEngine *tp,
-- 
cgit v1.2.3