Move array rewriter functions to source filearr_rewriter_refactor

Previously, most of the code for the theory of arrays rewriter was in
the header file, slowing down compilation. This commit moves the
functions to the body, replaces the ifdef guard in the header file with
a `pragma once` and reformats the code using clang-format. Note, this
commit removes an inline qualifier from the preRewrite function but
given the size of the function, this should not impact performance.

2 files changed, 483 insertions, 473 deletions

diff --git a/src/theory/arrays/theory_arrays_rewriter.cpp b/src/theory/arrays/theory_arrays_rewriter.cpp
index f1cf1d320..3ab90231d 100644
--- a/src/theory/arrays/theory_arrays_rewriter.cpp
+++ b/src/theory/arrays/theory_arrays_rewriter.cpp
@@ -15,20 +15,24 @@
  ** \todo document this file
  **/
 
-#include "expr/attribute.h"
 #include "theory/arrays/theory_arrays_rewriter.h"
 
+#include "expr/attribute.h"
+#include "theory/type_enumerator.h"
+
 namespace CVC4 {
 namespace theory {
 namespace arrays {
 
 namespace attr {
-  struct ArrayConstantMostFrequentValueTag { };
-  struct ArrayConstantMostFrequentValueCountTag { };
-}/* CVC4::theory::arrays::attr namespace */
+struct ArrayConstantMostFrequentValueTag {};
+struct ArrayConstantMostFrequentValueCountTag {};
+} /* CVC4::theory::arrays::attr namespace */
 
-typedef expr::Attribute<attr::ArrayConstantMostFrequentValueCountTag, uint64_t> ArrayConstantMostFrequentValueCountAttr;
-typedef expr::Attribute<attr::ArrayConstantMostFrequentValueTag, Node> ArrayConstantMostFrequentValueAttr;
+typedef expr::Attribute<attr::ArrayConstantMostFrequentValueCountTag, uint64_t>
+    ArrayConstantMostFrequentValueCountAttr;
+typedef expr::Attribute<attr::ArrayConstantMostFrequentValueTag, Node>
+    ArrayConstantMostFrequentValueAttr;
 
 Node getMostFrequentValue(TNode store) {
   return store.getAttribute(ArrayConstantMostFrequentValueAttr());
@@ -44,6 +48,464 @@ void setMostFrequentValueCount(TNode store, uint64_t count) {
   return store.setAttribute(ArrayConstantMostFrequentValueCountAttr(), count);
 }
 
-}/* CVC4::theory::arrays namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+Node TheoryArraysRewriter::normalizeConstant(TNode node,
+                                             Cardinality indexCard) {
+  TNode store = node[0];
+  TNode index = node[1];
+  TNode value = node[2];
+
+  std::vector<TNode> indices;
+  std::vector<TNode> elements;
+
+  // Normal form for nested stores is just ordering by index - but also need
+  // to check if we are writing to default value
+
+  // Go through nested stores looking for where to insert index
+  // Also check whether we are replacing an existing store
+  TNode replacedValue;
+  unsigned depth = 1;
+  unsigned valCount = 1;
+  while (store.getKind() == kind::STORE) {
+    if (index == store[1]) {
+      replacedValue = store[2];
+      store = store[0];
+      break;
+    } else if (!(index < store[1])) {
+      break;
+    }
+    if (value == store[2]) {
+      valCount += 1;
+    }
+    depth += 1;
+    indices.push_back(store[1]);
+    elements.push_back(store[2]);
+    store = store[0];
+  }
+  Node n = store;
+
+  // Get the default value at the bottom of the nested stores
+  while (store.getKind() == kind::STORE) {
+    if (value == store[2]) {
+      valCount += 1;
+    }
+    depth += 1;
+    store = store[0];
+  }
+  Assert(store.getKind() == kind::STORE_ALL);
+  ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
+  Node defaultValue = Node::fromExpr(storeAll.getExpr());
+  NodeManager* nm = NodeManager::currentNM();
+
+  // Check if we are writing to default value - if so the store
+  // to index can be ignored
+  if (value == defaultValue) {
+    if (replacedValue.isNull()) {
+      // Quick exit - if writing to default value and nothing was
+      // replaced, we can just return node[0]
+      return node[0];
+    }
+    // else rebuild the store without the replaced write and then exit
+  } else {
+    n = nm->mkNode(kind::STORE, n, index, value);
+  }
+
+  // Build the rest of the store after inserting/deleting
+  while (!indices.empty()) {
+    n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
+    indices.pop_back();
+    elements.pop_back();
+  }
+
+  // Ready to exit if write was to the default value (see previous comment)
+  if (value == defaultValue) {
+    return n;
+  }
+
+  if (indexCard.isInfinite()) {
+    return n;
+  }
+
+  // When index sort is finite, we have to check whether there is any value
+  // that is written to more than the default value.  If so, it must become
+  // the new default value
+
+  TNode mostFrequentValue;
+  unsigned mostFrequentValueCount = 0;
+  store = node[0];
+  if (store.getKind() == kind::STORE) {
+    mostFrequentValue = getMostFrequentValue(store);
+    mostFrequentValueCount = getMostFrequentValueCount(store);
+  }
+
+  // Compute the most frequently written value for n
+  if (valCount > mostFrequentValueCount ||
+      (valCount == mostFrequentValueCount && value < mostFrequentValue)) {
+    mostFrequentValue = value;
+    mostFrequentValueCount = valCount;
+  }
+
+  // Need to make sure the default value count is larger, or the same and the
+  // default value is expression-order-less-than nextValue
+  Cardinality::CardinalityComparison compare =
+      indexCard.compare(mostFrequentValueCount + depth);
+  Assert(compare != Cardinality::UNKNOWN);
+  if (compare == Cardinality::GREATER ||
+      (compare == Cardinality::EQUAL && (defaultValue < mostFrequentValue))) {
+    return n;
+  }
+
+  // Bad case: have to recompute value counts and/or possibly switch out
+  // default value
+  store = n;
+  std::hash_set<TNode, TNodeHashFunction> indexSet;
+  std::hash_map<TNode, unsigned, TNodeHashFunction> elementsMap;
+  std::hash_map<TNode, unsigned, TNodeHashFunction>::iterator it;
+  unsigned count;
+  unsigned max = 0;
+  TNode maxValue;
+  while (store.getKind() == kind::STORE) {
+    indices.push_back(store[1]);
+    indexSet.insert(store[1]);
+    elements.push_back(store[2]);
+    it = elementsMap.find(store[2]);
+    if (it != elementsMap.end()) {
+      (*it).second = (*it).second + 1;
+      count = (*it).second;
+    } else {
+      elementsMap[store[2]] = 1;
+      count = 1;
+    }
+    if (count > max || (count == max && store[2] < maxValue)) {
+      max = count;
+      maxValue = store[2];
+    }
+    store = store[0];
+  }
+
+  Assert(depth == indices.size());
+  compare = indexCard.compare(max + depth);
+  Assert(compare != Cardinality::UNKNOWN);
+  if (compare == Cardinality::GREATER ||
+      (compare == Cardinality::EQUAL && (defaultValue < maxValue))) {
+    Assert(!replacedValue.isNull() && mostFrequentValue == replacedValue);
+    return n;
+  }
+
+  // Out of luck: have to swap out default value
+
+  // Enumerate values from index type into newIndices and sort
+  std::vector<Node> newIndices;
+  TypeEnumerator te(index.getType());
+  bool needToSort = false;
+  unsigned numTe = 0;
+  while (!te.isFinished() &&
+         (!indexCard.isFinite() ||
+          numTe < indexCard.getFiniteCardinality().toUnsignedInt())) {
+    if (indexSet.find(*te) == indexSet.end()) {
+      if (!newIndices.empty() && (!(newIndices.back() < (*te)))) {
+        needToSort = true;
+      }
+      newIndices.push_back(*te);
+    }
+    ++numTe;
+    ++te;
+  }
+  Assert(indexCard.compare(newIndices.size() + depth) == Cardinality::EQUAL);
+  if (needToSort) {
+    std::sort(newIndices.begin(), newIndices.end());
+  }
+
+  n = nm->mkConst(ArrayStoreAll(node.getType().toType(), maxValue.toExpr()));
+  std::vector<Node>::iterator itNew = newIndices.begin(),
+                              it_end = newIndices.end();
+  while (itNew != it_end || !indices.empty()) {
+    if (itNew != it_end && (indices.empty() || (*itNew) < indices.back())) {
+      n = nm->mkNode(kind::STORE, n, (*itNew), defaultValue);
+      ++itNew;
+    } else if (itNew == it_end || indices.back() < (*itNew)) {
+      if (elements.back() != maxValue) {
+        n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
+      }
+      indices.pop_back();
+      elements.pop_back();
+    }
+  }
+  return n;
+}
+
+RewriteResponse TheoryArraysRewriter::postRewrite(TNode node) {
+  Trace("arrays-postrewrite") << "Arrays::postRewrite start " << node
+                              << std::endl;
+  switch (node.getKind()) {
+    case kind::SELECT: {
+      TNode store = node[0];
+      TNode index = node[1];
+      Node n;
+      bool val;
+      while (store.getKind() == kind::STORE) {
+        if (index == store[1]) {
+          val = true;
+        } else if (index.isConst() && store[1].isConst()) {
+          val = false;
+        } else {
+          n = Rewriter::rewrite(mkEqNode(store[1], index));
+          if (n.getKind() != kind::CONST_BOOLEAN) {
+            break;
+          }
+          val = n.getConst<bool>();
+        }
+        if (val) {
+          // select(store(a,i,v),j) = v if i = j
+          Trace("arrays-postrewrite") << "Arrays::postRewrite returning "
+                                      << store[2] << std::endl;
+          return RewriteResponse(REWRITE_DONE, store[2]);
+        }
+        // select(store(a,i,v),j) = select(a,j) if i /= j
+        store = store[0];
+      }
+      if (store.getKind() == kind::STORE_ALL) {
+        // select(store_all(v),i) = v
+        ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
+        n = Node::fromExpr(storeAll.getExpr());
+        Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n
+                                    << std::endl;
+        Assert(n.isConst());
+        return RewriteResponse(REWRITE_DONE, n);
+      } else if (store != node[0]) {
+        n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index);
+        Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n
+                                    << std::endl;
+        return RewriteResponse(REWRITE_DONE, n);
+      }
+      break;
+    }
+    case kind::STORE: {
+      TNode store = node[0];
+      TNode value = node[2];
+      // store(a,i,select(a,i)) = a
+      if (value.getKind() == kind::SELECT && value[0] == store &&
+          value[1] == node[1]) {
+        Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << store
+                                    << std::endl;
+        return RewriteResponse(REWRITE_DONE, store);
+      }
+      TNode index = node[1];
+      if (store.isConst() && index.isConst() && value.isConst()) {
+        // normalize constant
+        Node n = normalizeConstant(node);
+        Assert(n.isConst());
+        Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n
+                                    << std::endl;
+        return RewriteResponse(REWRITE_DONE, n);
+      }
+      if (store.getKind() == kind::STORE) {
+        // store(store(a,i,v),j,w)
+        bool val;
+        if (index == store[1]) {
+          val = true;
+        } else if (index.isConst() && store[1].isConst()) {
+          val = false;
+        } else {
+          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);
+          }
+          val = eqRewritten.getConst<bool>();
+        }
+        NodeManager* nm = NodeManager::currentNM();
+        if (val) {
+          // store(store(a,i,v),i,w) = store(a,i,w)
+          Node result;
+          if (value.getKind() == kind::SELECT && value[0] == store[0] &&
+              value[1] == index) {
+            result = store[0];
+          } else {
+            result = nm->mkNode(kind::STORE, store[0], index, value);
+          }
+          Trace("arrays-postrewrite") << "Arrays::postRewrite returning "
+                                      << result << std::endl;
+          return RewriteResponse(REWRITE_DONE, result);
+        } else if (index < store[1]) {
+          // store(store(a,i,v),j,w) = store(store(a,j,w),i,v)
+          //    IF i != j and j comes before i in the ordering
+          std::vector<TNode> indices;
+          std::vector<TNode> elements;
+          indices.push_back(store[1]);
+          elements.push_back(store[2]);
+          store = store[0];
+          Node n;
+          while (store.getKind() == kind::STORE) {
+            if (index == store[1]) {
+              val = true;
+            } else if (index.isConst() && store[1].isConst()) {
+              val = false;
+            } else {
+              n = Rewriter::rewrite(mkEqNode(store[1], index));
+              if (n.getKind() != kind::CONST_BOOLEAN) {
+                break;
+              }
+              val = n.getConst<bool>();
+            }
+            if (val) {
+              store = store[0];
+              break;
+            } else if (!(index < store[1])) {
+              break;
+            }
+            indices.push_back(store[1]);
+            elements.push_back(store[2]);
+            store = store[0];
+          }
+          if (value.getKind() == kind::SELECT && value[0] == store &&
+              value[1] == index) {
+            n = store;
+          } else {
+            n = nm->mkNode(kind::STORE, store, index, value);
+          }
+          while (!indices.empty()) {
+            n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
+            indices.pop_back();
+            elements.pop_back();
+          }
+          Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n
+                                      << std::endl;
+          return RewriteResponse(REWRITE_DONE, n);
+        }
+      }
+      break;
+    }
+    case kind::EQUAL:
+    case kind::IFF: {
+      if (node[0] == node[1]) {
+        Trace("arrays-postrewrite") << "Arrays::postRewrite returning true"
+                                    << std::endl;
+        return RewriteResponse(REWRITE_DONE,
+                               NodeManager::currentNM()->mkConst(true));
+      } else if (node[0].isConst() && node[1].isConst()) {
+        Trace("arrays-postrewrite") << "Arrays::postRewrite returning false"
+                                    << std::endl;
+        return RewriteResponse(REWRITE_DONE,
+                               NodeManager::currentNM()->mkConst(false));
+      }
+      if (node[0] > node[1]) {
+        Node newNode =
+            NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
+        Trace("arrays-postrewrite") << "Arrays::postRewrite returning "
+                                    << newNode << std::endl;
+        return RewriteResponse(REWRITE_DONE, newNode);
+      }
+      break;
+    }
+    default:
+      break;
+  }
+  Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << node
+                              << std::endl;
+  return RewriteResponse(REWRITE_DONE, node);
+}
+
+RewriteResponse TheoryArraysRewriter::preRewrite(TNode node) {
+  Trace("arrays-prerewrite") << "Arrays::preRewrite start " << node
+                             << std::endl;
+  switch (node.getKind()) {
+    case kind::SELECT: {
+      TNode store = node[0];
+      TNode index = node[1];
+      Node n;
+      bool val;
+      while (store.getKind() == kind::STORE) {
+        if (index == store[1]) {
+          val = true;
+        } else if (index.isConst() && store[1].isConst()) {
+          val = false;
+        } else {
+          n = Rewriter::rewrite(mkEqNode(store[1], index));
+          if (n.getKind() != kind::CONST_BOOLEAN) {
+            break;
+          }
+          val = n.getConst<bool>();
+        }
+        if (val) {
+          // select(store(a,i,v),j) = v if i = j
+          Trace("arrays-prerewrite") << "Arrays::preRewrite returning "
+                                     << store[2] << std::endl;
+          return RewriteResponse(REWRITE_AGAIN, store[2]);
+        }
+        // select(store(a,i,v),j) = select(a,j) if i /= j
+        store = store[0];
+      }
+      if (store.getKind() == kind::STORE_ALL) {
+        // select(store_all(v),i) = v
+        ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
+        n = Node::fromExpr(storeAll.getExpr());
+        Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << n
+                                   << std::endl;
+        Assert(n.isConst());
+        return RewriteResponse(REWRITE_DONE, n);
+      } else if (store != node[0]) {
+        n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index);
+        Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << n
+                                   << std::endl;
+        return RewriteResponse(REWRITE_DONE, n);
+      }
+      break;
+    }
+    case kind::STORE: {
+      TNode store = node[0];
+      TNode value = node[2];
+      // store(a,i,select(a,i)) = a
+      if (value.getKind() == kind::SELECT && value[0] == store &&
+          value[1] == node[1]) {
+        Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << store
+                                   << std::endl;
+        return RewriteResponse(REWRITE_AGAIN, store);
+      }
+      if (store.getKind() == kind::STORE) {
+        // store(store(a,i,v),j,w)
+        TNode index = node[1];
+        bool val;
+        if (index == store[1]) {
+          val = true;
+        } else if (index.isConst() && store[1].isConst()) {
+          val = false;
+        } else {
+          Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index));
+          if (eqRewritten.getKind() != kind::CONST_BOOLEAN) {
+            break;
+          }
+          val = eqRewritten.getConst<bool>();
+        }
+        NodeManager* nm = NodeManager::currentNM();
+        if (val) {
+          // store(store(a,i,v),i,w) = store(a,i,w)
+          Node newNode = nm->mkNode(kind::STORE, store[0], index, value);
+          Trace("arrays-prerewrite") << "Arrays::preRewrite returning "
+                                     << newNode << std::endl;
+          return RewriteResponse(REWRITE_DONE, newNode);
+        }
+      }
+      break;
+    }
+    case kind::EQUAL:
+    case kind::IFF: {
+      if (node[0] == node[1]) {
+        Trace("arrays-prerewrite") << "Arrays::preRewrite returning true"
+                                   << std::endl;
+        return RewriteResponse(REWRITE_DONE,
+                               NodeManager::currentNM()->mkConst(true));
+      }
+      break;
+    }
+    default:
+      break;
+  }
+
+  Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << node
+                             << std::endl;
+  return RewriteResponse(REWRITE_DONE, node);
+}
+} /* CVC4::theory::arrays namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index de10a861b..5a68d21a6 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -17,11 +17,9 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
-#define __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H
+#pragma once
 
 #include "theory/rewriter.h"
-#include "theory/type_enumerator.h"
 
 namespace CVC4 {
 namespace theory {
@@ -37,474 +35,24 @@ static inline Node mkEqNode(Node a, Node b) {
 }
 
 class TheoryArraysRewriter {
+ private:
   static Node normalizeConstant(TNode node) {
     return normalizeConstant(node, node[1].getType().getCardinality());
   }
-public:
-  //this function is called by printers when using the option "--model-u-dt-enum"
-  static Node normalizeConstant(TNode node, Cardinality indexCard) {
-    TNode store = node[0];
-    TNode index = node[1];
-    TNode value = node[2];
 
-    std::vector<TNode> indices;
-    std::vector<TNode> elements;
+ public:
+  // this function is called by printers when using the option
+  // "--model-u-dt-enum"
+  static Node normalizeConstant(TNode node, Cardinality indexCard);
 
-    // Normal form for nested stores is just ordering by index - but also need
-    // to check if we are writing to default value
-
-    // Go through nested stores looking for where to insert index
-    // Also check whether we are replacing an existing store
-    TNode replacedValue;
-    unsigned depth = 1;
-    unsigned valCount = 1;
-    while (store.getKind() == kind::STORE) {
-      if (index == store[1]) {
-        replacedValue = store[2];
-        store = store[0];
-        break;
-      }
-      else if (!(index < store[1])) {
-        break;
-      }
-      if (value == store[2]) {
-        valCount += 1;
-      }
-      depth += 1;
-      indices.push_back(store[1]);
-      elements.push_back(store[2]);
-      store = store[0];
-    }
-    Node n = store;
-
-    // Get the default value at the bottom of the nested stores
-    while (store.getKind() == kind::STORE) {
-      if (value == store[2]) {
-        valCount += 1;
-      }
-      depth += 1;
-      store = store[0];
-    }
-    Assert(store.getKind() == kind::STORE_ALL);
-    ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
-    Node defaultValue = Node::fromExpr(storeAll.getExpr());
-    NodeManager* nm = NodeManager::currentNM();
-
-    // Check if we are writing to default value - if so the store
-    // to index can be ignored
-    if (value == defaultValue) {
-      if (replacedValue.isNull()) {
-        // Quick exit - if writing to default value and nothing was
-        // replaced, we can just return node[0]
-        return node[0];
-      }
-      // else rebuild the store without the replaced write and then exit
-    }
-    else {
-      n = nm->mkNode(kind::STORE, n, index, value);
-    }
-
-    // Build the rest of the store after inserting/deleting
-    while (!indices.empty()) {
-      n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
-      indices.pop_back();
-      elements.pop_back();
-    }
-
-    // Ready to exit if write was to the default value (see previous comment)
-    if (value == defaultValue) {
-      return n;
-    }
-
-    if (indexCard.isInfinite()) {
-      return n;
-    }
-
-    // When index sort is finite, we have to check whether there is any value
-    // that is written to more than the default value.  If so, it must become
-    // the new default value
-
-    TNode mostFrequentValue;
-    unsigned mostFrequentValueCount = 0;
-    store = node[0];
-    if (store.getKind() == kind::STORE) {
-      mostFrequentValue = getMostFrequentValue(store);
-      mostFrequentValueCount = getMostFrequentValueCount(store);
-    }
-
-    // Compute the most frequently written value for n
-    if (valCount > mostFrequentValueCount ||
-        (valCount == mostFrequentValueCount && value < mostFrequentValue)) {
-      mostFrequentValue = value;
-      mostFrequentValueCount = valCount;
-    }
-
-    // Need to make sure the default value count is larger, or the same and the default value is expression-order-less-than nextValue
-    Cardinality::CardinalityComparison compare = indexCard.compare(mostFrequentValueCount + depth);
-    Assert(compare != Cardinality::UNKNOWN);
-    if (compare == Cardinality::GREATER ||
-        (compare == Cardinality::EQUAL && (defaultValue < mostFrequentValue))) {
-      return n;
-    }
-
-    // Bad case: have to recompute value counts and/or possibly switch out
-    // default value
-    store = n;
-    std::hash_set<TNode, TNodeHashFunction> indexSet;
-    std::hash_map<TNode, unsigned, TNodeHashFunction> elementsMap;
-    std::hash_map<TNode, unsigned, TNodeHashFunction>::iterator it;
-    unsigned count;
-    unsigned max = 0;
-    TNode maxValue;
-    while (store.getKind() == kind::STORE) {
-      indices.push_back(store[1]);
-      indexSet.insert(store[1]);
-      elements.push_back(store[2]);
-      it = elementsMap.find(store[2]);
-      if (it != elementsMap.end()) {
-        (*it).second = (*it).second + 1;
-        count = (*it).second;
-      }
-      else {
-        elementsMap[store[2]] = 1;
-        count = 1;
-      }
-      if (count > max ||
-          (count == max && store[2] < maxValue)) {
-        max = count;
-        maxValue = store[2];
-      }
-      store = store[0];
-    }
-
-    Assert(depth == indices.size());
-    compare = indexCard.compare(max + depth);
-    Assert(compare != Cardinality::UNKNOWN);
-    if (compare == Cardinality::GREATER ||
-        (compare == Cardinality::EQUAL && (defaultValue < maxValue))) {
-      Assert(!replacedValue.isNull() && mostFrequentValue == replacedValue);
-      return n;
-    }
-
-    // Out of luck: have to swap out default value
-
-    // Enumerate values from index type into newIndices and sort
-    std::vector<Node> newIndices;
-    TypeEnumerator te(index.getType());
-    bool needToSort = false;
-    unsigned numTe = 0;
-    while (!te.isFinished() && (!indexCard.isFinite() || numTe<indexCard.getFiniteCardinality().toUnsignedInt())) {
-      if (indexSet.find(*te) == indexSet.end()) {
-        if (!newIndices.empty() && (!(newIndices.back() < (*te)))) {
-          needToSort = true;
-        }
-        newIndices.push_back(*te);
-      }
-      ++numTe;
-      ++te;
-    }
-    Assert(indexCard.compare(newIndices.size() + depth) == Cardinality::EQUAL);
-    if (needToSort) {
-      std::sort(newIndices.begin(), newIndices.end());
-    }
-
-    n = nm->mkConst(ArrayStoreAll(node.getType().toType(), maxValue.toExpr()));
-    std::vector<Node>::iterator itNew = newIndices.begin(), it_end = newIndices.end();
-    while (itNew != it_end || !indices.empty()) {
-      if (itNew != it_end && (indices.empty() || (*itNew) < indices.back())) {
-        n = nm->mkNode(kind::STORE, n, (*itNew), defaultValue);
-        ++itNew;
-      }
-      else if (itNew == it_end || indices.back() < (*itNew)) {
-        if (elements.back() != maxValue) {
-          n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
-        }
-        indices.pop_back();
-        elements.pop_back();
-      }
-    }
-    return n;
-  }
-
-public:
-
-  static RewriteResponse postRewrite(TNode node) {
-    Trace("arrays-postrewrite") << "Arrays::postRewrite start " << node << std::endl;
-    switch (node.getKind()) {
-      case kind::SELECT: {
-        TNode store = node[0];
-        TNode index = node[1];
-        Node n;
-        bool val;
-        while (store.getKind() == kind::STORE) {
-          if (index == store[1]) {
-            val = true;
-          }
-          else if (index.isConst() && store[1].isConst()) {
-            val = false;
-          }
-          else {
-            n = Rewriter::rewrite(mkEqNode(store[1], index));
-            if (n.getKind() != kind::CONST_BOOLEAN) {
-              break;
-            }
-            val = n.getConst<bool>();
-          }
-          if (val) {
-            // select(store(a,i,v),j) = v if i = j
-            Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << store[2] << std::endl;
-            return RewriteResponse(REWRITE_DONE, store[2]);
-          }
-          // select(store(a,i,v),j) = select(a,j) if i /= j
-          store = store[0];
-        }
-        if (store.getKind() == kind::STORE_ALL) {
-          // select(store_all(v),i) = v
-          ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
-          n = Node::fromExpr(storeAll.getExpr());
-          Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl;
-          Assert(n.isConst());
-          return RewriteResponse(REWRITE_DONE, n);
-        }
-        else if (store != node[0]) {
-          n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index);
-          Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl;
-          return RewriteResponse(REWRITE_DONE, n);
-        }
-        break;
-      }
-      case kind::STORE: {
-        TNode store = node[0];
-        TNode value = node[2];
-        // store(a,i,select(a,i)) = a
-        if (value.getKind() == kind::SELECT &&
-            value[0] == store &&
-            value[1] == node[1]) {
-          Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << store << std::endl;
-          return RewriteResponse(REWRITE_DONE, store);
-        }
-        TNode index = node[1];
-        if (store.isConst() && index.isConst() && value.isConst()) {
-          // normalize constant
-          Node n = normalizeConstant(node);
-          Assert(n.isConst());
-          Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl;
-          return RewriteResponse(REWRITE_DONE, n);
-        }
-        if (store.getKind() == kind::STORE) {
-          // store(store(a,i,v),j,w)
-          bool val;
-          if (index == store[1]) {
-            val = true;
-          }
-          else if (index.isConst() && store[1].isConst()) {
-            val = false;
-          }
-          else {
-            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);
-            }
-            val = eqRewritten.getConst<bool>();
-          }
-          NodeManager* nm = NodeManager::currentNM();
-          if (val) {
-            // store(store(a,i,v),i,w) = store(a,i,w)
-            Node result;
-            if (value.getKind() == kind::SELECT &&
-                value[0] == store[0] &&
-                value[1] == index) {
-              result = store[0];
-            }
-            else {
-              result = nm->mkNode(kind::STORE, store[0], index, value);
-            }
-            Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << result << std::endl;
-            return RewriteResponse(REWRITE_DONE, result);
-          }
-          else if (index < store[1]) {
-            // store(store(a,i,v),j,w) = store(store(a,j,w),i,v)
-            //    IF i != j and j comes before i in the ordering
-            std::vector<TNode> indices;
-            std::vector<TNode> elements;
-            indices.push_back(store[1]);
-            elements.push_back(store[2]);
-            store = store[0];
-            Node n;
-            while (store.getKind() == kind::STORE) {
-              if (index == store[1]) {
-                val = true;
-              }
-              else if (index.isConst() && store[1].isConst()) {
-                val = false;
-              }
-              else {
-                n = Rewriter::rewrite(mkEqNode(store[1], index));
-                if (n.getKind() != kind::CONST_BOOLEAN) {
-                  break;
-                }
-                val = n.getConst<bool>();
-              }
-              if (val) {
-                store = store[0];
-                break;
-              }
-              else if (!(index < store[1])) {
-                break;
-              }
-              indices.push_back(store[1]);
-              elements.push_back(store[2]);
-              store = store[0];
-            }
-            if (value.getKind() == kind::SELECT &&
-                value[0] == store &&
-                value[1] == index) {
-              n = store;
-            }
-            else {
-              n = nm->mkNode(kind::STORE, store, index, value);
-            }
-            while (!indices.empty()) {
-              n = nm->mkNode(kind::STORE, n, indices.back(), elements.back());
-              indices.pop_back();
-              elements.pop_back();
-            }
-            Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << n << std::endl;
-            return RewriteResponse(REWRITE_DONE, n);
-          }
-        }
-        break;
-      }
-      case kind::EQUAL:
-      case kind::IFF: {
-        if(node[0] == node[1]) {
-          Trace("arrays-postrewrite") << "Arrays::postRewrite returning true" << std::endl;
-          return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
-        }
-        else if (node[0].isConst() && node[1].isConst()) {
-          Trace("arrays-postrewrite") << "Arrays::postRewrite returning false" << std::endl;
-          return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(false));
-        }
-        if (node[0] > node[1]) {
-          Node newNode = NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
-          Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << newNode << std::endl;
-          return RewriteResponse(REWRITE_DONE, newNode);
-        }
-        break;
-      }
-      default:
-        break;
-    }
-    Trace("arrays-postrewrite") << "Arrays::postRewrite returning " << node << std::endl;
-    return RewriteResponse(REWRITE_DONE, node);
-  }
-
-  static inline RewriteResponse preRewrite(TNode node) {
-    Trace("arrays-prerewrite") << "Arrays::preRewrite start " << node << std::endl;
-    switch (node.getKind()) {
-      case kind::SELECT: {
-        TNode store = node[0];
-        TNode index = node[1];
-        Node n;
-        bool val;
-        while (store.getKind() == kind::STORE) {
-          if (index == store[1]) {
-            val = true;
-          }
-          else if (index.isConst() && store[1].isConst()) {
-            val = false;
-          }
-          else {
-            n = Rewriter::rewrite(mkEqNode(store[1], index));
-            if (n.getKind() != kind::CONST_BOOLEAN) {
-              break;
-            }
-            val = n.getConst<bool>();
-          }
-          if (val) {
-            // select(store(a,i,v),j) = v if i = j
-            Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << store[2] << std::endl;
-            return RewriteResponse(REWRITE_AGAIN, store[2]);
-          }
-          // select(store(a,i,v),j) = select(a,j) if i /= j
-          store = store[0];
-        }
-        if (store.getKind() == kind::STORE_ALL) {
-          // select(store_all(v),i) = v
-          ArrayStoreAll storeAll = store.getConst<ArrayStoreAll>();
-          n = Node::fromExpr(storeAll.getExpr());
-          Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << n << std::endl;
-          Assert(n.isConst());
-          return RewriteResponse(REWRITE_DONE, n);
-        }
-        else if (store != node[0]) {
-          n = NodeManager::currentNM()->mkNode(kind::SELECT, store, index);
-          Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << n << std::endl;
-          return RewriteResponse(REWRITE_DONE, n);
-        }
-        break;
-      }
-      case kind::STORE: {
-        TNode store = node[0];
-        TNode value = node[2];
-        // store(a,i,select(a,i)) = a
-        if (value.getKind() == kind::SELECT &&
-            value[0] == store &&
-            value[1] == node[1]) {
-          Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << store << std::endl;
-          return RewriteResponse(REWRITE_AGAIN, store);
-        }
-        if (store.getKind() == kind::STORE) {
-          // store(store(a,i,v),j,w)
-          TNode index = node[1];
-          bool val;
-          if (index == store[1]) {
-            val = true;
-          }
-          else if (index.isConst() && store[1].isConst()) {
-            val = false;
-          }
-          else {
-            Node eqRewritten = Rewriter::rewrite(mkEqNode(store[1], index));
-            if (eqRewritten.getKind() != kind::CONST_BOOLEAN) {
-              break;
-            }
-            val = eqRewritten.getConst<bool>();
-          }
-          NodeManager* nm = NodeManager::currentNM();
-          if (val) {
-            // store(store(a,i,v),i,w) = store(a,i,w)
-            Node newNode = nm->mkNode(kind::STORE, store[0], index, value);
-            Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << newNode << std::endl;
-            return RewriteResponse(REWRITE_DONE, newNode);
-          }
-        }
-        break;
-      }
-      case kind::EQUAL:
-      case kind::IFF: {
-        if(node[0] == node[1]) {
-          Trace("arrays-prerewrite") << "Arrays::preRewrite returning true" << std::endl;
-          return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
-        }
-        break;
-      }
-      default:
-        break;
-    }
-
-    Trace("arrays-prerewrite") << "Arrays::preRewrite returning " << node << std::endl;
-    return RewriteResponse(REWRITE_DONE, node);
-  }
+  static RewriteResponse postRewrite(TNode node);
+  static RewriteResponse preRewrite(TNode node);
 
   static inline void init() {}
   static inline void shutdown() {}
 
-};/* class TheoryArraysRewriter */
-
-}/* CVC4::theory::arrays namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}; /* class TheoryArraysRewriter */
 
-#endif /* __CVC4__THEORY__ARRAYS__THEORY_ARRAYS_REWRITER_H */
+} /* CVC4::theory::arrays namespace */
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */