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 6eda6283ce86d1e7621920327056df6d69313418..5baaaf317af8ef86dbcf2d4b73e8e8a5e074ff1b 100644 (file)
--- 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 d2d6f0855a0c40d54d5b134d716a177eab562519..abd21e2221f21e0351939b5adbfa5363574ed9cb 100644 (file)
--- 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 (file)
index 0000000..8fdbfa6
--- /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 854062bebeabf6fa5de484e884a0f2485f6c27c8..50be132af51417635fcb28aa738745e72f65e5ba 100644 (file)
--- 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;