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 a91c332c9d0a3a52081e46e06083ab68c561ba2e..4aad2bf9a43485be9c4ce41ab5bce6add04b59ad 100644 (file)
--- 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 a1fddbbe52aae70bb0d8fc9de187df89ae43f52c..9c179eca9e4c490c762ea043c036725690bbbbf9 100644 (file)
--- 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 c365b62126def3c831658da7cf443517dfe0d47d..3e7c7a2491ca4e9332da0eda5cbf3dc6cfbef855 100644 (file)
--- 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 ef991eac573177d843f6c84bf7c4613901fa483e..8167bcca022dce154d0e556e7788ab06350f1f0f 100644 (file)
--- 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