From 354441c5b1c3d0f4d19d1f92e45df08e1d615b2c Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 14 Apr 2022 14:11:57 -0500 Subject: [PATCH] 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. --- src/theory/arrays/theory_arrays_rewriter.cpp | 15 ++++++++++++--- src/theory/arrays/theory_arrays_rewriter.h | 6 ++++-- src/theory/arrays/type_enumerator.cpp | 8 ++++++-- src/theory/uf/function_const.cpp | 12 +++++------- 4 files changed, 27 insertions(+), 14 deletions(-) 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 ArrayConstantMostFrequentValueCountAttr; -typedef expr::Attribute ArrayConstantMostFrequentValueAttr; +using ArrayConstantMostFrequentValueCountAttr = + expr::Attribute; +using ArrayConstantMostFrequentValueAttr = + expr::Attribute; 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 -- 2.30.2