diff --git a/src/ast/rewriter/bv2int_translator.cpp b/src/ast/rewriter/bv2int_translator.cpp index 77a4a1d76..3200cc6c7 100644 --- a/src/ast/rewriter/bv2int_translator.cpp +++ b/src/ast/rewriter/bv2int_translator.cpp @@ -317,7 +317,6 @@ void bv2int_translator::translate_bv(app* e) { else { expr* x = arg(0), * y = umod(e, 1); r = a.mk_int(0); - IF_VERBOSE(2, verbose_stream() << "shl " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n"); for (unsigned i = 0; i < bv.get_bv_size(e); ++i) r = if_eq(y, i, mul(x, a.mk_int(rational::power_of_two(i))), r); } @@ -332,7 +331,7 @@ void bv2int_translator::translate_bv(app* e) { else { expr* x = arg(0), * y = umod(e, 1); r = a.mk_int(0); - IF_VERBOSE(2, verbose_stream() << "lshr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n"); + IF_VERBOSE(4, verbose_stream() << "lshr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n"); for (unsigned i = 0; i < bv.get_bv_size(e); ++i) r = if_eq(y, i, a.mk_idiv(x, a.mk_int(rational::power_of_two(i))), r); } @@ -352,7 +351,7 @@ void bv2int_translator::translate_bv(app* e) { expr* x = umod(e, 0), * y = umod(e, 1); expr* signx = a.mk_ge(x, a.mk_int(N / 2)); r = m.mk_ite(signx, a.mk_int(-1), a.mk_int(0)); - IF_VERBOSE(1, verbose_stream() << "ashr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n"); + IF_VERBOSE(4, verbose_stream() << "ashr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n"); for (unsigned i = 0; i < sz; ++i) { expr* d = a.mk_idiv(x, a.mk_int(rational::power_of_two(i))); r = if_eq(y, i, @@ -363,7 +362,7 @@ void bv2int_translator::translate_bv(app* e) { break; case OP_BOR: // p | q := (p + q) - band(p, q) - IF_VERBOSE(2, verbose_stream() << "bor " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n"); + IF_VERBOSE(4, verbose_stream() << "bor " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n"); r = arg(0); for (unsigned i = 1; i < args.size(); ++i) r = a.mk_sub(add(r, arg(i)), a.mk_band(bv.get_bv_size(e), r, arg(i))); @@ -372,14 +371,14 @@ void bv2int_translator::translate_bv(app* e) { r = bnot(band(args)); break; case OP_BAND: - IF_VERBOSE(2, verbose_stream() << "band " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n"); + IF_VERBOSE(4, verbose_stream() << "band " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n"); r = band(args); break; case OP_BXNOR: case OP_BXOR: { // p ^ q := (p + q) - 2*band(p, q); unsigned sz = bv.get_bv_size(e); - IF_VERBOSE(2, verbose_stream() << "bxor " << bv.get_bv_size(e) << "\n"); + IF_VERBOSE(4, verbose_stream() << "bxor " << bv.get_bv_size(e) << "\n"); r = arg(0); for (unsigned i = 1; i < args.size(); ++i) { expr* q = arg(i); diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index cb28d733a..f1983364f 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -699,6 +699,7 @@ namespace smt { switch (m_params.m_bv_solver) { case 2: m_context.register_plugin(alloc(smt::theory_intblast, m_context)); + setup_lra_arith(); return; default: break; diff --git a/src/smt/theory_intblast.cpp b/src/smt/theory_intblast.cpp index e3b815a3d..82feb39bc 100644 --- a/src/smt/theory_intblast.cpp +++ b/src/smt/theory_intblast.cpp @@ -13,6 +13,7 @@ Author: #include "smt/smt_context.h" #include "smt/theory_intblast.h" +#include "smt/smt_model_generator.h" namespace smt { @@ -134,9 +135,34 @@ namespace smt { bool theory_intblast::internalize_atom(app * atom, bool gate_ctx) { return internalize_term(atom); } + + void theory_intblast::apply_sort_cnstr(enode* n, sort* s) { + SASSERT(bv.is_bv_sort(s)); + if (!is_attached_to_var(n)) { + m_translator.internalize_bv(n->get_expr()); + auto v = mk_var(n); + ctx.attach_th_var(n, this, v); + } + } bool theory_intblast::internalize_term(app* term) { + + ctx.internalize(term->get_args(), term->get_num_args(), false); m_translator.internalize_bv(term); + enode* n; + if (!ctx.e_internalized(term)) + n = ctx.mk_enode(term, false, false, false); + else + n = ctx.get_enode(term); + + if (!is_attached_to_var(n)) { + auto v = mk_var(n); + ctx.attach_th_var(n, this, v); + } + if (m.is_bool(term)) { + literal l(ctx.mk_bool_var(term)); + ctx.set_var_theory(l.var(), get_id()); + } return true; } @@ -144,5 +170,24 @@ namespace smt { m_translator.translate_eq(atom); } + void theory_intblast::init_model(model_generator& mg) { + m_factory = alloc(bv_factory, m); + mg.register_factory(m_factory); + } + model_value_proc* theory_intblast::mk_value(enode* n, model_generator& mg) { + expr* e = n->get_expr(); + SASSERT(bv.is_bv(e)); + auto ie = m_translator.translated(e); + expr_ref val(m); + rational r; + if (bv.is_numeral(e, r)) + ; + else { + VERIFY(ctx.get_value(ctx.get_enode(ie), val)); + VERIFY(a.is_numeral(val, r)); + } + return alloc(expr_wrapper_proc, m_factory->mk_num_value(r, bv.get_bv_size(e))); + } + } diff --git a/src/smt/theory_intblast.h b/src/smt/theory_intblast.h index a3db28141..b30c6931d 100644 --- a/src/smt/theory_intblast.h +++ b/src/smt/theory_intblast.h @@ -21,6 +21,7 @@ Author: #include "ast/sls/sat_ddfw.h" #include "smt/smt_theory.h" #include "model/model.h" +#include "model/numeral_factory.h" #include "ast/rewriter/bv2int_translator.h" @@ -42,6 +43,7 @@ namespace smt { bv_util bv; arith_util a; unsigned m_vars_qhead = 0, m_preds_qhead = 0; + bv_factory * m_factory = nullptr; bool add_bound_axioms(); bool add_predicate_axioms(); @@ -60,6 +62,9 @@ namespace smt { bool internalize_atom(app * atom, bool gate_ctx) override; bool internalize_term(app* term) override; void internalize_eq_eh(app * atom, bool_var v) override; + void apply_sort_cnstr(enode* n, sort* s) override; + void init_model(model_generator& m) override; + model_value_proc* mk_value(enode* n, model_generator& m) override; void new_eq_eh(theory_var v1, theory_var v2) override {} void new_diseq_eh(theory_var v1, theory_var v2) override {}