From 09d66569502849d3a934b83de0f4777e8ed38b08 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 14 Jan 2022 08:30:14 -0800 Subject: [PATCH] Refactor arithmetic pre-rewriter for multiplication (#7930) This PR refactors the pre-rewrite stage for multiplication. --- src/theory/arith/arith_rewriter.cpp | 31 +++++++++-------------------- 1 file changed, 9 insertions(+), 22 deletions(-) diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index bef9f9a3e..09a340f82 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -465,32 +465,19 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){ } } +RewriteResponse ArithRewriter::preRewriteMult(TNode node) +{ + Assert(node.getKind() == kind::MULT + || node.getKind() == kind::NONLINEAR_MULT); -RewriteResponse ArithRewriter::preRewriteMult(TNode t){ - Assert(t.getKind() == kind::MULT || t.getKind() == kind::NONLINEAR_MULT); - - if(t.getNumChildren() == 2){ - if (t[0].isConst() && t[0].getConst().isOne()) - { - return RewriteResponse(REWRITE_DONE, t[1]); - } - if (t[1].isConst() && t[1].getConst().isOne()) - { - return RewriteResponse(REWRITE_DONE, t[0]); - } - } - - // Rewrite multiplications with a 0 argument and to 0 - for(TNode::iterator i = t.begin(); i != t.end(); ++i) { - if ((*i).isConst()) + for (const auto& child : node) + { + if (child.isConst() && child.getConst().isZero()) { - if((*i).getConst().isZero()) { - TNode zero = (*i); - return RewriteResponse(REWRITE_DONE, zero); - } + return RewriteResponse(REWRITE_DONE, child); } } - return RewriteResponse(REWRITE_DONE, t); + return RewriteResponse(REWRITE_DONE, node); } static bool canFlatten(Kind k, TNode t){ -- 2.30.2