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. 

5 files changed, 40 insertions, 0 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 24eee5998..d2d6f0855 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -733,6 +733,10 @@ set(regress_0_tests
   regress0/nl/nta/sin-sym.smt2
   regress0/nl/nta/sqrt-simple.smt2
   regress0/nl/nta/tan-rewrite.smt2
+  regress0/nl/pow2-native-0.smt2
+  regress0/nl/pow2-native-1.smt2
+  regress0/nl/pow2-native-2.smt2
+  regress0/nl/pow2-native-3.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-native-0.smt2 b/test/regress/regress0/nl/pow2-native-0.smt2
new file mode 100644
index 000000000..f88ac4151
--- /dev/null
+++ b/test/regress/regress0/nl/pow2-native-0.smt2
@@ -0,0 +1,6 @@
+; EXPECT: unsat
+(set-logic QF_NIA)
+(declare-fun x () Int)
+(assert (< x 0))
+(assert (distinct (pow2 x) 0))
+(check-sat)
diff --git a/test/regress/regress0/nl/pow2-native-1.smt2 b/test/regress/regress0/nl/pow2-native-1.smt2
new file mode 100644
index 000000000..1e24ae572
--- /dev/null
+++ b/test/regress/regress0/nl/pow2-native-1.smt2
@@ -0,0 +1,9 @@
+; EXPECT: sat
+(set-logic QF_NIA)
+(set-info :status sat)
+(declare-fun x () Int)
+
+(assert (and (<= 0 x) (< x 16)))
+(assert (> (pow2 x) 0))
+
+(check-sat)
diff --git a/test/regress/regress0/nl/pow2-native-2.smt2 b/test/regress/regress0/nl/pow2-native-2.smt2
new file mode 100644
index 000000000..ba0621dbc
--- /dev/null
+++ b/test/regress/regress0/nl/pow2-native-2.smt2
@@ -0,0 +1,9 @@
+; EXPECT: unsat
+(set-logic QF_NIA)
+(set-info :status unsat)
+(declare-fun x () Int)
+
+(assert (and (<= 0 x) (< x 16)))
+(assert (< (pow2 x) x))
+
+(check-sat)
diff --git a/test/regress/regress0/nl/pow2-native-3.smt2 b/test/regress/regress0/nl/pow2-native-3.smt2
new file mode 100644
index 000000000..45975a474
--- /dev/null
+++ b/test/regress/regress0/nl/pow2-native-3.smt2
@@ -0,0 +1,12 @@
+; EXPECT: unsat
+(set-logic QF_NIA)
+(set-info :status unsat)
+(declare-fun x () Int)
+(declare-fun y () Int)
+
+(assert (<= 0 x))
+(assert (<= 0 y))
+(assert (< x y))
+(assert (> (pow2 x) (pow2 y)))
+
+(check-sat)