diff --git a/src/theory/arrays/theory_arrays_rewriter.cpp b/src/theory/arrays/theory_arrays_rewriter.cpp index 8aaa6c58fac..2b49cd62730 100644 --- a/src/theory/arrays/theory_arrays_rewriter.cpp +++ b/src/theory/arrays/theory_arrays_rewriter.cpp @@ -430,7 +430,7 @@ RewriteResponse TheoryArraysRewriter::postRewrite(TNode node) } else { - n = d_rewriter->rewrite(mkEqNode(store[1], index)); + n = mkEqNode(store[1], index); if (n.getKind() != Kind::CONST_BOOLEAN) { break; @@ -502,7 +502,7 @@ RewriteResponse TheoryArraysRewriter::postRewrite(TNode node) } else { - Node eqRewritten = d_rewriter->rewrite(mkEqNode(store[1], index)); + Node eqRewritten = mkEqNode(store[1], index); if (eqRewritten.getKind() != Kind::CONST_BOOLEAN) { Trace("arrays-postrewrite") @@ -542,7 +542,7 @@ RewriteResponse TheoryArraysRewriter::postRewrite(TNode node) } else { - n = d_rewriter->rewrite(mkEqNode(store[1], index)); + n = mkEqNode(store[1], index); if (n.getKind() != Kind::CONST_BOOLEAN) { break; @@ -639,12 +639,7 @@ RewriteResponse TheoryArraysRewriter::preRewrite(TNode node) } else { - n = d_rewriter->rewrite(mkEqNode(store[1], index)); - if (n.getKind() != Kind::CONST_BOOLEAN) - { - break; - } - val = n.getConst(); + break; } if (val) { @@ -702,12 +697,7 @@ RewriteResponse TheoryArraysRewriter::preRewrite(TNode node) } else { - Node eqRewritten = d_rewriter->rewrite(mkEqNode(store[1], index)); - if (eqRewritten.getKind() != Kind::CONST_BOOLEAN) - { - break; - } - val = eqRewritten.getConst(); + break; } NodeManager* nm = nodeManager(); if (val) @@ -754,6 +744,12 @@ Node TheoryArraysRewriter::expandDefinition(Node node) return Node::null(); } +Node TheoryArraysRewriter::mkEqNode(const Node& a, const Node& b) const +{ + Node eq = a.eqNode(b); + return d_rewriter->rewrite(eq); +} + } // namespace arrays } // namespace theory } // namespace cvc5::internal diff --git a/src/theory/arrays/theory_arrays_rewriter.h b/src/theory/arrays/theory_arrays_rewriter.h index 2792d1118c1..f904ca56193 100644 --- a/src/theory/arrays/theory_arrays_rewriter.h +++ b/src/theory/arrays/theory_arrays_rewriter.h @@ -40,8 +40,6 @@ uint64_t getMostFrequentValueCount(TNode store); void setMostFrequentValue(TNode store, TNode value); void setMostFrequentValueCount(TNode store, uint64_t count); -static inline Node mkEqNode(Node a, Node b) { return a.eqNode(b); } - class TheoryArraysRewriter : public TheoryRewriter { public: @@ -88,6 +86,13 @@ class TheoryArraysRewriter : public TheoryRewriter * be removed. */ Rewriter* d_rewriter; + /** + * Make rewritten equality. + * @param a The first term. + * @param b The second term. + * @return the rewritten form of the equality between a and b. + */ + Node mkEqNode(const Node& a, const Node& b) const; }; /* class TheoryArraysRewriter */ } // namespace arrays