pow2 -- final changes (#6800)

This commit adds the remaining changes for a working and integrated `pow2` solver.

In particular, it adds a rewrite and a lemma that identify `pow2(x)` with `0` whenever `x<0`.
Regressions are added as well, including `pow2-native-0.smt2` that shows the semantics of `pow2` on negative values.

The next steps are new rewrites and and more lemma schemas. 

1 files changed, 6 insertions, 0 deletions

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index b0453fad4..6eda6283c 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -393,6 +393,12 @@ RewriteResponse ArithRewriter::postRewritePow2(TNode t)
     // pow2 is only supported for integers
     Assert(t[0].getType().isInteger());
     Integer i = t[0].getConst<Rational>().getNumerator();
+    if (i < 0)
+    {
+      return RewriteResponse(
+          REWRITE_DONE,
+          nm->mkConst<Rational>(Rational(Integer(0), Integer(1))));
+    }
     unsigned long k = i.getUnsignedLong();
     Node ret = nm->mkConst<Rational>(Rational(Integer(2).pow(k), Integer(1)));
     return RewriteResponse(REWRITE_DONE, ret);