fix bug in hoist module, tune num2bits for large bit-vectors

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

src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h

@@ -75,9 +75,23 @@ bool bit_blaster_tpl<Cfg>::is_minus_one(unsigned sz, expr * const * bits) const
 static void _num2bits(ast_manager & m, rational const & v, unsigned sz, expr_ref_vector & out_bits) {
     SASSERT(v.is_nonneg());
     rational aux = v;
-    rational two(2);
+    rational two(2), base32(1ull << 32ull, rational::ui64());
     for (unsigned i = 0; i < sz; i++) {
-        if ((aux % two).is_zero())
+        if (i + 32 < sz) {
+            unsigned u = (aux % base32).get_unsigned();
+            for (unsigned j = 0; j < 32; ++j) {
+                if (0 != (u & (1 << j))) {
+                    out_bits.push_back(m.mk_true());
+                }
+                else {
+                    out_bits.push_back(m.mk_false());
+                }
+            }
+            aux = div(aux, base32);
+            i += 31;
+            continue;
+        }
+        else if ((aux % two).is_zero())
             out_bits.push_back(m.mk_false());
         else
             out_bits.push_back(m.mk_true());

src/ast/rewriter/hoist_rewriter.cpp

@@ -25,16 +25,16 @@ Notes:
 
 
 hoist_rewriter::hoist_rewriter(ast_manager & m, params_ref const & p):
-    m_manager(m), m_args(m) { 
+    m_manager(m), m_args1(m), m_args2(m) { 
     updt_params(p); 
 }
 
-br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * args, expr_ref & result) {
+br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * es, expr_ref & result) {
     if (num_args < 2) {
         return BR_FAILED;
     }
     for (unsigned i = 0; i < num_args; ++i) {
-        if (!is_and(args[i])) {
+        if (!is_and(es[i], nullptr)) {
             return BR_FAILED;
         }
     }
@@ -48,9 +48,10 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * args, expr_ref
     m_var2expr.reset();
     basic_union_find* uf[2] = { &m_uf1, &m_uf2 };
     obj_hashtable<expr>* preds[2] = { &m_preds1, &m_preds2 };
-    VERIFY(is_and(args[0]));
+    expr_ref_vector* args[2] = { &m_args1, &m_args2 };
+    VERIFY(is_and(es[0], args[turn]));
     expr* e1, *e2;
-    for (expr* e : m_args) {
+    for (expr* e : *(args[turn])) {
         if (m().is_eq(e, e1, e2)) {            
             (*uf)[turn].merge(mk_var(e1), mk_var(e2));
         }
@@ -69,8 +70,9 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * args, expr_ref
         (*preds)[turn].reset();
         reset(m_uf0);
         unsigned v1 = 0, v2 = 0;
-        VERIFY(is_and(args[j]));
+        VERIFY(is_and(es[j], args[turn]));
-        for (expr* e : m_args) {
+
+        for (expr* e : *args[turn]) {
             if (m().is_eq(e, e1, e2)) {
                 m_es.push_back(e1);                
                 m_uf0.merge(mk_var(e1), mk_var(e2));
@@ -79,6 +81,7 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * args, expr_ref
                 (*preds)[turn].insert(e);
             }
         }
+
         if ((*preds)[turn].empty() && m_es.empty()) {
             return BR_FAILED;
         }
@@ -109,12 +112,21 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * args, expr_ref
         for (auto const& p : m_eqs) {
             (*uf)[turn].merge(mk_var(p.first), mk_var(p.second));
         }
+        if ((*preds)[turn].empty() && m_eqs.empty()) {
+            return BR_FAILED;
+        }
     }
     // p & eqs & (or fmls)
     expr_ref_vector fmls(m()), ors(m());
     expr_safe_replace subst(m());
     for (expr * p : (*preds)[turn]) {
-        subst.insert(p, m().mk_true());
+        expr* q = nullptr;
+        if (m().is_not(p, q)) {
+            subst.insert(q, m().mk_false());
+        }
+        else {
+            subst.insert(p, m().mk_true());
+        }
         fmls.push_back(p);
     }
     for (auto const& p : m_eqs) {
@@ -124,11 +136,17 @@ br_status hoist_rewriter::mk_or(unsigned num_args, expr * const * args, expr_ref
 
     for (unsigned i = 0; i < num_args; ++i) {
         expr_ref tmp(m());
-        subst(args[i], tmp);
+        subst(es[i], tmp);
         ors.push_back(tmp);
     }
     fmls.push_back(m().mk_or(ors.size(), ors.c_ptr()));
     result = m().mk_and(fmls.size(), fmls.c_ptr());
+    TRACE("hoist", 
+          for (unsigned i = 0; i < num_args; ++i) {
+              tout << mk_pp(es[i], m()) << "\n";
+          }
+          tout << "=>\n";
+          tout << result << "\n";);
     return BR_DONE;
 }
 
@@ -154,15 +172,20 @@ br_status hoist_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c
     }
 }
 
-bool hoist_rewriter::is_and(expr * e) {
+bool hoist_rewriter::is_and(expr * e, expr_ref_vector* args) {
-    m_args.reset();
     if (m().is_and(e)) {
-        m_args.append(to_app(e)->get_num_args(), to_app(e)->get_args());
+        if (args) {
+            args->reset();
+            args->append(to_app(e)->get_num_args(), to_app(e)->get_args());
+        }
         return true;
     }
     if (m().is_not(e, e) && m().is_or(e)) {
-        for (expr* arg : *to_app(e)) {
+        if (args) {
-            m_args.push_back(::mk_not(m(), arg));
+            args->reset();
+            for (expr* arg : *to_app(e)) {
+                args->push_back(::mk_not(m(), arg));
+            }
         }
         return true;
     }

src/ast/rewriter/hoist_rewriter.h

@@ -27,7 +27,7 @@ Notes:
 
 class hoist_rewriter {
     ast_manager &  m_manager;
-    expr_ref_vector                 m_args;
+    expr_ref_vector                 m_args1, m_args2;
     obj_hashtable<expr>             m_preds1, m_preds2;
     basic_union_find                m_uf1, m_uf2, m_uf0;
     ptr_vector<expr>                m_es;
@@ -39,7 +39,7 @@ class hoist_rewriter {
 
     br_status mk_or(unsigned num_args, expr * const * args, expr_ref & result);
 
-    bool is_and(expr* e);
+    bool is_and(expr* e, expr_ref_vector* args);
 
     bool is_var(expr* e) { return m_expr2var.contains(e); }
     expr* mk_expr(unsigned v) { return m_var2expr[v]; }