Remove rewrites from iand and pow2 solvers (#7775)

This PR removes some more static calls to the rewriter from the iand and pow2 solvers.

diff --git a/src/theory/arith/nl/ext/monomial.cpp b/src/theory/arith/nl/ext/monomial.cpp
index 83d0ff71fae6f02d14b14c60dc42a0a368c1dca4..47beb6959f37d693e246455882cef36d6aba4acd 100644 (file)
--- 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 5d486230760079a9981e9ad2f264d4487f049ba6..90a9c5f784964578ce49eb97e4f97035a4b53499 100644 (file)
--- 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 0b6a1fac65b3f6b451eb615dd42f5072a2bd346b..997112fee2c50bb787f0683440552e2e390ae5cb 100644 (file)
--- 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 50e03bfa5f42389d65086c0bf0083f43b69824f3..8af1a38fb5f41f028f987b21821173558442fdb9 100644 (file)
--- 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 e3a26397ee0a0737ff4041f040c00ad8ca4b2d20..4752d45ffef5fc122f9b06b406e3ece4d41f1266 100644 (file)
--- 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 b4e12616cb48d8a1acc53c2bc9980d408e648558..42586f2064f9b43af70aa8d806d79df6c3e2410b 100644 (file)
--- 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 */