diff --git a/src/qe/qe_mbi.cpp b/src/qe/qe_mbi.cpp index b7de8d302..dd0d36418 100644 --- a/src/qe/qe_mbi.cpp +++ b/src/qe/qe_mbi.cpp @@ -126,30 +126,29 @@ namespace qe { struct euf_arith_mbi_plugin::is_arith_var_proc { ast_manager& m; app_ref_vector& m_avars; - arith_util arith; + app_ref_vector& m_proxies; + arith_util m_arith; obj_hashtable m_seen; - is_arith_var_proc(app_ref_vector& avars): - m(avars.m()), m_avars(avars), arith(m) { + is_arith_var_proc(app_ref_vector& avars, app_ref_vector& proxies): + m(avars.m()), m_avars(avars), m_proxies(proxies), m_arith(m) { } void operator()(app* a) { if (is_arith_op(a) || a->get_family_id() == m.get_basic_family_id()) { - // no-op + return; } - else if (!arith.is_int_real(a)) { - for (expr* arg : *a) { - if (is_app(arg) && !m_seen.contains(arg) && is_arith_op(to_app(arg))) { - m_avars.push_back(to_app(arg)); - m_seen.insert(arg); - } - } - } - else if (!m_seen.contains(a)) { - m_seen.insert(a); + + if (m_arith.is_int_real(a)) { m_avars.push_back(a); } + for (expr* arg : *a) { + if (is_app(arg) && !m_seen.contains(arg) && m_arith.is_int_real(arg)) { + m_proxies.push_back(to_app(arg)); + m_seen.insert(arg); + } + } } bool is_arith_op(app* a) { - return a->get_family_id() == arith.get_family_id(); + return a->get_family_id() == m_arith.get_family_id(); } void operator()(expr*) {} }; @@ -221,9 +220,9 @@ namespace qe { /** * \brief extract arithmetical variables and arithmetical terms in shared positions. */ - app_ref_vector euf_arith_mbi_plugin::get_arith_vars(model_ref& mdl, expr_ref_vector& lits) { + app_ref_vector euf_arith_mbi_plugin::get_arith_vars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& proxies) { app_ref_vector avars(m); - is_arith_var_proc _proc(avars); + is_arith_var_proc _proc(avars, proxies); for_each_expr(_proc, lits); return avars; } @@ -259,14 +258,15 @@ namespace qe { TRACE("qe", tout << lits << "\n" << *mdl << "\n";); // 1. arithmetical variables - atomic and in purified positions - app_ref_vector avars = get_arith_vars(mdl, lits); - TRACE("qe", tout << "vars: " << avars << "\nlits: " << lits << "\n";); + app_ref_vector proxies(m); + app_ref_vector avars = get_arith_vars(mdl, lits, proxies); + TRACE("qe", tout << "vars: " << avars << "\nproxies: " << proxies << "\nlits: " << lits << "\n";); // 2. project private non-arithmetical variables from lits project_euf(mdl, lits, avars); // 3. Order arithmetical variables and purified positions - order_avars(mdl, lits, avars); + order_avars(mdl, lits, avars, proxies); TRACE("qe", tout << "ordered: " << lits << "\n";); // 4. Perform arithmetical projection @@ -307,15 +307,14 @@ namespace qe { /** * \brief Order arithmetical variables: - * 1. add literals that order the variable according to the model. - * 2. remove non-atomic arithmetical terms from projection. + * 1. add literals that order the proxies according to the model. * 2. sort arithmetical terms, such that deepest terms are first. */ - void euf_arith_mbi_plugin::order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars) { + void euf_arith_mbi_plugin::order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars, app_ref_vector const& proxies) { arith_util a(m); model_evaluator mev(*mdl.get()); vector> vals; - for (app* v : avars) { + for (app* v : proxies) { rational val; expr_ref tmp = mev(v); VERIFY(a.is_numeral(tmp, val)); @@ -327,7 +326,7 @@ namespace qe { return x.first < y.first; } }; - // add linear order between avars + // add linear order between proxies compare_first cmp; std::sort(vals.begin(), vals.end(), cmp); for (unsigned i = 1; i < vals.size(); ++i) { @@ -338,6 +337,7 @@ namespace qe { lits.push_back(a.mk_lt(vals[i-1].second, vals[i].second)); } } + // filter out only private variables filter_private_arith(avars); diff --git a/src/qe/qe_mbi.h b/src/qe/qe_mbi.h index 23294ee6e..aa5d935b4 100644 --- a/src/qe/qe_mbi.h +++ b/src/qe/qe_mbi.h @@ -103,12 +103,12 @@ namespace qe { struct is_atom_proc; struct is_arith_var_proc; - app_ref_vector get_arith_vars(model_ref& mdl, expr_ref_vector& lits); + app_ref_vector get_arith_vars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& proxies); bool get_literals(model_ref& mdl, expr_ref_vector& lits); void collect_atoms(expr_ref_vector const& fmls); void project(model_ref& mdl, expr_ref_vector& lits); void project_euf(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars); - void order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars); + void order_avars(model_ref& mdl, expr_ref_vector& lits, app_ref_vector& avars, app_ref_vector const& proxies); void substitute(vector const& defs, expr_ref_vector& lits); void filter_private_arith(app_ref_vector& avars); public: diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 5dea80f5e..c79068298 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -200,6 +200,7 @@ namespace smt { out << "current assignment:\n"; for (literal lit : m_assigned_literals) { display_literal(out, lit); + if (!is_relevant(lit)) out << " n "; out << ": "; display_verbose(out, m_manager, 1, &lit, m_bool_var2expr.c_ptr()); out << "\n"; diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 6e1626cc1..3a5f5e709 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -53,6 +53,7 @@ namespace smt { unsigned bv_size = get_bv_size(n); context & ctx = get_context(); literal_vector & bits = m_bits[v]; + TRACE("bv", tout << "v" << v << "\n";); bits.reset(); for (unsigned i = 0; i < bv_size; i++) { app * bit = mk_bit2bool(owner, i); @@ -77,6 +78,7 @@ namespace smt { context & ctx = get_context(); SASSERT(!ctx.b_internalized(n)); + TRACE("bv", tout << "bit2bool: " << mk_pp(n, ctx.get_manager()) << "\n";); expr* first_arg = n->get_arg(0); if (!ctx.e_internalized(first_arg)) { @@ -98,17 +100,20 @@ namespace smt { rational val; unsigned sz; if (!ctx.b_internalized(n) && m_util.is_numeral(first_arg, val, sz)) { + + TRACE("bv", tout << "bit2bool constants\n";); theory_var v = first_arg_enode->get_th_var(get_id()); app* owner = first_arg_enode->get_owner(); for (unsigned i = 0; i < sz; ++i) { - ctx.internalize(mk_bit2bool(owner, i), true); + app* e = mk_bit2bool(owner, i); + ctx.internalize(e, true); } m_bits[v].reset(); rational bit; for (unsigned i = 0; i < sz; ++i) { div(val, rational::power_of_two(i), bit); mod(bit, rational(2), bit); - m_bits[v].push_back(bit.is_zero()?false_literal:true_literal); + m_bits[v].push_back(bit.is_zero()?false_literal:true_literal); } } } @@ -135,6 +140,18 @@ namespace smt { SASSERT(a->m_occs == 0); a->m_occs = new (get_region()) var_pos_occ(v_arg, idx); } + rational val; + unsigned sz; + if (m_util.is_numeral(first_arg, val, sz)) { + rational bit; + unsigned idx = n->get_decl()->get_parameter(0).get_int(); + div(val, rational::power_of_two(idx), bit); + mod(bit, rational(2), bit); + literal lit = ctx.get_literal(n); + if (bit.is_zero()) lit.neg(); + ctx.mark_as_relevant(lit); + ctx.mk_th_axiom(get_id(), 1, &lit); + } } void theory_bv::process_args(app * n) { @@ -622,7 +639,9 @@ namespace smt { context& ctx = get_context(); process_args(n); mk_enode(n); - mk_bits(ctx.get_enode(n)->get_th_var(get_id())); + theory_var v = ctx.get_enode(n)->get_th_var(get_id()); + mk_bits(v); + if (!ctx.relevancy()) { assert_int2bv_axiom(n); } @@ -1179,7 +1198,7 @@ namespace smt { m_prop_queue.push_back(var_pos(curr->m_var, curr->m_idx)); curr = curr->m_next; } - TRACE("bv", tout << m_prop_queue.size() << "\n";); + TRACE("bv", tout << "prop queue size: " << m_prop_queue.size() << "\n";); propagate_bits(); } } @@ -1196,7 +1215,7 @@ namespace smt { literal_vector & bits = m_bits[v]; literal bit = bits[idx]; - lbool val = ctx.get_assignment(bit); + lbool val = ctx.get_assignment(bit); if (val == l_undef) { continue; } @@ -1213,6 +1232,7 @@ namespace smt { SASSERT(bit != ~bit2); lbool val2 = ctx.get_assignment(bit2); TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v2)->get_owner_id() << "[" << idx << "] = " << val2 << "\n";); + TRACE("bv", tout << bit << " " << bit2 << "\n";); if (val != val2) { literal consequent = bit2;