From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 14 Apr 2022 19:11:57 +0000 (-0500)
Subject: Remove static calls to rewrite involving array constants (#8613)
X-Git-Tag: cvc5-1.0.1~259
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=354441c5b1c3d0f4d19d1f92e45df08e1d615b2c;p=cvc5.git

Remove static calls to rewrite involving array constants (#8613)

The type enumerators for arrays and functions relied on static calls to the rewriter. This is overkill, as the appropriate calls to the utility method normalizeConstant in the array rewriter class suffices.

The eliminates 2 of the remaining static calls to the rewriter.
---

diff --git a/src/theory/arrays/theory_arrays_rewriter.cpp b/src/theory/arrays/theory_arrays_rewriter.cpp
index a91c332c9..4aad2bf9a 100644
--- a/src/theory/arrays/theory_arrays_rewriter.cpp
+++ b/src/theory/arrays/theory_arrays_rewriter.cpp
@@ -23,6 +23,7 @@
 #include "proof/conv_proof_generator.h"
 #include "proof/eager_proof_generator.h"
 #include "theory/arrays/skolem_cache.h"
+#include "theory/type_enumerator.h"
 #include "util/cardinality.h"
 
 namespace cvc5::internal {
@@ -38,8 +39,10 @@ struct ArrayConstantMostFrequentValueCountTag
 };
 }  // namespace attr
 
-typedef expr::Attribute<attr::ArrayConstantMostFrequentValueCountTag, uint64_t> ArrayConstantMostFrequentValueCountAttr;
-typedef expr::Attribute<attr::ArrayConstantMostFrequentValueTag, Node> ArrayConstantMostFrequentValueAttr;
+using ArrayConstantMostFrequentValueCountAttr =
+    expr::Attribute<attr::ArrayConstantMostFrequentValueCountTag, uint64_t>;
+using ArrayConstantMostFrequentValueAttr =
+    expr::Attribute<attr::ArrayConstantMostFrequentValueTag, Node>;
 
 Node getMostFrequentValue(TNode store) {
   return store.getAttribute(ArrayConstantMostFrequentValueAttr());
@@ -63,7 +66,13 @@ TheoryArraysRewriter::TheoryArraysRewriter(Rewriter* rewriter,
 
 Node TheoryArraysRewriter::normalizeConstant(TNode node)
 {
-  return normalizeConstant(node, node[1].getType().getCardinality());
+  if (node.isConst())
+  {
+    return node;
+  }
+  Node ret = normalizeConstant(node, node[1].getType().getCardinality());
+  Assert(ret.isConst());
+  return ret;
 }
 
 // this function is called by printers when using the option "--model-u-dt-enum"
diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h
index a1fddbbe5..9c179eca9 100644
--- a/src/theory/arrays/theory_arrays_rewriter.h
+++ b/src/theory/arrays/theory_arrays_rewriter.h
@@ -26,7 +26,6 @@
 
 #include "theory/rewriter.h"
 #include "theory/theory_rewriter.h"
-#include "theory/type_enumerator.h"
 
 namespace cvc5::internal {
 
@@ -69,13 +68,16 @@ class TheoryArraysRewriter : public TheoryRewriter
 
   static inline void init() {}
 
- private:
   /**
    * Puts array constant node into normal form. This is so that array constants
    * that are distinct nodes are semantically disequal.
+   *
+   * This method should only be called on STORE chains whose AST is built
+   * from constant terms only.
    */
   static Node normalizeConstant(TNode node);
 
+ private:
   /** The associated rewriter. */
   Rewriter* d_rewriter;
 
diff --git a/src/theory/arrays/type_enumerator.cpp b/src/theory/arrays/type_enumerator.cpp
index c365b6212..3e7c7a249 100644
--- a/src/theory/arrays/type_enumerator.cpp
+++ b/src/theory/arrays/type_enumerator.cpp
@@ -17,6 +17,7 @@
 #include "expr/array_store_all.h"
 #include "expr/kind.h"
 #include "expr/type_node.h"
+#include "theory/arrays/theory_arrays_rewriter.h"
 #include "theory/rewriter.h"
 #include "theory/type_enumerator.h"
 
@@ -86,9 +87,12 @@ Node ArrayEnumerator::operator*()
                      n,
                      d_indexVec[d_indexVec.size() - 1 - i],
                      *(*(d_constituentVec[i])));
+    // Normalize the constant. We must do this every iteration of this loop,
+    // since this utility requires all children of n to be constant, which
+    // implies the first argument to STORE on the next iteration must be
+    // normalized.
+    n = TheoryArraysRewriter::normalizeConstant(n);
   }
-  Trace("array-type-enum") << "operator * prerewrite: " << n << std::endl;
-  n = Rewriter::rewrite(n);
   Trace("array-type-enum") << "operator * returning: " << n << std::endl;
   return n;
 }
diff --git a/src/theory/uf/function_const.cpp b/src/theory/uf/function_const.cpp
index ef991eac5..8167bcca0 100644
--- a/src/theory/uf/function_const.cpp
+++ b/src/theory/uf/function_const.cpp
@@ -16,6 +16,7 @@
 #include "theory/uf/function_const.h"
 
 #include "expr/array_store_all.h"
+#include "theory/arrays/theory_arrays_rewriter.h"
 #include "theory/rewriter.h"
 
 namespace cvc5::internal {
@@ -383,6 +384,9 @@ Node FunctionConst::getArrayRepresentationForLambdaRec(TNode n,
       size_t ii = (numCond - 1) - i;
       Assert(conds[ii].getType().isSubtypeOf(first_arg.getType()));
       curr = nm->mkNode(kind::STORE, curr, conds[ii], vals[ii]);
+      // normalize it using the array rewriter utility, which must be done at
+      // each iteration of this loop
+      curr = arrays::TheoryArraysRewriter::normalizeConstant(curr);
     }
     Trace("builtin-rewrite-debug")
         << "...got array " << curr << " for " << n << std::endl;
@@ -400,13 +404,7 @@ Node FunctionConst::getArrayRepresentationForLambda(TNode n)
   // must carry the overall return type to deal with cases like (lambda ((x Int)
   // (y Int)) (ite (= x _) 0.5 0.0)), where the inner construction for the else
   // case above should be (arraystoreall (Array Int Real) 0.0)
-  Node anode = getArrayRepresentationForLambdaRec(n, n[1].getType());
-  if (anode.isNull())
-  {
-    return anode;
-  }
-  // must rewrite it to make canonical
-  return Rewriter::rewrite(anode);
+  return getArrayRepresentationForLambdaRec(n, n[1].getType());
 }
 
 }  // namespace uf