From 8f514283c62415abbc6498758cc128682984afcc Mon Sep 17 00:00:00 2001
From: yoni206 <yoni206@users.noreply.github.com>
Date: Tue, 21 Dec 2021 16:49:35 +0200
Subject: [PATCH] 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.
---
 src/theory/arith/arith_rewriter.cpp |  7 +++--
 test/unit/api/cpp/solver_black.cpp  | 44 +++++++++++++++++++++++++++++
 2 files changed, 48 insertions(+), 3 deletions(-)

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 0268a9eb1..f7d2a2a11 100644
--- 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 d96ff17a0..960d4bb69 100644
--- 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");
-- 
2.30.2