diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index cf7e7c951..a3bb3b6e1 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -75,9 +75,23 @@ bool bit_blaster_tpl::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()); diff --git a/src/ast/rewriter/hoist_rewriter.cpp b/src/ast/rewriter/hoist_rewriter.cpp index ad7dffbdb..5deeebdf4 100644 --- a/src/ast/rewriter/hoist_rewriter.cpp +++ b/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* 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])); - for (expr* e : m_args) { + VERIFY(is_and(es[j], args[turn])); + + 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) { - m_args.reset(); +bool hoist_rewriter::is_and(expr * e, expr_ref_vector* args) { 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)) { - m_args.push_back(::mk_not(m(), arg)); + if (args) { + args->reset(); + for (expr* arg : *to_app(e)) { + args->push_back(::mk_not(m(), arg)); + } } return true; } diff --git a/src/ast/rewriter/hoist_rewriter.h b/src/ast/rewriter/hoist_rewriter.h index dbaeebd4d..0f45a073c 100644 --- a/src/ast/rewriter/hoist_rewriter.h +++ b/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 m_preds1, m_preds2; basic_union_find m_uf1, m_uf2, m_uf0; ptr_vector 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]; }