Rewrite (pow2 x) to (pow 2 x) when x is a constant (#7849)

Fixes https://github.com/cvc5/cvc5-projects/issues/371.
Fixes https://github.com/cvc5/cvc5-projects/issues/339.
Fixes https://github.com/cvc5/cvc5-projects/issues/333.

Variants of the tests in the above issues are added to this PR. In them, we expect to get an exception because the constant is too big.

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 0268a9eb1d688432d5315c762fe69922bd8d5e73..f7d2a2a11e11ef6e23e527481cf91126c22969f0 100644 (file)
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -396,9 +396,10 @@ RewriteResponse ArithRewriter::postRewritePow2(TNode t)
     {
       return RewriteResponse(REWRITE_DONE, nm->mkConstInt(Rational(0)));
     }
-    unsigned long k = i.getUnsignedLong();
-    Node ret = nm->mkConstInt(Rational(Integer(2).pow(k)));
-    return RewriteResponse(REWRITE_DONE, ret);
+    // (pow2 t) ---> (pow 2 t) and continue rewriting to eliminate pow
+    Node two = nm->mkConstInt(Rational(Integer(2)));
+    Node ret = nm->mkNode(kind::POW, two, t[0]);
+    return RewriteResponse(REWRITE_AGAIN, ret);
   }
   return RewriteResponse(REWRITE_DONE, t);
 }

diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index d96ff17a07f439658e2642854ffb1a31663c3e64..960d4bb6977a9d4445e48bd598f0df4b1555d2e8 100644 (file)
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -28,6 +28,50 @@ class TestApiBlackSolver : public TestApi
 {
 };
 
+TEST_F(TestApiBlackSolver, pow2Large1)
+{
+  // Based on https://github.com/cvc5/cvc5-projects/issues/371
+  Sort s1 = d_solver.getStringSort();
+  Sort s2 = d_solver.getIntegerSort();
+  Sort s4 = d_solver.mkArraySort(s1, s2);
+  Sort s7 = d_solver.mkArraySort(s2, s1);
+  Term t10 = d_solver.mkInteger("68038927088685865242724985643");
+  Term t74 = d_solver.mkInteger("8416288636405");
+  std::vector<DatatypeConstructorDecl> ctors;
+  ctors.push_back(d_solver.mkDatatypeConstructorDecl("_x109"));
+  ctors.back().addSelector("_x108", s7);
+  ctors.push_back(d_solver.mkDatatypeConstructorDecl("_x113"));
+  ctors.back().addSelector("_x110", s4);
+  ctors.back().addSelector("_x111", s2);
+  ctors.back().addSelector("_x112", s7);
+  Sort s11 = d_solver.declareDatatype("_x107", ctors);
+  Term t82 = d_solver.mkConst(s11, "_x114");
+  Term t180 = d_solver.mkTerm(POW2, t10);
+  Term t258 = d_solver.mkTerm(GEQ, t74, t180);
+  d_solver.assertFormula(t258);
+  ASSERT_THROW(d_solver.simplify(t82), CVC5ApiException);
+}
+
+TEST_F(TestApiBlackSolver, pow2Large2)
+{
+  // Based on https://github.com/cvc5/cvc5-projects/issues/333
+  Term t1 = d_solver.mkBitVector(63, ~(((uint64_t)1) << 62));
+  Term t2 = d_solver.mkTerm(Kind::BITVECTOR_TO_NAT, t1);
+  Term t3 = d_solver.mkTerm(Kind::POW2, t2);
+  Term t4 = d_solver.mkTerm(Kind::DISTINCT, t3, t2);
+  ASSERT_THROW(d_solver.checkSatAssuming({t4}), CVC5ApiException);
+}
+
+TEST_F(TestApiBlackSolver, pow2Large3)
+{
+  // Based on https://github.com/cvc5/cvc5-projects/issues/339
+  Sort s4 = d_solver.getIntegerSort();
+  Term t203 = d_solver.mkInteger("6135470354240554220207");
+  Term t262 = d_solver.mkTerm(POW2, t203);
+  Term t536 = d_solver.mkTerm(d_solver.mkOp(INT_TO_BITVECTOR, 49), t262);
+  ASSERT_THROW(d_solver.simplify(t536), CVC5ApiException);
+}
+
 TEST_F(TestApiBlackSolver, recoverableException)
 {
   d_solver.setOption("produce-models", "true");