From: Gereon Kremer <gkremer@stanford.edu>
Date: Fri, 14 Jan 2022 16:30:14 +0000 (-0800)
Subject: Refactor arithmetic pre-rewriter for multiplication (#7930)
X-Git-Tag: cvc5-1.0.0~546
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=09d66569502849d3a934b83de0f4777e8ed38b08;p=cvc5.git

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 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<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){