fix #3951

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/ast/rewriter/bool_rewriter.h

@@ -133,6 +133,11 @@ public:
         if (mk_eq_core(lhs, rhs, result) == BR_FAILED)
             result = mk_eq(lhs, rhs);
     }
+    expr_ref mk_eq_rw(expr* lhs, expr* rhs) {
+        expr_ref r(m());
+        mk_eq(lhs, rhs, r);
+        return r;
+    }
     void mk_iff(expr * lhs, expr * rhs, expr_ref & result) { mk_eq(lhs, rhs, result); }
     void mk_xor(expr * lhs, expr * rhs, expr_ref & result);
     void mk_and(unsigned num_args, expr * const * args, expr_ref & result) {
@@ -187,6 +192,11 @@ public:
         if (mk_ite_core(c, t, e, result) == BR_FAILED)
             result = m().mk_ite(c, t, e);
     }
+    expr_ref mk_ite(expr * c, expr * t, expr * e) {
+        expr_ref r(m());
+        mk_ite(c, t, e, r);
+        return r;
+    }
     void mk_distinct(unsigned num_args, expr * const * args, expr_ref & result) {
         if (mk_distinct_core(num_args, args, result) == BR_FAILED)
             result = m().mk_distinct(num_args, args);
@@ -195,6 +205,11 @@ public:
         if (mk_not_core(t, result) == BR_FAILED)
             result = m().mk_not(t);
     }
+    expr_ref mk_not(expr* t) {
+        expr_ref r(m());
+        mk_not(t, r);
+        return r;
+    }
 
     void mk_nand(unsigned num_args, expr * const * args, expr_ref & result);
     void mk_nor(unsigned num_args, expr * const * args, expr_ref & result);

src/tactic/core/reduce_invertible_tactic.cpp

@@ -25,6 +25,7 @@ Notes:
 #include "ast/ast_pp.h"
 #include "ast/rewriter/expr_safe_replace.h"
 #include "ast/rewriter/rewriter_def.h"
+#include "ast/rewriter/th_rewriter.h"
 #include "tactic/tactic.h"
 #include "tactic/core/reduce_invertible_tactic.h"
 #include "tactic/core/collect_occs.h"
@@ -306,6 +307,11 @@ private:
             }
             if (!rest) return false;
 
+            // so far just support numeral
+            rational r;
+            if (!m_bv.is_numeral(rest, r)) 
+                return false;
+
             // create case split on
             // divisbility of 2
             // v * t -> 
@@ -318,31 +324,30 @@ private:
             // to reproduce the original v from t
             // solve for v*t = extract[sz-1:i](v') ++ zero[i-1:0]
             // using values for t and v'
-            // thus
+            // thus let t' = t / 2^i
+            // and t'' = the multiplicative inverse of t'
+            // then t'' * v' * t = t'' * v' * t' * 2^i = v' * 2^i = extract[sz-1:i](v') ++ zero[i-1:0]
+            // so t'' *v' works 
             // 
-            //    udiv(extract[sz-1:i](v') ++ zero[i-1:0], t)
-            // 
-            // TBD: this argument is flawed. Unit test breaks with either
-            // the above or udiv(v, t)
-
             unsigned sz = m_bv.get_bv_size(p);
             expr_ref bit1(m_bv.mk_numeral(1, 1), m);
             new_v = m_bv.mk_numeral(0, sz);
-            for (unsigned i = sz; i-- > 0; ) {
+
-                expr_ref extr_i(m_bv.mk_extract(i, i, rest), m);
+            
-                expr_ref cond(m.mk_eq(extr_i, bit1), m);
+            unsigned sh = 0;
-                expr_ref part(v, m);
+            while (r.is_pos() && r.is_even()) {
-                if (i > 0) {
+                r /= rational(2);
-                    part = m_bv.mk_concat(m_bv.mk_extract(sz-1, i, v), m_bv.mk_numeral(0, i));
+                ++sh;
-                }
-                new_v = m.mk_ite(cond, part, new_v);
             }
-            if (mc) {
+            if (r.is_pos() && sh > 0) {
+                new_v = m_bv.mk_concat(m_bv.mk_extract(sz-1, sh, v), m_bv.mk_numeral(0, sh));
+            }
+            if (mc && !r.is_zero()) {
                 ensure_mc(mc);
-                expr_ref div(m), def(m);
+                expr_ref def(m);
-                div = m.mk_app(m_bv.get_fid(), OP_BUDIV_I, v, rest);
+                rational inv_r;
-                def = m_bv.mk_numeral(0, sz);
+                VERIFY(m_bv.mult_inverse(r, sz, inv_r));
-                def = m.mk_ite(m.mk_eq(def, rest), def, div);
+                def = m_bv.mk_bv_mul(m_bv.mk_numeral(inv_r, sz), v);
                 (*mc)->add(v, def);
                 TRACE("invertible_tactic", tout << def << "\n";);
             }