From 37536425f42d4d2057554ab6b8101c6ec7b8388b Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Thu, 15 Dec 2022 14:03:42 +0100
Subject: [PATCH] Encode 2^k*x as (bvshl x k) in the fallback solver

---
 .../polysat/univariate/univariate_solver.cpp  | 35 ++++++++++++++++++-
 src/test/polysat.cpp                          |  3 +-
 2 files changed, 36 insertions(+), 2 deletions(-)

diff --git a/src/math/polysat/univariate/univariate_solver.cpp b/src/math/polysat/univariate/univariate_solver.cpp
index e00777ab8..7c23b56ec 100644
--- a/src/math/polysat/univariate/univariate_solver.cpp
+++ b/src/math/polysat/univariate/univariate_solver.cpp
@@ -64,7 +64,8 @@ namespace polysat {
             return bv->mk_numeral(r, bit_width);
         }
 
-        // [d,c,b,a]  ==>  ((a*x + b)*x + c)*x + d
+#if 0
+        // [d,c,b,a]  -->  ((a*x + b)*x + c)*x + d
         expr* mk_poly(univariate const& p) const {
             if (p.empty()) {
                 return mk_numeral(rational::zero());
@@ -79,6 +80,38 @@ namespace polysat {
                 return e;
             }
         }
+#else
+        // TODO: shouldn't the simplification step of the underlying solver already support this transformation? how to enable?
+        // 2^k*x  -->  x << k
+        // n*x    -->  n * x
+        expr* mk_poly_term(rational const& coeff, expr* xpow) const {
+            unsigned pow;
+            if (coeff.is_power_of_two(pow))
+                return bv->mk_bv_shl(xpow, mk_numeral(rational(pow)));
+            else
+                return bv->mk_bv_mul(mk_numeral(coeff), xpow);
+        }
+
+        // [d,c,b,a]  -->  d + c*x + b*(x*x) + a*(x*x*x)
+        expr* mk_poly(univariate const& p) const {
+            if (p.empty()) {
+                return mk_numeral(rational::zero());
+            }
+            else {
+                expr* e = mk_numeral(p.back());
+                expr* xpow = x;
+                for (unsigned i = p.size() - 1; i-- > 0; ) {
+                    if (!p[i].is_zero()) {
+                        expr* t = mk_poly_term(p[i], xpow);
+                        e = bv->mk_bv_add(e, t);
+                    }
+                    if (i)
+                        xpow = bv->mk_bv_mul(xpow, x);
+                }
+                return e;
+            }
+        }
+#endif
 
         void add(expr* e, bool sign, dep_t dep) {
             if (sign)
diff --git a/src/test/polysat.cpp b/src/test/polysat.cpp
index b81c66352..d96f20e60 100644
--- a/src/test/polysat.cpp
+++ b/src/test/polysat.cpp
@@ -1661,7 +1661,8 @@ void tst_polysat() {
     // test_polysat::test_parity1b();
     // test_polysat::test_parity2();
     // test_polysat::test_parity3();
-    test_polysat::test_parity4();
+    // test_polysat::test_parity4();
+    // test_polysat::test_parity4(32);
     test_polysat::test_parity4(256);
     // test_polysat::test_ineq2();
     // test_polysat::test_ineq_non_axiom4(32, 3);  // stuck in viable refinement loop