Refactor arithmetic pre-rewriter for multiplication (#7930)

This PR refactors the pre-rewrite stage for multiplication.

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index bef9f9a3ee4ce9a1c5fb71b9b11b458f23b58e40..09a340f82df3588b65fcd9da404a46789442683d 100644 (file)
--- 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<Rational>().isOne())
-    {
-      return RewriteResponse(REWRITE_DONE, t[1]);
-    }
-    if (t[1].isConst() && t[1].getConst<Rational>().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<Rational>().isZero())
     {
-      if((*i).getConst<Rational>().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){