From: yoni206 <yoni206@users.noreply.github.com>
Date: Mon, 28 Jun 2021 23:42:13 +0000 (-0700)
Subject: Rewrite POW to POW2 when the base is 2 (#6806)
X-Git-Tag: cvc5-1.0.0~1550
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5652f1bcb3702ff60ebe3248a6e027a3138d5c99;p=cvc5.git

Rewrite POW to POW2 when the base is 2 (#6806)

This PR introduces a rewrite from (^ 2 t) to (pow2 t) in order to make use of the specialized pow2 solver.
One regression that expects an error when t is not a constant is changed accordingly.
---

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 6eda6283c..5baaaf317 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -255,6 +255,12 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
             }
           }
         }
+        else if (t[0].getKind() == kind::CONST_RATIONAL
+                 && t[0].getConst<Rational>().getNumerator().toUnsignedInt() == 2)
+        {
+          return RewriteResponse(
+              REWRITE_DONE, NodeManager::currentNM()->mkNode(kind::POW2, t[1]));
+        }
 
         // Todo improve the exception thrown
         std::stringstream ss;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index d2d6f0855..abd21e222 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -737,6 +737,7 @@ set(regress_0_tests
   regress0/nl/pow2-native-1.smt2
   regress0/nl/pow2-native-2.smt2
   regress0/nl/pow2-native-3.smt2
+  regress0/nl/pow2-pow.smt2
   regress0/nl/real-as-int.smt2
   regress0/nl/real-div-ufnra.smt2
   regress0/nl/sin-cos-346-b-chunk-0169.smt2
diff --git a/test/regress/regress0/nl/pow2-pow.smt2 b/test/regress/regress0/nl/pow2-pow.smt2
new file mode 100644
index 000000000..8fdbfa659
--- /dev/null
+++ b/test/regress/regress0/nl/pow2-pow.smt2
@@ -0,0 +1,6 @@
+; EXPECT: unsat
+(set-logic QF_NIA)
+(declare-fun x () Int)
+(assert (< x 0))
+(assert (distinct (^ 2 x) 0))
+(check-sat)
diff --git a/test/regress/regress1/arith/bug716.1.cvc b/test/regress/regress1/arith/bug716.1.cvc
index 854062beb..50be132af 100644
--- a/test/regress/regress1/arith/bug716.1.cvc
+++ b/test/regress/regress1/arith/bug716.1.cvc
@@ -1,6 +1,6 @@
 % EXPECT: The exponent of the POW(^) operator can only be a positive integral constant below 67108864. Exception occurred in:
-% EXPECT:   2 ^ x
+% EXPECT:   3 ^ x
 % EXIT: 1
 x: INT;
-ASSERT 2^x = 8;
+ASSERT 3^x = 27;
 QUERY x=3;