From 0e3ece61a4dbec520bcf1ef4087b3b5eb79d5771 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gkremer@stanford.edu>
Date: Wed, 8 Dec 2021 15:25:19 -0800
Subject: [PATCH] Remove rewrites from iand and pow2 solvers (#7775)

This PR removes some more static calls to the rewriter from the iand and pow2 solvers.
---
 src/theory/arith/nl/ext/monomial.cpp |  1 -
 src/theory/arith/nl/iand_solver.cpp  |  4 ++--
 src/theory/arith/nl/iand_solver.h    |  4 ++--
 src/theory/arith/nl/iand_utils.cpp   | 13 +++----------
 src/theory/arith/nl/pow2_solver.cpp  |  3 +--
 src/theory/arith/nl/pow2_solver.h    |  2 +-
 6 files changed, 9 insertions(+), 18 deletions(-)

diff --git a/src/theory/arith/nl/ext/monomial.cpp b/src/theory/arith/nl/ext/monomial.cpp
index 83d0ff71f..47beb6959 100644
--- a/src/theory/arith/nl/ext/monomial.cpp
+++ b/src/theory/arith/nl/ext/monomial.cpp
@@ -326,7 +326,6 @@ Node MonomialDb::mkMonomialRemFactor(Node n,
     children.insert(children.end(), inc, v);
   }
   Node ret = safeConstructNary(MULT, children);
-  ret = Rewriter::rewrite(ret);
   Trace("nl-ext-mono-factor") << "...return : " << ret << std::endl;
   return ret;
 }
diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index 5d4862307..90a9c5f78 100644
--- a/src/theory/arith/nl/iand_solver.cpp
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -100,7 +100,7 @@ void IAndSolver::checkInitialRefine()
       // conj.push_back(i.eqNode(nm->mkNode(IAND, op, i[1], i[0])));
       // 0 <= iand(x,y) < 2^k
       conj.push_back(nm->mkNode(LEQ, d_zero, i));
-      conj.push_back(nm->mkNode(LT, i, d_iandUtils.twoToK(k)));
+      conj.push_back(nm->mkNode(LT, i, rewrite(d_iandUtils.twoToK(k))));
       // iand(x,y)<=x
       conj.push_back(nm->mkNode(LEQ, i, i[0]));
       // iand(x,y)<=y
@@ -296,7 +296,7 @@ Node IAndSolver::bitwiseLemma(Node i)
       bitIAnd = d_iandUtils.createBitwiseIAndNode(x, y, high_bit, j);
       // enforce bitwise equality
       lem = nm->mkNode(
-          AND, lem, d_iandUtils.iextract(high_bit, j, i).eqNode(bitIAnd));
+          AND, lem, rewrite(d_iandUtils.iextract(high_bit, j, i)).eqNode(bitIAnd));
     }
   }
   return lem;
diff --git a/src/theory/arith/nl/iand_solver.h b/src/theory/arith/nl/iand_solver.h
index 0b6a1fac6..997112fee 100644
--- a/src/theory/arith/nl/iand_solver.h
+++ b/src/theory/arith/nl/iand_solver.h
@@ -103,7 +103,7 @@ class IAndSolver : protected EnvObj
 
   /**
    * convert integer value to bitvector value of bitwidth k,
-   * equivalent to Rewriter::rewrite( ((_ intToBv k) n) ).
+   * equivalent to rewrite( ((_ intToBv k) n) ).
    */
   Node convertToBvK(unsigned k, Node n) const;
   /** make iand */
@@ -115,7 +115,7 @@ class IAndSolver : protected EnvObj
   /**
    * Value-based refinement lemma for i of the form ((_ iand k) x y). Returns:
    *   x = M(x) ^ y = M(y) =>
-   *     ((_ iand k) x y) = Rewriter::rewrite(((_ iand k) M(x) M(y)))
+   *     ((_ iand k) x y) = rewrite(((_ iand k) M(x) M(y)))
    */
   Node valueBasedLemma(Node i);
   /**
diff --git a/src/theory/arith/nl/iand_utils.cpp b/src/theory/arith/nl/iand_utils.cpp
index 50e03bfa5..8af1a38fb 100644
--- a/src/theory/arith/nl/iand_utils.cpp
+++ b/src/theory/arith/nl/iand_utils.cpp
@@ -186,9 +186,7 @@ Node IAndUtils::iextract(unsigned i, unsigned j, Node n) const
   NodeManager* nm = NodeManager::currentNM();
   //  ((_ extract i j) n) is n / 2^j mod 2^{i-j+1}
   Node n2j = nm->mkNode(kind::INTS_DIVISION_TOTAL, n, twoToK(j));
-  Node ret = nm->mkNode(kind::INTS_MODULUS_TOTAL, n2j, twoToK(i - j + 1));
-  ret = Rewriter::rewrite(ret);
-  return ret;
+  return nm->mkNode(kind::INTS_MODULUS_TOTAL, n2j, twoToK(i - j + 1));
 }
 
 void IAndUtils::computeAndTable(uint64_t granularity)
@@ -266,19 +264,14 @@ Node IAndUtils::twoToK(unsigned k) const
 {
   // could be faster
   NodeManager* nm = NodeManager::currentNM();
-  Node ret =
-      nm->mkNode(kind::POW, d_two, nm->mkConst(CONST_RATIONAL, Rational(k)));
-  ret = Rewriter::rewrite(ret);
-  return ret;
+  return nm->mkNode(kind::POW, d_two, nm->mkConst(CONST_RATIONAL, Rational(k)));
 }
 
 Node IAndUtils::twoToKMinusOne(unsigned k) const
 {
   // could be faster
   NodeManager* nm = NodeManager::currentNM();
-  Node ret = nm->mkNode(kind::MINUS, twoToK(k), d_one);
-  ret = Rewriter::rewrite(ret);
-  return ret;
+  return nm->mkNode(kind::MINUS, twoToK(k), d_one);
 }
 
 }  // namespace nl
diff --git a/src/theory/arith/nl/pow2_solver.cpp b/src/theory/arith/nl/pow2_solver.cpp
index e3a26397e..4752d45ff 100644
--- a/src/theory/arith/nl/pow2_solver.cpp
+++ b/src/theory/arith/nl/pow2_solver.cpp
@@ -190,8 +190,7 @@ Node Pow2Solver::valueBasedLemma(Node i)
   Node valC = nm->mkNode(POW2, valX);
   valC = rewrite(valC);
 
-  Node lem = nm->mkNode(IMPLIES, x.eqNode(valX), i.eqNode(valC));
-  return lem;
+  return nm->mkNode(IMPLIES, x.eqNode(valX), i.eqNode(valC));
 }
 
 }  // namespace nl
diff --git a/src/theory/arith/nl/pow2_solver.h b/src/theory/arith/nl/pow2_solver.h
index b4e12616c..42586f206 100644
--- a/src/theory/arith/nl/pow2_solver.h
+++ b/src/theory/arith/nl/pow2_solver.h
@@ -100,7 +100,7 @@ class Pow2Solver : protected EnvObj
   /**
    * Value-based refinement lemma for i of the form (pow2 x). Returns:
    *   x = M(x) /\ x>= 0 ---->
-   *     (pow2 x) = Rewriter::rewrite((pow2 M(x)))
+   *     (pow2 x) = rewrite((pow2 M(x)))
    */
   Node valueBasedLemma(Node i);
 }; /* class Pow2Solver */
-- 
2.30.2